awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n].TFAE
have tfae_3_iff_1 : FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremFor n
Tactic: tfae_have 3 ↔ 1 := by
    rw [fermatLastTheoremFor_iff_int]
    apply fermatLastTheoremWith'_iff_fermatLastTheoremWith
    intro a b c ha hb hc
    by_cases hn : n = 0
    · subst hn
      simp only [pow_zero, Int.reduceAdd, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true]
    · rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc
      -- case division
      rcases ha with ha | ha <;> rcases hb with hb | hb <;> rcases hc with hc | hc <;>
        rw [ha, hb, hc] <;> decide
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
⊢ False
have obtain : ∀ (A : R) (hA : a = d * A), False
Tactic: obtain ⟨A, hA⟩ : d ∣ a := gcd_dvd (by simp [s])
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
⊢ False
have obtain : ∀ (B : R) (hB : b = d * B), False
Tactic: obtain ⟨B, hB⟩ : d ∣ b := gcd_dvd (by simp [s])
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
⊢ False
have obtain : ∀ (C : R) (hC : c = d * C), False
Tactic: obtain ⟨C, hC⟩ : d ∣ c := gcd_dvd (by simp [s])
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
⊢ False
have ha₁ : d ≠ 0 ∧ A ≠ 0
Tactic: simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc
Cleared hypotheses: ha, hb, hc, habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha₁ : d ≠ 0 ∧ A ≠ 0
⊢ False
have hb₁ : d ≠ 0 ∧ B ≠ 0
Tactic: simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc
Cleared hypotheses: ha, hb, hc, habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha₁ : d ≠ 0 ∧ A ≠ 0
hb₁ : d ≠ 0 ∧ B ≠ 0
⊢ False
have hc₁ : d ≠ 0 ∧ C ≠ 0
Tactic: simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc
Cleared hypotheses: ha, hb, hc, habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha₁ : d ≠ 0 ∧ A ≠ 0
hb₁ : d ≠ 0 ∧ B ≠ 0
hc₁ : d ≠ 0 ∧ C ≠ 0
⊢ False
have habc₁ : d ^ n * A ^ n + d ^ n * B ^ n = d ^ n * C ^ n
Tactic: simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc
Cleared hypotheses: ha, hb, hc, habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : d ^ n * A ^ n + d ^ n * B ^ n = d ^ n * C ^ n
⊢ False
have habc₁ : A ^ n + B ^ n = C ^ n
Tactic: rw [← mul_add, mul_right_inj' (pow_ne_zero n ha.1)] at habc
Cleared hypotheses: habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ False
have refine : Eq (α := R) (Finset.gcd {A, B, C} id) 1
Tactic: refine hn A B C ha.2 hb.2 hc.2 ?_ habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ Eq (α := R) (Finset.gcd {A, B, C} id) 1
have rw : IsUnit (M := R) (Finset.gcd {A, B, C} id)
Tactic: rw [← Finset.normalize_gcd, normalize_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ IsUnit (M := R) (Finset.gcd {A, B, C} id)
have obtain : ∀ (u : Rˣ) (hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d),
  IsUnit (M := R) (Finset.gcd {A, B, C} id)
Tactic: obtain ⟨u, hu⟩ := normalize_associated d
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
⊢ IsUnit (M := R) (Finset.gcd {A, B, C} id)
have refine : d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
Tactic: refine ⟨u, mul_left_cancel₀ (mt normalize_eq_zero.mp ha.1) (hu.symm ▸ ?_)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₄ : d = Finset.gcd {d * id A, d * id B, d * id C} id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
rw₄ : d = Finset.gcd {d * id A, d * id B, d * id C} id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₅ : d = Finset.gcd {d * A, d * id B, d * id C} id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
rw₄ : d = Finset.gcd {d * id A, d * id B, d * id C} id
rw₅ : d = Finset.gcd {d * A, d * id B, d * id C} id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₆ : d = Finset.gcd {d * A, d * B, d * id C} id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
rw₄ : d = Finset.gcd {d * id A, d * id B, d * id C} id
rw₅ : d = Finset.gcd {d * A, d * id B, d * id C} id
rw₆ : d = Finset.gcd {d * A, d * B, d * id C} id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₇ : d = Finset.gcd {d * A, d * B, d * C} id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
rw₄ : d = Finset.gcd {d * id A, d * id B, d * id C} id
rw₅ : d = Finset.gcd {d * A, d * id B, d * id C} id
rw₆ : d = Finset.gcd {d * A, d * B, d * id C} id
rw₇ : d = Finset.gcd {d * A, d * B, d * C} id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₈ : d = Finset.gcd {a, d * B, d * C} id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
rw₄ : d = Finset.gcd {d * id A, d * id B, d * id C} id
rw₅ : d = Finset.gcd {d * A, d * id B, d * id C} id
rw₆ : d = Finset.gcd {d * A, d * B, d * id C} id
rw₇ : d = Finset.gcd {d * A, d * B, d * C} id
rw₈ : d = Finset.gcd {a, d * B, d * C} id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₉ : d = Finset.gcd {a, b, d * C} id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
rw₄ : d = Finset.gcd {d * id A, d * id B, d * id C} id
rw₅ : d = Finset.gcd {d * A, d * id B, d * id C} id
rw₆ : d = Finset.gcd {d * A, d * B, d * id C} id
rw₇ : d = Finset.gcd {d * A, d * B, d * C} id
rw₈ : d = Finset.gcd {a, d * B, d * C} id
rw₉ : d = Finset.gcd {a, b, d * C} id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
have rw₁₀ : d = Finset.gcd {a, b, c} id
Tactic: rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
⊢ p ∣ c
have inl : ∀ (HF : HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 + HPow.hPow (β := ℕ) c 0 = 0), p ∣ c
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n, HF
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
inl : ∀ (HF : HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 + HPow.hPow (β := ℕ) c 0 = 0), p ∣ c
⊢ p ∣ c
have inr : ∀ (hn : n ≠ 0), p ∣ c
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ c
have inr : p ∣ -c ^ n
Tactic: refine hp.dvd_of_dvd_pow (n := n) (dvd_neg.1 ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ -c ^ n
have HF₁ : a ^ n + b ^ n = -c ^ n
Tactic: rw [add_eq_zero_iff_eq_neg] at HF
Cleared hypotheses: HF, hn
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
⊢ IsCoprime a b
have inl : ∀ (HF : HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 + HPow.hPow (β := ℕ) c 0 = 0), IsCoprime a b
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n, HF
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
inl : ∀ (HF : HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 + HPow.hPow (β := ℕ) c 0 = 0), IsCoprime a b
⊢ IsCoprime a b
have inr : ∀ (hn : n ≠ 0), IsCoprime a b
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ IsCoprime a b
have inr : ¬(a = 0 ∧ b = 0)
Tactic: refine isCoprime_of_prime_dvd ?_ <| (fun p hp hpa hpb ↦ hp.not_dvd_one ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
inr : ¬(a = 0 ∧ b = 0)
⊢ IsCoprime a b
have inr₁ : ∀ (p : ℤ) (hp : Prime p) (hpa : p ∣ a) (hpb : p ∣ b), p ∣ 1
Tactic: refine isCoprime_of_prime_dvd ?_ <| (fun p hp hpa hpb ↦ hp.not_dvd_one ?_)