-- Mathlib/NumberTheory/FLT/Basic.lean
lemma fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) :
    TFAE [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n]

Proof state:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ b.natAbs ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inr.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ |c| ^ n + |b| ^ n = |a| ^ n

Tactic:
simp only [abs_of_pos, abs_of_neg, hn.neg_pow, habc, add_neg_eq_iff_eq_add,
  eq_add_neg_iff_add_eq, *]

Result:
no goals

Proof state:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
⊢ b.natAbs ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ c.natAbs ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ ↑c.den ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inl.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : 0 < c
⊢ False

Tactic:
exact (by positivity : 0 < c ^ n).not_lt <| habc.symm.trans_lt <| add_neg (hn.pow_neg ha) <|
  hn.pow_neg hb

Result:
no goals

Proof state:
case inr.inr.inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : c < 0
⊢ False

Tactic:
exact (by positivity : 0 < a ^ n + b ^ n).not_lt <| habc.trans_lt <| hn.pow_neg hc

Result:
no goals

Proof state:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ a.natAbs ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
tfae_2_to_3 : FermatLastTheoremWith ℤ n → FermatLastTheoremWith ℚ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Tactic:
tfae_have 3 → 1
| h, a, b, c => mod_cast h a b c

Result:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
tfae_2_to_3 : FermatLastTheoremWith ℤ n → FermatLastTheoremWith ℚ n
tfae_3_to_1 : FermatLastTheoremWith ℚ n → FermatLastTheoremWith ℕ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Proof state:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Tactic:
tfae_have 2 → 3
| h, a, b, c, ha, hb, hc, habc => by
  rw [← Rat.num_ne_zero] at ha hb hc
  refine h (a.num * b.den * c.den) (a.den * b.num * c.den) (a.den * b.den * c.num)
    (by positivity) (by positivity) (by positivity) ?_
  have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity
  refine Int.cast_injective <| (div_left_inj' this).1 ?_
  push_cast
  simp only [add_div, ← div_pow, mul_div_mul_comm, div_self (by positivity : (a.den : ℚ) ≠ 0),
    div_self (by positivity : (b.den : ℚ) ≠ 0), div_self (by positivity : (c.den : ℚ) ≠ 0),
    one_mul, mul_one, Rat.num_div_den, habc]

Result:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
tfae_2_to_3 : FermatLastTheoremWith ℤ n → FermatLastTheoremWith ℚ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Proof state:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ ↑a.den * ↑b.den * c.num ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inr.inl.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
⊢ |c| ^ n + |a| ^ n = |b| ^ n

Tactic:
simp only [abs_of_pos, abs_of_neg, hn.neg_pow, habc, neg_add_eq_iff_eq_add,
  eq_add_neg_iff_add_eq, *]

Result:
no goals

Proof state:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ c.natAbs ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ False

Tactic:
refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
  (Int.natCast_inj.1 ?_)

Result:
case inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)

Proof state:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ (a.num * ↑b.den * ↑c.den) ^ n + (↑a.den * b.num * ↑c.den) ^ n = (↑a.den * ↑b.den * c.num) ^ n

Tactic:
have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity

Result:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ (a.num * ↑b.den * ↑c.den) ^ n + (↑a.den * b.num * ↑c.den) ^ n = (↑a.den * ↑b.den * c.num) ^ n

Proof state:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ c.natAbs ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inr.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)

Tactic:
push_cast

Result:
case inr.inr.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ |a| ^ n + |b| ^ n = |c| ^ n

Proof state:
case inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ |a| ^ n + |b| ^ n = |c| ^ n

Tactic:
simp only [hn.pow_abs, habc]

Result:
no goals

Proof state:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ c.natAbs ≠ 0

Tactic:
positivity

Result:
no goals