awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
tfae_2_to_3 : ∀ (a : FermatLastTheoremWith ℤ n), FermatLastTheoremWith ℚ n
⊢ FermatLastTheoremWith ℕ n

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
tfae_2_to_3 : ∀ (a : FermatLastTheoremWith ℤ n), FermatLastTheoremWith ℚ n
⊢ ∀ (a : FermatLastTheoremWith ℚ n), FermatLastTheoremWith ℕ n

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
tfae_2_to_3 : ∀ (a : FermatLastTheoremWith ℤ n), FermatLastTheoremWith ℚ n
⊢ ∀ (a : FermatLastTheoremWith ℚ n), FermatLastTheoremWith ℕ n

Tactic:
tfae_have 3 → 1
  | h, a, b, c => mod_cast h a b c
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
tfae_2_to_3 : ∀ (a : FermatLastTheoremWith ℤ n), FermatLastTheoremWith ℚ n
tfae_3_to_1 : ∀ (a : FermatLastTheoremWith ℚ n), FermatLastTheoremWith ℕ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremFor n ↔ FermatLastTheoremWith ℕ n

Tactic:
Iff.rfl

Premises used: Iff.rfl, FermatLastTheoremFor
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremFor n ↔ FermatLastTheoremWith ℤ n

Tactic:
(fermatLastTheoremWith_nat_int_rat_tfae n).out 0 1

Premises used: fermatLastTheoremWith_nat_int_rat_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremFor n ↔ FermatLastTheoremWith ℚ n

Tactic:
(fermatLastTheoremWith_nat_int_rat_tfae n).out 0 2

