awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ False
have inr : Eq (α := ℤ) (↑(c.natAbs ^ n + a.natAbs ^ n) : ℤ) (↑(b.natAbs ^ n) : ℤ)
Tactic: refine h c.natAbs a.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ Eq (α := ℤ) (↑(c.natAbs ^ n + a.natAbs ^ n) : ℤ) (↑(b.natAbs ^ n) : ℤ)
have inr : |c| ^ n + |a| ^ n = |b| ^ n
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ False
have inr : Eq (α := ℤ) (↑(c.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(a.natAbs ^ n) : ℤ)
Tactic: refine h c.natAbs b.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ Eq (α := ℤ) (↑(c.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(a.natAbs ^ n) : ℤ)
have inr : |c| ^ n + |b| ^ n = |a| ^ n
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ False
have inr : Eq (α := ℤ) (↑(a.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(c.natAbs ^ n) : ℤ)
Tactic: refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ Eq (α := ℤ) (↑(a.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(c.natAbs ^ n) : ℤ)
have inr : |a| ^ n + |b| ^ n = |c| ^ n
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE
have tfae_1_to_2 : ∀ (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, *]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
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
⊢ False
have ha₁ : a.num ≠ 0
Tactic: rw [← Rat.num_ne_zero] at ha hb hc
Cleared hypotheses: ha, hb, hc, habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
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
⊢ False
have hb₁ : b.num ≠ 0
Tactic: rw [← Rat.num_ne_zero] at ha hb hc
Cleared hypotheses: ha, hb, hc, habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
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
⊢ False
have hc₁ : c.num ≠ 0
Tactic: rw [← Rat.num_ne_zero] at ha hb hc
Cleared hypotheses: ha, hb, hc, habc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ False
have refine : (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 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) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
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 : ℤ)) ^ n + ((↑a.den : ℤ) * b.num * (↑c.den : ℤ)) ^ n =
    (HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑b.den : ℤ) * c.num) ^ n
have this : (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n ≠ 0
Tactic: have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
have 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
Tactic: refine Int.cast_injective <| (div_left_inj' this).1 ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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.den : ℚ)) ^ n =
    (↑((HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑b.den : ℤ) * c.num) ^ n) : ℚ) /
      (HMul.hMul (α := ℚ) (↑a.den : ℚ) (↑b.den : ℚ) * (↑c.den : ℚ)) ^ n
have 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
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE
have tfae_2_to_3 : ∀ (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]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
tfae_1_to_2 : ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n
tfae_2_to_3 : ∀ (a : FermatLastTheoremWith ℤ n), FermatLastTheoremWith ℚ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE
have tfae_3_to_1 : ∀ (a : FermatLastTheoremWith ℚ n), FermatLastTheoremWith ℕ n
Tactic: tfae_have 3 → 1
  | h, a, b, c => mod_cast h a b c
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ ∃ (d : R) (a' : R) (b' : R) (c' : R), (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ False
have 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
Tactic: rcases h a b c ha hb hc heq with ⟨d, a', b', c', ⟨rfl, rfl, rfl⟩, ⟨ua, ub, uc⟩⟩
Cleared hypotheses: a, b, c, ha, hb, hc, heq
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
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'
⊢ False
have heq₁ : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
Tactic: rw [mul_pow, mul_pow, mul_pow, ← add_mul] at heq
Cleared hypotheses: heq, ua, ub, uc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
⊢ FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
have hn : ∀ (a b c : ℕ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
Tactic: apply fermatLastTheoremWith'_iff_fermatLastTheoremWith
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
⊢ ∀ (a b c : ℕ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
have hn : ∀ (a b c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n
Tactic: simp only [Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n a b c : ℕ
ha : a = 1
hb : b = 1
hc : c = 1
⊢ a ^ n + b ^ n ≠ c ^ n
have hn : HPow.hPow (α := ℕ) 1 n + HPow.hPow (α := ℕ) 1 n ≠ HPow.hPow (α := ℕ) 1 n
Tactic: rw [ha, hb, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
Goal:
n : ℕ
⊢ [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n].TFAE
have tfae_2_iff_1 : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremFor n
have rw : FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremWith ℤ n
Tactic: rw [fermatLastTheoremFor_iff_int]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
⊢ FermatLastTheoremWith' ℤ n ↔ FermatLastTheoremWith ℤ n
have hn : ∀ (a b c : ℤ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
Tactic: apply fermatLastTheoremWith'_iff_fermatLastTheoremWith
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
Goal:
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
have pos : ∀ (hn : n = 0), a ^ n + b ^ n ≠ c ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : ∀ (hn : ¬n = 0), a ^ n + b ^ n ≠ c ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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 + b ^ n ≠ c ^ n
have pos : ∀ (tfae_2_iff_1 : FermatLastTheoremWith' ℕ 0 ↔ FermatLastTheoremFor 0),
  HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 ≠ HPow.hPow (β := ℕ) c 0
Tactic: subst hn
Cleared hypotheses: n, tfae_2_iff_1, hn
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
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 + b ^ n ≠ c ^ n
have ha₁ : a ^ n = 1 ∨ a ^ n = -1
Tactic: rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc
Cleared hypotheses: ha, hb, hc, hn
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have hb₁ : b ^ n = 1 ∨ b ^ n = -1
Tactic: rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc
Cleared hypotheses: ha, hb, hc, hn
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (hypothesis)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have hc₁ : c ^ n = 1 ∨ c ^ n = -1
Tactic: rw [← isUnit_pow_iff hn, Int.isUnit_iff] at ha hb hc
Cleared hypotheses: ha, hb, hc, hn
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : ∀ (ha : a ^ n = 1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases ha with ha | ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg₁ : ∀ (ha : a ^ n = -1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases ha with ha | ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : ∀ (hb : b ^ n = 1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg₁ : ∀ (hb : b ^ n = -1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : ∀ (hb : b ^ n = 1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg₁ : ∀ (hb : b ^ n = -1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : ∀ (hc : c ^ n = 1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg₁ : ∀ (hc : c ^ n = -1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : ∀ (hc : c ^ n = 1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg₁ : ∀ (hc : c ^ n = -1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : ∀ (hc : c ^ n = 1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg₁ : ∀ (hc : c ^ n = -1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : ∀ (hc : c ^ n = 1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg₁ : ∀ (hc : c ^ n = -1), a ^ n + b ^ n ≠ c ^ n
Tactic: rcases hc with hc | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : HAdd.hAdd (α := ℤ) 1 1 ≠ 1
Tactic: rw [ha, hb, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : HAdd.hAdd (α := ℤ) 1 1 ≠ -1
Tactic: rw [ha, hb, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : HAdd.hAdd (α := ℤ) 1 (-1) ≠ 1
Tactic: rw [ha, hb, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : HAdd.hAdd (α := ℤ) 1 (-1) ≠ -1
Tactic: rw [ha, hb, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : HAdd.hAdd (α := ℤ) (-1) 1 ≠ 1
Tactic: rw [ha, hb, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : HAdd.hAdd (α := ℤ) (-1) 1 ≠ -1
Tactic: rw [ha, hb, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : HAdd.hAdd (α := ℤ) (-1) (-1) ≠ 1
Tactic: rw [ha, hb, hc]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Basic (goal)
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
⊢ a ^ n + b ^ n ≠ c ^ n
have neg : HAdd.hAdd (α := ℤ) (-1) (-1) ≠ -1
Tactic: rw [ha, hb, hc]