Choose the smallest suspect, again

Lean definition · original excerpt

Mathlib · db584cd · Four.lean

58/-- We say a solution to `a ^ 4 + b ^ 4 = c ^ 2` is minimal if there is no other solution with59a smaller `c` (in absolute value). -/60def Minimal (a b c : ℤ) : Prop :=61  Fermat42 a b c ∧ ∀ a1 b1 c1 : ℤ, Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c162 63/-- if we have a solution to `a ^ 4 + b ^ 4 = c ^ 2` then there must be a minimal one. -/64theorem exists_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minimal a0 b0 c0 := by65  classical66  let S : Set ℕ := { n | ∃ s : ℤ × ℤ × ℤ, Fermat42 s.1 s.2.1 s.2.2 ∧ n = Int.natAbs s.2.2 }67  have S_nonempty : S.Nonempty := by68    use Int.natAbs c69    rw [Set.mem_ofPred_eq]70    use ⟨a, ⟨b, c⟩⟩71  let m : ℕ := Nat.find S_nonempty72  have m_mem : m ∈ S := Nat.find_spec S_nonempty73  rcases m_mem with ⟨s0, hs0, hs1⟩74  use s0.1, s0.2.1, s0.2.2, hs075  intro a1 b1 c1 h176  rw [← hs1]77  apply Nat.find_min'78  use ⟨a1, ⟨b1, c1⟩⟩

How to read this Lean

The proof is mechanical well-ordering: the set S collects the |c| values that solutions realize; S_nonempty installs the given solution; Nat.find picks its least member; Nat.find_min' turns that into the universal claim over all solutions. The witness tuple s is unpacked by rcases on the way. From here a descent can always speak of “the smallest gauge”.