awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
inr : Eq (α := ℤ) (↑(a.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(c.natAbs ^ n) : ℤ)
⊢ False

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

Premises used: Int.natAbs, Iff.mp, Int.natCast_inj
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
inr : |a| ^ n + |b| ^ n = |c| ^ n
⊢ Eq (α := ℤ) (↑(a.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(c.natAbs ^ n) : ℤ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ |a| ^ n + |b| ^ n = |c| ^ n

Tactic:
simp only [abs_of_neg, neg_pow a, neg_pow b, neg_pow c, ← mul_add, *]

Premises used: abs_of_neg, neg_pow, mul_add
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : 0 < c
⊢ 0 < c ^ n

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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_gt <| habc.symm.trans_lt <| add_neg (hn.pow_neg ha) <|
        hn.pow_neg hb

Premises used: add_neg, Eq.trans_lt, LT.lt.not_gt, Odd.pow_neg, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ b.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ a.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
inr : Eq (α := ℤ) (↑(b.natAbs ^ n + c.natAbs ^ n) : ℤ) (↑(a.natAbs ^ n) : ℤ)
⊢ False

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

Premises used: Int.natAbs, Iff.mp, Int.natCast_inj
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
inr : |b| ^ n + |c| ^ n = |a| ^ n
⊢ Eq (α := ℤ) (↑(b.natAbs ^ n + c.natAbs ^ n) : ℤ) (↑(a.natAbs ^ n) : ℤ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ |b| ^ n + |c| ^ n = |a| ^ n

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

Premises used: Odd.neg_pow, abs_of_neg, eq_neg_add_iff_add_eq, abs_of_pos, add_neg_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ a.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
inr : Eq (α := ℤ) (↑(a.natAbs ^ n + c.natAbs ^ n) : ℤ) (↑(b.natAbs ^ n) : ℤ)
⊢ False

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

Premises used: Int.natAbs, Iff.mp, Int.natCast_inj
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
inr : |a| ^ n + |c| ^ n = |b| ^ n
⊢ Eq (α := ℤ) (↑(a.natAbs ^ n + c.natAbs ^ n) : ℤ) (↑(b.natAbs ^ n) : ℤ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ |a| ^ n + |c| ^ n = |b| ^ n

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

Premises used: Odd.neg_pow, abs_of_neg, neg_add_eq_iff_eq_add, abs_of_pos
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
⊢ c.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
⊢ a.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
inr : Eq (α := ℤ) (↑(c.natAbs ^ n + a.natAbs ^ n) : ℤ) (↑(b.natAbs ^ n) : ℤ)
⊢ False

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

Premises used: Int.natAbs, Iff.mp, Int.natCast_inj
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
inr : |c| ^ n + |a| ^ n = |b| ^ n
⊢ Eq (α := ℤ) (↑(c.natAbs ^ n + a.natAbs ^ n) : ℤ) (↑(b.natAbs ^ n) : ℤ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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, neg_add_eq_iff_eq_add,
        eq_add_neg_iff_add_eq, *]

Premises used: Odd.neg_pow, abs_of_neg, neg_add_eq_iff_eq_add, abs_of_pos, eq_add_neg_iff_add_eq
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ b.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
inr : Eq (α := ℤ) (↑(c.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(a.natAbs ^ n) : ℤ)
⊢ False

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

Premises used: Int.natAbs, Iff.mp, Int.natCast_inj
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
inr : |c| ^ n + |b| ^ n = |a| ^ n
⊢ Eq (α := ℤ) (↑(c.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(a.natAbs ^ n) : ℤ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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, add_neg_eq_iff_eq_add,
        *]

Premises used: Odd.neg_pow, abs_of_neg, abs_of_pos, add_neg_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : c < 0
⊢ 0 < a ^ n + b ^ n

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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_gt <| habc.trans_lt <| hn.pow_neg hc

Premises used: Eq.trans_lt, LT.lt.not_gt, Odd.pow_neg
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ b.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ c.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
inr : Eq (α := ℤ) (↑(a.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(c.natAbs ^ n) : ℤ)
⊢ False

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

Premises used: Int.natAbs, Iff.mp, Int.natCast_inj
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
inr : |a| ^ n + |b| ^ n = |c| ^ n
⊢ Eq (α := ℤ) (↑(a.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(c.natAbs ^ n) : ℤ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : 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

Tactic:
simp only [abs_of_pos, *]

Premises used: abs_of_pos
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n

Tactic:
tfae_have 1 → 2
  | h, a, b, c, ha, hb, hc, habc => by
    obtain hn | hn := n.even_or_odd
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [hn.pow_abs, habc]
    obtain ha | ha := ha.lt_or_gt <;> obtain hb | hb := hb.lt_or_gt <;>
      obtain hc | hc := hc.lt_or_gt
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_neg, neg_pow a, neg_pow b, neg_pow c, ← mul_add, *]
    · exact (by positivity : 0 < c ^ n).not_gt <| habc.symm.trans_lt <| add_neg (hn.pow_neg ha) <|
        hn.pow_neg hb
    · refine h b.natAbs c.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add,
        eq_neg_add_iff_add_eq, *]
    · refine h a.natAbs c.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add,
        *]
    · refine h c.natAbs a.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add,
        eq_add_neg_iff_add_eq, *]
    · refine h c.natAbs b.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add,
        *]
    · exact (by positivity : 0 < a ^ n + b ^ n).not_gt <| habc.trans_lt <| hn.pow_neg hc
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, *]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ 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 : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ 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_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
⊢ ∀ (a : FermatLastTheoremWith ℤ n), FermatLastTheoremWith ℚ n

Tactic:
2 → 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_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ a.num ≠ 0

Tactic:
rw [← Rat.num_ne_zero] at ha hb hc

Premises used: Rat.num_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
ha₁ : a.num ≠ 0
⊢ b.num ≠ 0

Tactic:
rw [← Rat.num_ne_zero] at ha hb hc

Premises used: Rat.num_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
ha₁ : a.num ≠ 0
hb₁ : b.num ≠ 0
⊢ c.num ≠ 0

Tactic:
rw [← Rat.num_ne_zero] at ha hb hc

Premises used: Rat.num_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
ha₁ : a.num ≠ 0
hb₁ : b.num ≠ 0
hc₁ : c.num ≠ 0
⊢ a ^ n + b ^ n = c ^ n

Tactic:
rw [← Rat.num_ne_zero] at ha hb hc

Premises used: Rat.num_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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 : ℤ) ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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.num * (↑c.den : ℤ) ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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
⊢ HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑b.den : ℤ) * c.num ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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
refine :
  (a.num * (↑b.den : ℤ) * (↑c.den : ℤ)) ^ n + ((↑a.den : ℤ) * b.num * (↑c.den : ℤ)) ^ n =
    (HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑b.den : ℤ) * c.num) ^ n
⊢ False

Tactic:
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) ?_

