Theorem: fermatLastTheoremFive (FltRegular/FLT5.lean)

State before:
⊢ FermatLastTheoremFor 5
Tactic:
have : Fact (Nat.Prime 5) := ⟨by norm_num⟩
State after:
this : Fact (Nat.Prime 5)
⊢ FermatLastTheoremFor 5

State before:
this : Fact (Nat.Prime 5)
⊢ FermatLastTheoremFor 5
Tactic:
refine flt_regular ?_ (by omega)
State after:
this : Fact (Nat.Prime 5)
⊢ IsRegularPrime 5

State before:
this : Fact (Nat.Prime 5)
⊢ IsRegularPrime 5
Tactic:
rw [IsRegularPrime, IsRegularNumber]
State after:
this : Fact (Nat.Prime 5)
⊢ Coprime 5 (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨5, ⋯⟩ ℚ))))

State before:
this : Fact (Nat.Prime 5)
⊢ Coprime 5 (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨5, ⋯⟩ ℚ))))
Tactic:
convert coprime_one_right _
State after:
case h.e'_2
this : Fact (Nat.Prime 5)
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨5, ⋯⟩ ℚ))) = 1

State before:
case h.e'_2
this : Fact (Nat.Prime 5)
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨5, ⋯⟩ ℚ))) = 1
Tactic:
exact classNumber_eq_one_iff.2 (Rat.five_pid (CyclotomicField _ ℚ))
State after:
no goals

State before:
⊢ Nat.Prime 5
Tactic:
norm_num
State after:
no goals

State before:
this : Fact (Nat.Prime 5)
⊢ 5 ≠ 2
Tactic:
omega
State after:
no goals