awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 1 * a ^ n + 1 * b ^ n + -1 * c ^ n = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have hone : Eq.{u_1 + 1} (α := k[X]) 1 ((C : (a : k) → k[X]) 1)
Tactic: have hone : (1 : k[X]) = C 1 := by rfl
-- 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 : 1 * a ^ n + 1 * b ^ n + -1 * c ^ n = 0
hn' : 0 < n
hone : Eq.{u_1 + 1} (α := k[X]) 1 ((C : (a : k) → k[X]) 1)
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have hneg_one : Eq.{u_1 + 1} (α := k[X]) (-1) ((C : (a : k) → k[X]) (-1))
Tactic: have hneg_one : (-1 : k[X]) = C (-1) := by simp only [map_neg, map_one]
-- 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 : 1 * a ^ n + 1 * b ^ n + -1 * c ^ n = 0
hn' : 0 < n
hone : Eq.{u_1 + 1} (α := k[X]) 1 ((C : (a : k) → k[X]) 1)
hneg_one : Eq.{u_1 + 1} (α := k[X]) (-1) ((C : (a : k) → k[X]) (-1))
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have heq₁ : (C : (a : k) → k[X]) 1 * a ^ n + (C : (a : k) → k[X]) 1 * b ^ n + (C : (a : k) → k[X]) (-1) * c ^ n = 0
Tactic: simp_rw [hneg_one, hone] at heq
Cleared hypotheses: heq
-- 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
hn' : 0 < n
hone : Eq.{u_1 + 1} (α := k[X]) 1 ((C : (a : k) → k[X]) 1)
hneg_one : Eq.{u_1 + 1} (α := k[X]) (-1) ((C : (a : k) → k[X]) (-1))
heq : (C : (a : k) → k[X]) 1 * a ^ n + (C : (a : k) → k[X]) 1 * b ^ n + (C : (a : k) → k[X]) (-1) * c ^ n = 0
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
have apply : n * n + n * n + n * n ≤ n * n * n
Tactic: apply flt_catalan hn'.ne' hn'.ne' hn'.ne' _
    chn chn chn ha hb hc hab one_ne_zero one_ne_zero (neg_ne_zero.mpr one_ne_zero) heq
-- 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
hn' : 0 < n
hone : Eq.{u_1 + 1} (α := k[X]) 1 ((C : (a : k) → k[X]) 1)
hneg_one : Eq.{u_1 + 1} (α := k[X]) (-1) ((C : (a : k) → k[X]) (-1))
heq : (C : (a : k) → k[X]) 1 * a ^ n + (C : (a : k) → k[X]) 1 * b ^ n + (C : (a : k) → k[X]) (-1) * c ^ n = 0
⊢ n * n + n * n + n * n ≤ n * n * n
have eq_lhs : n * n + n * n + n * n = 3 * n * n
Tactic: have eq_lhs : n * n + n * n + n * n = 3 * n * n := by ring
-- 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
hn' : 0 < n
hone : Eq.{u_1 + 1} (α := k[X]) 1 ((C : (a : k) → k[X]) 1)
hneg_one : Eq.{u_1 + 1} (α := k[X]) (-1) ((C : (a : k) → k[X]) (-1))
heq : (C : (a : k) → k[X]) 1 * a ^ n + (C : (a : k) → k[X]) 1 * b ^ n + (C : (a : k) → k[X]) (-1) * c ^ n = 0
eq_lhs : n * n + n * n + n * n = 3 * n * n
⊢ n * n + n * n + n * n ≤ n * n * n
have rw : 3 * (n * n) ≤ n * (n * n)
Tactic: rw [eq_lhs, mul_assoc, mul_assoc]
-- 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
heq : a ^ n + b ^ n = c ^ n
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have obtain : ∀ (a' : k[X]) (eq_a : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * a'),
  ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Tactic: obtain ⟨a', eq_a⟩ := gcd_dvd_left a b
-- 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
heq : a ^ n + b ^ n = c ^ n
a' : k[X]
eq_a : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * a'
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have obtain : ∀ (b' : k[X]) (eq_b : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * b'),
  ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Tactic: obtain ⟨b', eq_b⟩ := gcd_dvd_right a b