Premises used: Rat.num, HMul.hMul, Rat.den, Nat.cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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
⊢ (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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
⊢ (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0

Tactic:
have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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 : (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0
⊢ (a.num * (↑b.den : ℤ) * (↑c.den : ℤ)) ^ n + ((↑a.den : ℤ) * b.num * (↑c.den : ℤ)) ^ n =
    (HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑b.den : ℤ) * c.num) ^ n

Tactic:
Int.cast_injective <| (div_left_inj' this).1 ?_

Premises used: Iff.mp, div_left_inj', Int.cast_injective
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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 : (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0
refine :
  (↑((a.num * (↑b.den : ℤ) * (↑c.den : ℤ)) ^ n + ((↑a.den : ℤ) * b.num * (↑c.den : ℤ)) ^ n) : ℚ) /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n =
    (↑((HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑b.den : ℤ) * c.num) ^ n) : ℚ) /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n
⊢ (a.num * (↑b.den : ℤ) * (↑c.den : ℤ)) ^ n + ((↑a.den : ℤ) * b.num * (↑c.den : ℤ)) ^ n =
    (HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑b.den : ℤ) * c.num) ^ n

Tactic:
refine Int.cast_injective <| (div_left_inj' this).1 ?_

Premises used: Iff.mp, div_left_inj', Int.cast_injective
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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 : (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0
push_cast :
  ((HMul.hMul (α := ℚ) (↑a.num : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n +
        (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.num : ℚ) * (↑c.den : ℚ)) ^ n) /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n =
    (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.num : ℚ)) ^ n /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n
⊢ (↑((a.num * (↑b.den : ℤ) * (↑c.den : ℤ)) ^ n + ((↑a.den : ℤ) * b.num * (↑c.den : ℤ)) ^ n) : ℚ) /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n =
    (↑((HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑b.den : ℤ) * c.num) ^ n) : ℚ) /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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 : (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0
⊢ Ne (α := ℚ) (↑a.den : ℚ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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 : (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0
⊢ Ne (α := ℚ) (↑b.den : ℚ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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 : (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0
⊢ Ne (α := ℚ) (↑c.den : ℚ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : 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 : (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0
⊢ ((HMul.hMul (α := ℚ) (↑a.num : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n +
        (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.num : ℚ) * (↑c.den : ℚ)) ^ n) /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n =
    (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.num : ℚ)) ^ n /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n

Tactic:
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]

Premises used: Rat.num_div_den, div_pow, mul_div_mul_comm, mul_one, one_mul, div_self, add_div
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
⊢ ∀ (a : FermatLastTheoremWith ℤ n), FermatLastTheoremWith ℚ n

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]
-- 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:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false