-- 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 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
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
suffices goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0 by
  simp [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⟩

Result:
case 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
⊢ a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0

Proof state:
case 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
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 a' b' c', (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

Result:
case 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
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 a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ 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
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'

Tactic:
have hdc : d ∣ c := by
  have hn : 0 < n := by omega
  have hdncn : d ^ n ∣ c ^ n := ⟨_, heq.symm⟩
  rw [dvd_iff_normalizedFactors_le_normalizedFactors hd hc]
  rw [dvd_iff_normalizedFactors_le_normalizedFactors
        (pow_ne_zero n hd) (pow_ne_zero n hc),
      normalizedFactors_pow, normalizedFactors_pow] at hdncn
  simp_rw [Multiset.le_iff_count, Multiset.count_nsmul,
    mul_le_mul_left hn] at hdncn ⊢
  exact hdncn

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
hdc : d ∣ c
⊢ ∃ 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
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')

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

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
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 : d ≠ 0 ∧ cb' ≠ 0
hb' : C cb' = b'
cc' : k
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
⊢ FermatLastTheoremWith' k[X] n

Tactic:
rw [FermatLastTheoremWith']

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
⊢ ∀ (a b c : k[X]),
    a ≠ 0 →
      b ≠ 0 →
        c ≠ 0 →
          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'

Proof state:
case 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
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 a' b' c', (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⟩, ?_⟩

Result:
case 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
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'

Proof state:
case 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
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'

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

Result:
case 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
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Proof state:
case 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
⊢ a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0

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

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
⊢ IsCoprime a' b'

Proof state:
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'

Tactic:
obtain ⟨b', eq_b⟩ := gcd_dvd_right 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' : 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'

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
⊢ d ∣ c

Tactic:
have hdncn : d ^ n ∣ c ^ n := ⟨_, heq.symm⟩

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
⊢ d ∣ c