-- 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
heq : a ^ n + b ^ n = c ^ n
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
eq_a : a = d * a'
eq_b : b = d * b'
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have hd : d ≠ 0
Tactic: have hd : d ≠ 0 := gcd_ne_zero_of_left ha
-- 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
heq : a ^ n + b ^ n = c ^ n
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have heq₁ : d ^ n * (a' ^ n + b' ^ n) = c ^ n
Tactic: rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq
Cleared hypotheses: heq, eq_a, eq_b, hd
-- 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
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
⊢ d ∣ c
have hn₁ : 0 < n
Tactic: have hn : 0 < n := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Polynomial (hypothesis)
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn_1 : 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
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
hn : 0 < n
⊢ d ∣ c
have hdncn : d ^ n ∣ c ^ n
Tactic: have hdncn : d ^ n ∣ c ^ n := ⟨_, heq.symm⟩
-- 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
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have hdc : d ∣ c
Tactic: have hdc : d ∣ c := by
    -- TODO: This is basically reproving `IsIntegrallyClosed.pow_dvd_pow_iff`
    have hn : 0 < n := by lia
    have hdncn : d ^ n ∣ c ^ n := ⟨_, heq.symm⟩
    simpa [dvd_iff_normalizedFactors_le_normalizedFactors, Multiset.le_iff_count, *] using hdncn
-- 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
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
hdc : d ∣ c
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have obtain : ∀ (c' : k[X]) (eq_c : c = d * c'),
  ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Tactic: obtain ⟨c', eq_c⟩ := hdc
