Lean Proof

# Lean Proof Methodology

These are non-negotiable constraints for writing Lean proofs correctly.

## One Step at a Time

Write one tactic, check diagnostics (use `done` to see unsolved goals), repeat. Never write multiple tactics before checking.

**`by sorry` is acceptable**: For placeholders you're not actively working on.
**`done` is required**: When you expect there to be next steps in an active proof.

## Error Priority

Fix errors in this order — higher-priority errors make lower-priority ones unreliable:

1. **Syntax errors** → 2. **Type errors** → 3. **Unsolved goals / tactic failures** → 4. **Linter warnings**

"Unsolved goals" errors appear on `by` or `=>` lines, NOT where you add tactics. If there's an "unsolved goals" on line 59 but a tactic error on line 65 — fix line 65 FIRST.

Stop writing tactics after any error.

## Work on the Hardest Case First

### Across Theorems

Go directly to the target theorem. Don't fill in `sorry`s in helper lemmas first — Lean treats `sorry` as an axiom, so dependent theorems still work.

Move sorries earlier in the file by replacing a `sorry` proof with references to simpler lemmas:

```lean
-- Before:
theorem main_theorem : A = C := by sorry

-- After:
theorem lemma1 : A = B := by sorry
theorem lemma2 : B = C := by sorry
theorem main_theorem : A = C := by
  rw [lemma1, lemma2]
```

### Within a Proof

When a proof has multiple cases, `sorry` the easy cases and work on the hardest one first. If the hard case fails, effort on easy cases is wasted.

```lean
match n with
| 0 => sorry -- fill in later
| 1 => sorry -- fill in later
| n + 2 => -- WORK ON THIS FIRST
```

## Proof Cleanup

After getting a proof to work, clean it up immediately:
- Combine redundant steps (`rw [a]; rw [b]` → `rw [a, b]`)
- Test if `simp` can handle more (remove earlier steps one by one)
- Find the truly minimal proof

## Dependent Type Rewriting Issues

**When you encounter "motive is not type correct" or similar errors during rewriting:**

### The Problem

Rewriting a term `b` that appears in dependent types (like `hab : a ≤ b`) fails because the motive cannot abstract over the dependencies.

```lean
have hb : b = f x
rw [hb]  -- Error: motive is not type correct
```

### The Solution: Generalize First, Instantiate Last

Prove a generalized statement for an arbitrary parameter, then instantiate:

```lean
suffices ∀ s, statement_about s by
  have h_specific := the_equality_you_have
  convert this ?_ <;> exact h_specific
intro s
-- Now prove the general statement for arbitrary s
```

This works because the generalized statement has no dependencies on the problematic term, and `convert` handles the dependent type coercions at the end.

## Verification

Never declare a proof complete while `sorry` placeholders or error diagnostics remain.