awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
pos :
  ∀ (hw : w = 0),
    a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
        b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
          Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
have neg : ∀ (hw : ¬w = 0),
  a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
Tactic: by_cases hw : w = 0
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
have pos : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
  Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
have wab₁ : 0 = a.wronskian b
Tactic: rw [hw] at wab wbc
Cleared hypotheses: wab, hbc, hsum', hca, wbc, wca, abc_dr_dvd_w, hw
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
wab₁ : 0 = a.wronskian b
hbc₁ : IsCoprime b c
hsum'₁ : b + c + a = 0
hca₁ : IsCoprime c a
⊢ Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
have wbc₁ : 0 = b.wronskian c
Tactic: rw [hw] at wab wbc
Cleared hypotheses: wab, hbc, hsum', hca, wbc, wca, abc_dr_dvd_w, hw
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : 0 = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : 0 = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
have ga : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
Tactic: obtain ⟨ga, gb⟩ := hab.wronskian_eq_zero_iff.mp wab.symm
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : 0 = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : 0 = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
ga : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
⊢ Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
have gb : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X])
Tactic: obtain ⟨ga, gb⟩ := hab.wronskian_eq_zero_iff.mp wab.symm
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : 0 = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : 0 = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
ga : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X])
gb left : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X])
⊢ Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
have gc : Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
Tactic: obtain ⟨_, gc⟩ := hbc.wronskian_eq_zero_iff.mp wbc.symm
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) a : k[X]) (0 : k[X]) ∧
      Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) b : k[X]) (0 : k[X]) ∧
        Eq (α := k[X]) ((derivative : (a : k[X]) → k[X]) c : k[X]) (0 : k[X])
have neg : a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
  b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have neg : a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
neg : a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have neg₁ : b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
neg : a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
neg₁ : b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have neg₂ : c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have neg : ∀ (abc_dr_dvd_w : divRadical (b * c * a) ∣ w) (hw : ¬w = 0), a.natDegree + 1 ≤ (radical (b * c * a)).natDegree
Tactic: rw [mul_rotate] at abc_dr_dvd_w ⊢
Cleared hypotheses: abc_dr_dvd_w, hw
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (b * c * a) ∣ w
hw : ¬w = 0
neg : b ≠ 0
neg₁ : c ≠ 0
neg₂ : a ≠ 0
neg₃ : divRadical (b * c * a) ∣ w
⊢ a.natDegree + 1 ≤ (radical (b * c * a)).natDegree
have apply : w ≠ 0
Tactic: apply abc_subcall wbc
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have neg : ∀ (abc_dr_dvd_w : divRadical (c * a * b) ∣ w) (hw : ¬w = 0), b.natDegree + 1 ≤ (radical (c * a * b)).natDegree
Tactic: rw [← mul_rotate] at abc_dr_dvd_w ⊢
Cleared hypotheses: abc_dr_dvd_w, hw
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (c * a * b) ∣ w
hw : ¬w = 0
neg : c ≠ 0
neg₁ : a ≠ 0
neg₂ : b ≠ 0
neg₃ : divRadical (c * a * b) ∣ w
⊢ b.natDegree + 1 ≤ (radical (c * a * b)).natDegree
have apply : w ≠ 0
Tactic: apply abc_subcall wca
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.MasonStothers (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
neg : a ≠ 0
neg₁ : b ≠ 0
neg₂ : c ≠ 0
neg₃ : divRadical (a * b * c) ∣ w
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
have apply : w ≠ 0
Tactic: apply abc_subcall wab
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab : IsCoprime a b
⊢ IsCoprime b c
have hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
Tactic: have hCu : IsUnit (C u) := hu.isUnit_C
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
⊢ IsCoprime b c
have hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
Tactic: have hCv : IsUnit (C v) := hv.isUnit_C
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
⊢ IsCoprime b c
have hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
Tactic: have hCw : IsUnit (C w) := hw.isUnit_C
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab : IsCoprime a b
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
⊢ IsCoprime b c
have hab₁ : IsCoprime (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))
Tactic: rw [← IsCoprime.pow_iff hp.bot_lt hq.bot_lt, ← isCoprime_mul_units_left hCu hCv] at hab
Cleared hypotheses: hab, hCu, hCv, hCw
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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
hab :
  IsCoprime (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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
⊢ IsCoprime b c
have 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)
Tactic: rw [add_eq_zero_iff_neg_eq] at heq
Cleared hypotheses: heq, hab, hCu, hCv, hCw
-- 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
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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)
hab :
  IsCoprime (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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
⊢ IsCoprime b c
have rw : IsCoprime (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q))
  (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))
Tactic: rw [← IsCoprime.pow_iff hq.bot_lt hr.bot_lt, ← isCoprime_mul_units_left hCv hCw,
    ← heq, IsCoprime.neg_right_iff]
-- 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
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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)
hab :
  IsCoprime (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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
⊢ IsCoprime (HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q))
    (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))
have h : HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) * 1
Tactic: convert! IsCoprime.add_mul_left_right hab.symm 1 using 2
-- 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
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
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)
hab :
  IsCoprime (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))
hCu : IsUnit (M := k[X]) ((C : (a : k) → k[X]) u : k[X])
hCv : IsUnit (M := k[X]) ((C : (a : k) → k[X]) v : k[X])
hCw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) w : k[X])
⊢ HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) * 1
have h : HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q) =
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) v : k[X]) (b ^ q)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ False
have suffices : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)
Tactic: suffices h : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c) by simp at h
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) <
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)
have h₁ : 0 < q * r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
h₁ : 0 < q * r
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) <
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)
have h₂ : 0 < r * p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
h₁ : 0 < q * r
h₂ : 0 < r * p
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) <
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)
have h₃ : 0 < p * q
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)
have _ : p * q * r * (a + b + c) + 1 = p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1
Tactic: calc
    _ = (p * a) * (q * r) + (q * b) * (r * p) + (r * c) * (p * q) + 1 := by ring
    _ ≤ (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) := by
      rw [Nat.succ_le_iff]
      gcongr
    _ = (q * r + r * p + p * q) * (a + b + c) := by ring
    _ ≤ _ := by gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (goal)
Goal:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
_ : p * q * r * (a + b + c) + 1 = p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1
⊢ p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c)
have _₁ : p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1 ≤
  (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)
Tactic: calc
    _ = (p * a) * (q * r) + (q * b) * (r * p) + (r * c) * (p * q) + 1 := by ring
    _ ≤ (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) := by
      rw [Nat.succ_le_iff]
      gcongr
    _ = (q * r + r * p + p * q) * (a + b + c) := by ring
    _ ≤ _ := by gcongr