-- Mathlib/NumberTheory/FLT/Polynomial.lean
theorem fermatLastTheoremWith'_polynomial {n : ℕ} (hn : 3 ≤ n) (chn : (n : k) ≠ 0) :
    FermatLastTheoremWith' k[X] n

Proof state:
case intro.intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd 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 a' b' c', (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

Result:
case intro.intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd 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 a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
hn✝ : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd 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:
rw [dvd_iff_normalizedFactors_le_normalizedFactors hd hc]

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
hn✝ : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd 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
⊢ normalizedFactors d ≤ normalizedFactors c

Proof state:
case h.e'_4
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd 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' = b / gcd a b

Tactic:
exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd 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 ca' = a'
cb' : k
hb' : C cb' = b'
cc' : k
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')

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

Result:
case intro.intro.intro.intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd 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 ca' = a'
cb' : k
hb' : C cb' = b'
cc' : k
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')

Proof state:
case intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 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 a b
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

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

Result:
case intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd 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 a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Proof state:
case convert_6
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd 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' * d ≠ 0

Tactic:
exact mul_ne_zero hb.right hb.left

Result:
no goals

Proof state:
case h.e'_3
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd 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' = ?convert_4 / gcd ?convert_4 ?convert_5

Tactic:
exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm

Result:
no goals

Proof state:
case intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd 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 a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
obtain ⟨c', eq_c⟩ := hdc

Result:
case intro.intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd 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 a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd 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'

Tactic:
simp [natDegree_eq_zero] at goal

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd 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, C x = a') ∧ (∃ x, C x = b') ∧ ∃ x, C x = c'
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Proof state:
case intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 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 a b * a'
b' : k[X]
eq_b : b = gcd a b * b'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
set d := gcd a b

Result:
case intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 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 a b
eq_a : a = d * a'
eq_b : b = d * b'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Proof state:
case intro.intro.intro.intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd 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 ca' = a'
cb' : k
hb : d ≠ 0 ∧ cb' ≠ 0
hb' : C cb' = b'
cc' : k
hc : d ≠ 0 ∧ cc' ≠ 0
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')

Tactic:
exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
⊢ ∃ d a' b' c', (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

Result:
case intro
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 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 a b * a'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'