Cleared hypotheses: hdc
-- 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
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
eq_c : c = d * c'
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have rw : ∀ (ha : d ≠ 0 ∧ a' ≠ 0) (heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n) (eq_a : a = d * a') (eq_b : b = d * b') (hd : d ≠ 0)
  (c' : k[X]) (eq_c : c = d * c'),
  ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Tactic: rw [eq_a, mul_ne_zero_iff] at ha
Cleared hypotheses: ha, heq, eq_a, eq_b, hd, c', eq_c
-- 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]
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
eq_c : c = d * c'
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have rw : ∀ (hb : d ≠ 0 ∧ b' ≠ 0) (ha : d ≠ 0 ∧ a' ≠ 0) (heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n) (eq_a : a = d * a')
  (eq_b : b = d * b') (hd : d ≠ 0) (c' : k[X]) (eq_c : c = d * c'),
  ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Tactic: rw [eq_b, mul_ne_zero_iff] at hb
Cleared hypotheses: hb, ha, heq, eq_a, eq_b, hd, c', eq_c
-- 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]
hc : c ≠ 0
a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
eq_c : c = d * c'
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have hc₁ : d ≠ 0 ∧ c' ≠ 0
Tactic: rw [eq_c, mul_ne_zero_iff] at hc
Cleared hypotheses: hc, eq_c
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = d * c'
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have rw : ∀ (eq_a : a = a' * d) (eq_b : b = b' * d) (hd : d ≠ 0) (c' : k[X]) (hc : d ≠ 0 ∧ c' ≠ 0) (eq_c : c = c' * d),
  ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Tactic: rw [mul_comm] at eq_a eq_b eq_c
Cleared hypotheses: eq_a, eq_b, hd, c', hc, eq_c
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ ∃ (d : k[X]) (a' : k[X]) (b' : k[X]) (c' : k[X]),
    (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have refine : IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Tactic: refine ⟨d, a', b', c', ⟨eq_a, eq_b, eq_c⟩, ?_⟩
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have heq₁ : a' ^ n + b' ^ n = c' ^ n
Tactic: rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq
Cleared hypotheses: heq, hc, eq_c
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have goal₁ : (∃ (x : k), (C : (a : k) → k[X]) x = a') ∧
  (∃ (x : k), (C : (a : k) → k[X]) x = b') ∧ ∃ (x : k), (C : (a : k) → k[X]) x = c'
Tactic: simp only [natDegree_eq_zero] at goal
Cleared hypotheses: goal
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
goal :
  (∃ (x : k), (C : (a : k) → k[X]) x = a') ∧
    (∃ (x : k), (C : (a : k) → k[X]) x = b') ∧ ∃ (x : k), (C : (a : k) → k[X]) x = c'
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have obtain : ∀ (ca' : k) (ha' : (C : (a : k) → k[X]) ca' = a') (cb' : k) (hb' : (C : (a : k) → k[X]) cb' = b') (cc' : k)
  (hc' : (C : (a : k) → k[X]) cc' = c'), IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Tactic: obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal
Cleared hypotheses: goal
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
ca' : k
ha' : (C : (a : k) → k[X]) ca' = a'
cb' : k
hb' : (C : (a : k) → k[X]) cb' = b'
cc' : k
hc' : (C : (a : k) → k[X]) cc' = c'
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have rw : IsUnit (M := k[X]) ((C : (a : k) → k[X]) ca' : k[X]) ∧
  IsUnit (M := k[X]) ((C : (a : k) → k[X]) cb' : k[X]) ∧ IsUnit (M := k[X]) ((C : (a : k) → k[X]) cc' : k[X])
Tactic: rw [← ha', ← hb', ← hc']
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
ca' : k
ha' : (C : (a : k) → k[X]) ca' = a'
cb' : k
hb' : (C : (a : k) → k[X]) cb' = b'
cc' : k
hc' : (C : (a : k) → k[X]) cc' = c'
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) ca' : k[X]) ∧
    IsUnit (M := k[X]) ((C : (a : k) → k[X]) cb' : k[X]) ∧ IsUnit (M := k[X]) ((C : (a : k) → k[X]) cc' : k[X])
have rw : ∀ (ha : d ≠ 0 ∧ ca' ≠ 0) (ha' : (C : (a : k) → k[X]) ca' = a') (cb' : k) (hb' : (C : (a : k) → k[X]) cb' = b') (cc' : k)
  (hc' : (C : (a : k) → k[X]) cc' = c'),
  IsUnit (M := k[X]) ((C : (a : k) → k[X]) ca' : k[X]) ∧
    IsUnit (M := k[X]) ((C : (a : k) → k[X]) cb' : k[X]) ∧ IsUnit (M := k[X]) ((C : (a : k) → k[X]) cc' : k[X])
Tactic: rw [← ha', C_ne_zero] at ha
Cleared hypotheses: ha, ha', cb', hb', cc', hc'
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
ca' : k
ha : d ≠ 0 ∧ ca' ≠ 0
ha' : (C : (a : k) → k[X]) ca' = a'
cb' : k
hb' : (C : (a : k) → k[X]) cb' = b'
cc' : k
hc' : (C : (a : k) → k[X]) cc' = c'
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) ca' : k[X]) ∧
    IsUnit (M := k[X]) ((C : (a : k) → k[X]) cb' : k[X]) ∧ IsUnit (M := k[X]) ((C : (a : k) → k[X]) cc' : k[X])
have rw : ∀ (hb : d ≠ 0 ∧ cb' ≠ 0) (hb' : (C : (a : k) → k[X]) cb' = b') (cc' : k) (hc' : (C : (a : k) → k[X]) cc' = c'),
  IsUnit (M := k[X]) ((C : (a : k) → k[X]) ca' : k[X]) ∧
    IsUnit (M := k[X]) ((C : (a : k) → k[X]) cb' : k[X]) ∧ IsUnit (M := k[X]) ((C : (a : k) → k[X]) cc' : k[X])
Tactic: rw [← hb', C_ne_zero] at hb
Cleared hypotheses: hb, hb', cc', hc'
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
ca' : k
ha : d ≠ 0 ∧ ca' ≠ 0
ha' : (C : (a : k) → k[X]) ca' = a'
cb' : k
hb : d ≠ 0 ∧ cb' ≠ 0
hb' : (C : (a : k) → k[X]) cb' = b'
cc' : k
hc' : (C : (a : k) → k[X]) cc' = c'
⊢ IsUnit (M := k[X]) ((C : (a : k) → k[X]) ca' : k[X]) ∧
    IsUnit (M := k[X]) ((C : (a : k) → k[X]) cb' : k[X]) ∧ IsUnit (M := k[X]) ((C : (a : k) → k[X]) cc' : k[X])
have hc₁ : d ≠ 0 ∧ cc' ≠ 0
Tactic: rw [← hc', C_ne_zero] at hc
Cleared hypotheses: hc, hc'
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
have suffices : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0
Tactic: suffices goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0 by
    simp only [natDegree_eq_zero] at goal
    obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal
    rw [← ha', ← hb', ← hc']
    rw [← ha', C_ne_zero] at ha
    rw [← hb', C_ne_zero] at hb
    rw [← hc', C_ne_zero] at hc
    exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0
have apply : IsCoprime a' b'
Tactic: apply flt hn chn ha.right hb.right hc.right _ heq
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ IsCoprime a' b'
have h : a' = a / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
Tactic: convert! isCoprime_div_gcd_div_gcd _
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
h : a' = a / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
⊢ IsCoprime a' b'
have h₁ : b' = b / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
Tactic: convert! isCoprime_div_gcd_div_gcd _
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
h : a' = a / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
h₁ : b' = b / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
⊢ IsCoprime a' b'
have convert_3 : GCDMonoid k[X]
Tactic: convert! isCoprime_div_gcd_div_gcd _
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
h : a' = a / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
h₁ : b' = b / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
convert_3 : GCDMonoid k[X]
convert_4 convert_5 : k[X]
⊢ IsCoprime a' b'
have convert_6 : b ≠ 0
Tactic: convert! isCoprime_div_gcd_div_gcd _
-- 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 a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b ≠ 0
have convert_6 : b' * d ≠ 0
Tactic: rw [eq_b]