Premises used: fermatLastTheoremWith_nat_int_rat_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
h_1 : a ≠ 0
h_2 : b ≠ 0
h_3 : c ≠ 0
h_4 : a ^ n + b ^ n = c ^ n
exfalso : False
⊢ ∃ (d : R) (a' : R) (b' : R) (c' : R), (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
h_1 : a ≠ 0
h_2 : b ≠ 0
h_3 : c ≠ 0
h_4 : a ^ n + b ^ n = c ^ n
a₁ : a ≠ 0
a₂ : b ≠ 0
a₃ : c ≠ 0
a₄ : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
apply h a b c
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
h_1 : a ≠ 0
h_2 : b ≠ 0
h_3 : c ≠ 0
h_4 : a ^ n + b ^ n = c ^ n
⊢ a ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
h_1 : a ≠ 0
h_2 : b ≠ 0
h_3 : c ≠ 0
h_4 : a ^ n + b ^ n = c ^ n
⊢ b ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
h_1 : a ≠ 0
h_2 : b ≠ 0
h_3 : c ≠ 0
h_4 : a ^ n + b ^ n = c ^ n
⊢ c ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
h_1 : a ≠ 0
h_2 : b ≠ 0
h_3 : c ≠ 0
h_4 : a ^ n + b ^ n = c ^ n
⊢ a ^ n + b ^ n = c ^ n

Tactic:
assumption
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
𝕜 : Type u_2
inst : Semifield 𝕜
n : ℕ
⊢ FermatLastTheoremWith' 𝕜 n

Tactic:
fun a b c ha hb hc _ ↦
  ⟨1, a, b, c,
    ⟨(mul_one a).symm, (mul_one b).symm, (mul_one c).symm⟩,
    ⟨ha.isUnit, hb.isUnit, hc.isUnit⟩⟩

Premises used: Ne.isUnit, And.intro, Exists.intro, mul_one, OfNat.ofNat, Eq.symm, FermatLastTheoremWith'
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
rcases :
  ∀ (d a' b' c' : R) (ha : a' * d ≠ 0) (hb : b' * d ≠ 0) (hc : c' * d ≠ 0)
    (heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n) (ua : IsUnit a') (ub : IsUnit b') (uc : IsUnit c'), False
⊢ False

Tactic:
rcases h a b c ha hb hc heq with ⟨d, a', b', c', ⟨rfl, rfl, rfl⟩, ⟨ua, ub, uc⟩⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n

Tactic:
rw [mul_pow, mul_pow, mul_pow, ← add_mul] at heq

Premises used: add_mul, mul_pow
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
heq₁ : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
⊢ IsUnit a'

Tactic:
rw [mul_pow, mul_pow, mul_pow, ← add_mul] at heq

Premises used: add_mul, mul_pow
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
heq₁ : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
ua₁ : IsUnit a'
⊢ IsUnit b'

Tactic:
rw [mul_pow, mul_pow, mul_pow, ← add_mul] at heq

Premises used: add_mul, mul_pow
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
heq₁ : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
ua₁ : IsUnit a'
ub₁ : IsUnit b'
⊢ IsUnit c'

Tactic:
rw [mul_pow, mul_pow, mul_pow, ← add_mul] at heq

Premises used: add_mul, mul_pow
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False

Tactic:
hn _ _ _ ua ub uc <| mul_right_cancel₀ (pow_ne_zero _ (right_ne_zero_of_mul ha)) heq

Premises used: pow_ne_zero, right_ne_zero_of_mul, mul_right_cancel₀
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False

Tactic:
exact hn _ _ _ ua ub uc <| mul_right_cancel₀ (pow_ne_zero _ (right_ne_zero_of_mul ha)) heq

Premises used: pow_ne_zero, right_ne_zero_of_mul, mul_right_cancel₀
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
n : ℕ
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
⊢ FermatLastTheoremWith' R n ↔ FermatLastTheoremWith R n

Tactic:
Iff.intro (fun h ↦ h.fermatLastTheoremWith hn) (fun h ↦ h.fermatLastTheoremWith')

Premises used: FermatLastTheoremWith.fermatLastTheoremWith', Iff.intro, FermatLastTheoremWith'.fermatLastTheoremWith
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremWith' ℕ n

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremFor n

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n

Tactic:
2 ↔ 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
hn : ∀ (a b c : ℕ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
⊢ FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n

Tactic:
apply fermatLastTheoremWith'_iff_fermatLastTheoremWith

Premises used: fermatLastTheoremWith'_iff_fermatLastTheoremWith
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
hn : ∀ (a b c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n
⊢ ∀ (a b c : ℕ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n

Tactic:
simp only [Nat.isUnit_iff]

Premises used: Nat.isUnit_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n a : ℕ
hn : ∀ (b c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n
⊢ ∀ (b c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n

Tactic:
_
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n a b : ℕ
hn : ∀ (c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n
⊢ ∀ (c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n

Tactic:
_
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n a b c : ℕ
ha : a = 1
hb : b = 1
hc : c = 1
hn : HPow.hPow (α := ℕ) 1 n + HPow.hPow (α := ℕ) 1 n ≠ HPow.hPow (α := ℕ) 1 n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n a b c : ℕ
ha : a = 1
hb : b = 1
hc : c = 1
⊢ HPow.hPow (α := ℕ) 1 n + HPow.hPow (α := ℕ) 1 n ≠ HPow.hPow (α := ℕ) 1 n

Tactic:
simp only [one_pow, Nat.reduceAdd, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true]

Premises used: one_pow, OfNat.ofNat_ne_one, Nat.reduceAdd, ne_eq, not_false_eq_true
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n

Tactic:
tfae_have 2 ↔ 1 := by
    apply fermatLastTheoremWith'_iff_fermatLastTheoremWith
    simp only [Nat.isUnit_iff]
    intro _ _ _ ha hb hc
    rw [ha, hb, hc]
    simp only [one_pow, Nat.reduceAdd, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ FermatLastTheoremWith' ℤ n

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ FermatLastTheoremFor n

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremFor n

Tactic:
3 ↔ 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
rw : FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremWith ℤ n
⊢ FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremFor n

Tactic:
rw [fermatLastTheoremFor_iff_int]

Premises used: fermatLastTheoremFor_iff_int
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
hn : ∀ (a b c : ℤ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
⊢ FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremWith ℤ n

Tactic:
apply fermatLastTheoremWith'_iff_fermatLastTheoremWith

Premises used: fermatLastTheoremWith'_iff_fermatLastTheoremWith
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
pos : ∀ (hn : n = 0), a ^ n + b ^ n ≠ c ^ n
neg : ∀ (hn : ¬n = 0), a ^ n + b ^ n ≠ c ^ n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hn : n = 0
pos :
  ∀ (tfae_2_iff_1 : FermatLastTheoremWith' ℕ 0 ↔ FermatLastTheoremFor 0),
    HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 ≠ HPow.hPow (β := ℕ) c 0
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
subst hn
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
tfae_2_iff_1 : FermatLastTheoremWith' ℕ 0 ↔ FermatLastTheoremFor 0
⊢ HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 ≠ HPow.hPow (β := ℕ) c 0

Tactic:
simp only [pow_zero, Int.reduceAdd, ne_eq, OfNat.ofNat_ne_one, not_false_eq_true]

Premises used: Int.reduceAdd, OfNat.ofNat_ne_one, ne_eq, pow_zero, not_false_eq_true
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hn : ¬n = 0
⊢ a ^ n = 1 ∨ a ^ n = -1

Tactic:
rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc

Premises used: isUnit_pow_iff, Int.isUnit_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hn : ¬n = 0
ha₁ : a ^ n = 1 ∨ a ^ n = -1
⊢ b ^ n = 1 ∨ b ^ n = -1

Tactic:
rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc

Premises used: isUnit_pow_iff, Int.isUnit_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hn : ¬n = 0
ha₁ : a ^ n = 1 ∨ a ^ n = -1
hb₁ : b ^ n = 1 ∨ b ^ n = -1
⊢ c ^ n = 1 ∨ c ^ n = -1

Tactic:
rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc

Premises used: isUnit_pow_iff, Int.isUnit_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hn : ¬n = 0
ha₁ : a ^ n = 1 ∨ a ^ n = -1
hb₁ : b ^ n = 1 ∨ b ^ n = -1
hc₁ : c ^ n = 1 ∨ c ^ n = -1
⊢ ¬n = 0

Tactic:
rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc

Premises used: isUnit_pow_iff, Int.isUnit_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : a ^ n = 1 ∨ a ^ n = -1
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
neg : ∀ (ha : a ^ n = 1), a ^ n + b ^ n ≠ c ^ n
neg₁ : ∀ (ha : a ^ n = -1), a ^ n + b ^ n ≠ c ^ n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases ha with ha | ha
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
neg : ∀ (hb : b ^ n = 1), a ^ n + b ^ n ≠ c ^ n
neg₁ : ∀ (hb : b ^ n = -1), a ^ n + b ^ n ≠ c ^ n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases hb with hb | hb
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
neg : ∀ (hb : b ^ n = 1), a ^ n + b ^ n ≠ c ^ n
neg₁ : ∀ (hb : b ^ n = -1), a ^ n + b ^ n ≠ c ^ n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases hb with hb | hb
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
neg : ∀ (hc : c ^ n = 1), a ^ n + b ^ n ≠ c ^ n
neg₁ : ∀ (hc : c ^ n = -1), a ^ n + b ^ n ≠ c ^ n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases hc with hc | hc
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
neg : ∀ (hc : c ^ n = 1), a ^ n + b ^ n ≠ c ^ n
neg₁ : ∀ (hc : c ^ n = -1), a ^ n + b ^ n ≠ c ^ n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases hc with hc | hc
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
neg : ∀ (hc : c ^ n = 1), a ^ n + b ^ n ≠ c ^ n
neg₁ : ∀ (hc : c ^ n = -1), a ^ n + b ^ n ≠ c ^ n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases hc with hc | hc
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
neg : ∀ (hc : c ^ n = 1), a ^ n + b ^ n ≠ c ^ n
neg₁ : ∀ (hc : c ^ n = -1), a ^ n + b ^ n ≠ c ^ n
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases hc with hc | hc
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = 1
neg : HAdd.hAdd (α := ℤ) 1 1 ≠ 1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = -1
neg : HAdd.hAdd (α := ℤ) 1 1 ≠ -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = 1
neg : HAdd.hAdd (α := ℤ) 1 (-1) ≠ 1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = -1
neg : HAdd.hAdd (α := ℤ) 1 (-1) ≠ -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = 1
neg : HAdd.hAdd (α := ℤ) (-1) 1 ≠ 1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = -1
neg : HAdd.hAdd (α := ℤ) (-1) 1 ≠ -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = 1
neg : HAdd.hAdd (α := ℤ) (-1) (-1) ≠ 1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = -1
neg : HAdd.hAdd (α := ℤ) (-1) (-1) ≠ -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = 1
⊢ HAdd.hAdd (α := ℤ) 1 1 ≠ 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ HAdd.hAdd (α := ℤ) 1 1 ≠ -1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ HAdd.hAdd (α := ℤ) 1 (-1) ≠ 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ HAdd.hAdd (α := ℤ) 1 (-1) ≠ -1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = 1
⊢ HAdd.hAdd (α := ℤ) (-1) 1 ≠ 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ HAdd.hAdd (α := ℤ) (-1) 1 ≠ -1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ HAdd.hAdd (α := ℤ) (-1) (-1) ≠ 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ HAdd.hAdd (α := ℤ) (-1) (-1) ≠ -1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ 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
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
tfae_3_iff_1 : FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremFor n
⊢ [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.NumberTheory.FLT.Basic
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 ∈ s

Tactic:
simp [s]
-- Module: Mathlib.NumberTheory.FLT.Basic
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
obtain : ∀ (A : R) (hA : a = d * A), False
⊢ False

Tactic:
obtain ⟨A, hA⟩ : d ∣ a := gcd_dvd (by simp [s])

Premises used: Finset.gcd_dvd
-- Module: Mathlib.NumberTheory.FLT.Basic
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 ∈ s

Tactic:
simp [s]
-- Module: Mathlib.NumberTheory.FLT.Basic
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
obtain : ∀ (B : R) (hB : b = d * B), False
⊢ False

Tactic:
obtain ⟨B, hB⟩ : d ∣ b := gcd_dvd (by simp [s])

Premises used: Finset.gcd_dvd