awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
⊢ 3 * (n * n) ≤ n * (n * n)

Tactic:
Nat.mul_le_mul_right (n * n) hn

Premises used: HMul.hMul, Nat.mul_le_mul_right
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
⊢ 3 * (n * n) ≤ n * (n * n)

Tactic:
exact Nat.mul_le_mul_right (n * n) hn

Premises used: HMul.hMul, Nat.mul_le_mul_right
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
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'
⊢ ∃ (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

Premises used: GCDMonoid.gcd_dvd_left
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
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'
⊢ ∃ (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

Premises used: GCDMonoid.gcd_dvd_right
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
b' : k[X]
eq_b : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * b'
⊢ let d := @gcd _ CommSemiring.toCommMonoidWithZero _ a b;
  a = d * a'

Tactic:
set d := gcd a b

Premises used: GCDMonoid.gcd
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
b' : k[X]
eq_b : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * b'
eq_a₁ :
  let d := @gcd _ CommSemiring.toCommMonoidWithZero _ a b;
  a = d * a'
⊢ let d := @gcd _ CommSemiring.toCommMonoidWithZero _ a b;
  b = d * b'

Tactic:
set d := gcd a b

Premises used: GCDMonoid.gcd
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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 ≠ 0

Tactic:
have hd : d ≠ 0 := gcd_ne_zero_of_left ha
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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 ^ n * (a' ^ n + b' ^ n) = c ^ n

Tactic:
rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq

Premises used: mul_add, mul_pow
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
heq₁ : d ^ n * (a' ^ n + b' ^ n) = c ^ n
⊢ a = d * a'

Tactic:
rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq

Premises used: mul_add, mul_pow
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
heq₁ : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a₁ : a = d * a'
⊢ b = d * b'

Tactic:
rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq

Premises used: mul_add, mul_pow
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
heq₁ : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a₁ : a = d * a'
eq_b₁ : b = d * b'
⊢ d ≠ 0

Tactic:
rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq

Premises used: mul_add, mul_pow
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
⊢ 0 < n

Tactic:
have hn : 0 < n := by lia
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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 ^ n ∣ c ^ n

Tactic:
have hdncn : d ^ n ∣ c ^ n := ⟨_, heq.symm⟩
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
hdncn : d ^ n ∣ c ^ n
⊢ d ∣ c

Tactic:
simpa [dvd_iff_normalizedFactors_le_normalizedFactors, Multiset.le_iff_count, *] using hdncn

Premises used: Multiset.le_iff_count, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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

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
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
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'
⊢ ∃ (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
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
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'
⊢ ∃ (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

Premises used: mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
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'
⊢ ∃ (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

Premises used: mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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 ≠ 0 ∧ c' ≠ 0

Tactic:
rw [eq_c, mul_ne_zero_iff] at hc

Premises used: mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
hc₁ : d ≠ 0 ∧ c' ≠ 0
⊢ c = d * c'

Tactic:
rw [eq_c, mul_ne_zero_iff] at hc

Premises used: mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
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'
⊢ ∃ (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

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'

Tactic:
⟨d, a', b', c', ⟨eq_a, eq_b, eq_c⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
refine : IsUnit a' ∧ IsUnit b' ∧ IsUnit 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:
refine ⟨d, a', b', c', ⟨eq_a, eq_b, eq_c⟩, ?_⟩
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
⊢ a' ^ n + b' ^ n = c' ^ n

Tactic:
rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq

Premises used: pow_ne_zero, mul_comm, mul_left_inj', mul_pow
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
heq₁ : a' ^ n + b' ^ n = c' ^ n
⊢ d ≠ 0 ∧ c' ≠ 0

Tactic:
rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq

Premises used: pow_ne_zero, mul_comm, mul_left_inj', mul_pow
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
heq₁ : a' ^ n + b' ^ n = c' ^ n
hc₁ : d ≠ 0 ∧ c' ≠ 0
⊢ c = c' * d

Tactic:
rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq

Premises used: pow_ne_zero, mul_comm, mul_left_inj', mul_pow
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
⊢ (∃ (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

Premises used: Polynomial.natDegree_eq_zero
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
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'
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
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])
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
rw [← ha', ← hb', ← hc']
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
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])
⊢ 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

Premises used: Polynomial.C_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
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])
⊢ 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

Premises used: Polynomial.C_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
⊢ d ≠ 0 ∧ cc' ≠ 0

Tactic:
rw [← hc', C_ne_zero] at hc

Premises used: Polynomial.C_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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'
hc₁ : d ≠ 0 ∧ cc' ≠ 0
⊢ (C : (a : k) → k[X]) cc' = c'

Tactic:
rw [← hc', C_ne_zero] at hc

Premises used: Polynomial.C_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
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 : d ≠ 0 ∧ cc' ≠ 0
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:
⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩

Premises used: And.right, And.intro, _private.0.Ne.isUnit_C
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
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 : d ≠ 0 ∧ cc' ≠ 0
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:
exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
suffices : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

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⟩
-- Module: Mathlib.NumberTheory.FLT.Polynomial
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
apply : IsCoprime a' b'
⊢ a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0

Tactic:
apply flt hn chn ha.right hb.right hc.right _ heq

Premises used: And.right, Polynomial.flt