awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
bd : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X])
cd : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch : (a : k[X]) → k[X]) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch : (a : k[X]) → k[X]) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch : (a : k[X]) → k[X]) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
heq :
  Eq (α := k[X])
    ((expand k ch : (a : k[X]) → k[X])
        (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (ca ^ p) +
            HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (cb ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (cc ^ r)) :
      k[X])
    (0 : k[X])
⊢ HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (ca ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (cb ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (cc ^ r) =
    0
have rwa : ∀
  (heq :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (ca ^ p) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (cb ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (cc ^ r) =
      0),
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (ca ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (cb ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (cc ^ r) =
    0
Tactic: rwa [Polynomial.expand_eq_zero (zero_lt_iff.mpr chn0)] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
chn0 : ringChar k ≠ 0
d : ℕ
eq_d : a.natDegree = d
⊢ d = 0
have inr : ∀ {a b c : k[X]}
  (heq :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
      0)
  (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (eq_d : a.natDegree = 0), Eq (α := ℕ) 0 0
Tactic: induction d
      using Nat.case_strong_induction_on
      generalizing a b c ha hb hc hab heq with
    | hz => rfl
    | hi d ih_d => -- have derivatives of `a, b, c` zero
      obtain ⟨ad, bd, cd⟩ := flt_catalan_deriv
        hp hq hr hineq chp chq chr ha hb hc hab hu hv hw heq
      -- find contracts `ca, cb, cc` so that `a(k) = ca(k^ch)`
      obtain ⟨ca, ca_nz, eq_a, eq_deg_a⟩ := find_contract ha ad chn0
      obtain ⟨cb, cb_nz, eq_b, eq_deg_b⟩ := find_contract hb bd chn0
      obtain ⟨cc, cc_nz, eq_c, eq_deg_c⟩ := find_contract hc cd chn0
      set ch := ringChar k
      suffices hca : ca.natDegree = 0 by
        rw [← eq_d, eq_deg_a, hca, zero_mul]
      by_contra hnca; apply hnca
      apply ih_d _ _ _ ca_nz cb_nz cc_nz <;> clear ih_d <;> try rfl
      · apply (isCoprime_expand chn0).mp
        rwa [← eq_a, ← eq_b]
      · have _ : ch ≠ 1 := CharP.ringChar_ne_one
        have hch2 : 2 ≤ ch := by lia
        rw [← add_le_add_iff_right 1, ← eq_d, eq_deg_a]
        grw [← hch2]
        lia
      · rw [eq_a, eq_b, eq_c, ← expand_C ch u, ← expand_C ch v, ← expand_C ch w] at heq
        simp_rw [← map_pow, ← map_mul, ← map_add] at heq
        rwa [Polynomial.expand_eq_zero (zero_lt_iff.mpr chn0)] at heq
Cleared hypotheses: a, b, c, heq, ha, hb, hc, hab, d, eq_d
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
chn0 : ringChar k ≠ 0
d : ℕ
eq_d : a.natDegree = d
inr :
  ∀ {a b c : k[X]}
    (heq :
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
            HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
        0)
    (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (eq_d : a.natDegree = 0), Eq (α := ℕ) 0 0
⊢ d = 0
have inr₁ : ∀ (d : ℕ)
  (ih_d :
    ∀ m ≤ d,
      ∀ {a b c : k[X]}
        (heq :
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
                HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
              HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
            0)
        (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (eq_d : a.natDegree = m), m = 0)
  {a b c : k[X]}
  (heq :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
      0)
  (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (eq_d : a.natDegree = d + 1), d + 1 = 0
Tactic: induction d
      using Nat.case_strong_induction_on
      generalizing a b c ha hb hc hab heq with
    | hz => rfl
    | hi d ih_d => -- have derivatives of `a, b, c` zero
      obtain ⟨ad, bd, cd⟩ := flt_catalan_deriv
        hp hq hr hineq chp chq chr ha hb hc hab hu hv hw heq
      -- find contracts `ca, cb, cc` so that `a(k) = ca(k^ch)`
      obtain ⟨ca, ca_nz, eq_a, eq_deg_a⟩ := find_contract ha ad chn0
      obtain ⟨cb, cb_nz, eq_b, eq_deg_b⟩ := find_contract hb bd chn0
      obtain ⟨cc, cc_nz, eq_c, eq_deg_c⟩ := find_contract hc cd chn0
      set ch := ringChar k
      suffices hca : ca.natDegree = 0 by
        rw [← eq_d, eq_deg_a, hca, zero_mul]
      by_contra hnca; apply hnca
      apply ih_d _ _ _ ca_nz cb_nz cc_nz <;> clear ih_d <;> try rfl
      · apply (isCoprime_expand chn0).mp
        rwa [← eq_a, ← eq_b]
      · have _ : ch ≠ 1 := CharP.ringChar_ne_one
        have hch2 : 2 ≤ ch := by lia
        rw [← add_le_add_iff_right 1, ← eq_d, eq_deg_a]
        grw [← hch2]
        lia
      · rw [eq_a, eq_b, eq_c, ← expand_C ch u, ← expand_C ch v, ← expand_C ch w] at heq
        simp_rw [← map_pow, ← map_mul, ← map_add] at heq
        rwa [Polynomial.expand_eq_zero (zero_lt_iff.mpr chn0)] at heq
Cleared hypotheses: a, b, c, heq, ha, hb, hc, hab, d, eq_d
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have hbc : IsCoprime b c
Tactic: have hbc : IsCoprime b c := by
    apply rot_coprime heq hab <;> assumption
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hbc : IsCoprime b c
⊢ HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
have rwa : ∀
  (heq :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
      0)
  (hbc : IsCoprime b c),
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
Tactic: rwa [add_rotate] at heq
Cleared hypotheses: heq, hbc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hbc : IsCoprime b c
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have heq' : HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
  0
Tactic: have heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0 := by
    rwa [add_rotate] at heq
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hbc : IsCoprime b c
heq' :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have hca : IsCoprime c a
Tactic: have hca : IsCoprime c a := by
    apply rot_coprime heq' hbc <;> assumption
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hbc : IsCoprime b c
heq' :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have refine_1 : a.natDegree = 0
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hbc : IsCoprime b c
heq' :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
refine_1 : a.natDegree = 0
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have refine_2 : b.natDegree = 0
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hbc : IsCoprime b c
heq' :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
refine_1 : a.natDegree = 0
refine_2 : b.natDegree = 0
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have refine_3 : c.natDegree = 0
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hbc : IsCoprime b c
heq' :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ b.natDegree = 0
have refine_2 : ∀ (hineq : r * p + p * q + q * r ≤ p * q * r) (chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0)
  (chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0) (chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0) {a b c : k[X]} (ha : a ≠ 0)
  (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0)
  (heq :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
      0)
  (hbc : IsCoprime b c)
  (heq' :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
      0)
  (hca : IsCoprime c a), b.natDegree = 0
Tactic: rw [add_rotate] at heq hineq
Cleared hypotheses: hineq, chp, chq, chr, a, b, c, ha, hb, hc, hab, u, v, w, hu, hv, hw, heq, hbc, heq', hca
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : r * p + p * q + q * r ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hbc : IsCoprime b c
heq' :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ b.natDegree = 0
have refine_2 : ∀ (hineq : r * p + p * q + q * r ≤ q * r * p) (chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0)
  (chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0) (chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0) {a b c : k[X]} (ha : a ≠ 0)
  (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0)
  (heq :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
      0)
  (hbc : IsCoprime b c)
  (heq' :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
      0)
  (hca : IsCoprime c a), b.natDegree = 0
Tactic: rw [mul_rotate] at hineq
Cleared hypotheses: hineq, chp, chq, chr, a, b, c, ha, hb, hc, hab, u, v, w, hu, hv, hw, heq, hbc, heq', hca
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) =
    0
hbc : IsCoprime b c
heq' :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ c.natDegree = 0
have refine_3 : ∀ (hineq : p * q + q * r + r * p ≤ p * q * r) (chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0)
  (chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0) (chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0) {a b c : k[X]} (ha : a ≠ 0)
  (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0)
  (heq :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
      0)
  (hbc : IsCoprime b c)
  (heq' :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
      0)
  (hca : IsCoprime c a), c.natDegree = 0
Tactic: rw [← add_rotate] at heq hineq
Cleared hypotheses: hineq, chp, chq, chr, a, b, c, ha, hb, hc, hab, u, v, w, hu, hv, hw, heq, hbc, heq', hca
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : p * q + q * r + r * p ≤ p * q * r
chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0
chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0
chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
    0
hbc : IsCoprime b c
heq' :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
      HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
    0
hca : IsCoprime c a
⊢ c.natDegree = 0
have refine_3 : ∀ (hineq : p * q + q * r + r * p ≤ r * p * q) (chp : Ne.{u_1 + 1} (α := k) (↑p : k) 0)
  (chq : Ne.{u_1 + 1} (α := k) (↑q : k) 0) (chr : Ne.{u_1 + 1} (α := k) (↑r : k) 0) {a b c : k[X]} (ha : a ≠ 0)
  (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0)
  (heq :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
      0)
  (hbc : IsCoprime b c)
  (heq' :
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) +
          HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) w : k[X]) (c ^ r) +
        HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) u : k[X]) (a ^ p) =
      0)
  (hca : IsCoprime c a), c.natDegree = 0
Tactic: rw [← mul_rotate] at hineq
Cleared hypotheses: hineq, chp, chq, chr, a, b, c, ha, hb, hc, hab, u, v, w, hu, hv, hw, heq, hbc, heq', hca
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : a ^ n + b ^ n = c ^ n
⊢ 0 < n
have linarith : n ≤ 0 → HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 3 (↑n : ℤ) + HSub.hSub (α := ℤ) (↑n : ℤ) 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : a ^ n + b ^ n = c ^ n
linarith : n ≤ 0 → HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 3 (↑n : ℤ) + HSub.hSub (α := ℤ) (↑n : ℤ) 0 = 0
⊢ 0 < n
have linarith₁ : n ≤ 0 → GT.gt (α := ℤ) 3 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : a ^ n + b ^ n = c ^ n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have hn' : 0 < n
Tactic: have hn' : 0 < n := by linarith
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : a ^ n + b ^ n = c ^ n
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have heq₁ : 1 * a ^ n + 1 * b ^ n + -1 * c ^ n = 0
Tactic: rw [← sub_eq_zero, ← one_mul (a ^ n), ← one_mul (b ^ n), ← one_mul (c ^ n), sub_eq_add_neg,
    ← neg_mul] at heq
Cleared hypotheses: heq, hn'