-- Mathlib/NumberTheory/FLT/Basic.lean
lemma fermatLastTheoremWith'_nat_int_tfae (n : ℕ) :
    TFAE [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n]

Proof state:
case pos
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
tfae_2_iff_1 : FermatLastTheoremWith' ℕ 0 ↔ FermatLastTheoremFor 0
⊢ a ^ 0 + b ^ 0 ≠ c ^ 0

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

Result:
no goals

Proof state:
case neg
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
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases ha with ha | ha <;> rcases hb with hb | hb <;> rcases hc with hc | hc <;>
  rw [ha, hb, hc] <;> decide

Result:
no goals

Proof state:
case hn
n : ℕ
⊢ ∀ (a b c : ℕ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n

Tactic:
simp only [Nat.isUnit_iff]

Result:
case hn
n : ℕ
⊢ ∀ (a b c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n

Proof state:
case hn
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ ∀ (a b c : ℤ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n

Tactic:
intro a b c ha hb hc

Result:
case hn
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
⊢ a ^ n + b ^ n ≠ c ^ n

Proof state:
case neg
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 + b ^ n ≠ c ^ n

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

Result:
case neg
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
⊢ a ^ n + b ^ n ≠ c ^ n

Proof state:
case hn
n : ℕ
⊢ ∀ (a b c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n

Tactic:
intro _ _ _ ha hb hc

Result:
case hn
n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ a✝ ^ n + b✝ ^ n ≠ c✝ ^ n

Proof state:
case hn
n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ a✝ ^ n + b✝ ^ n ≠ c✝ ^ n

Tactic:
rw [ha, hb, hc]

Result:
case hn
n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ 1 ^ n + 1 ^ n ≠ 1 ^ n

Proof state:
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

Result:
no goals

Proof state:
n : ℕ
⊢ [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n].TFAE

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]

Result:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n].TFAE

Proof state:
case hn
n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ 1 ^ n + 1 ^ n ≠ 1 ^ n

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

Result:
no goals

Proof state:
case hn
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
by_cases hn : n = 0

Result:
case pos
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 + b ^ n ≠ c ^ n

case neg
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 + b ^ n ≠ c ^ n

Proof state:
case pos
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 + b ^ n ≠ c ^ n

Tactic:
subst hn

Result:
case pos
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
tfae_2_iff_1 : FermatLastTheoremWith' ℕ 0 ↔ FermatLastTheoremFor 0
⊢ a ^ 0 + b ^ 0 ≠ c ^ 0

Proof state:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremWith ℤ n

Tactic:
apply fermatLastTheoremWith'_iff_fermatLastTheoremWith

Result:
case hn
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ ∀ (a b c : ℤ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n

Proof state:
n : ℕ
⊢ FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n

Tactic:
apply fermatLastTheoremWith'_iff_fermatLastTheoremWith

Result:
case hn
n : ℕ
⊢ ∀ (a b c : ℕ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n

Proof state:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremFor n

Tactic:
rw [fermatLastTheoremFor_iff_int]

Result:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremWith ℤ n