-- 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
rw rw₁ rw₂ rw₃ :
  ∀ (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'
rw₄ :
  ∀ (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'
rw₅ :
  ∀ (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'),
    ∃ (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'
rw₆ :
  ∀ (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]),
    let d := @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'
rw₇ :
  ∀ (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]),
    let d := @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'
rw₈ :
  ∀ (a b c : k[X]) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (a' b' : k[X]),
    let d := @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'
rw₉ :
  ∀ (a b c : k[X]) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (a' b' : k[X]),
    let d := @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'
rw₁₀ :
  ∀ (a b c : k[X]) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (a' b' : k[X]),
    let d := @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'
rw₁₁ :
  ∀ (a b c : k[X]) (hb : b ≠ 0) (hc : c ≠ 0) (a' b' : k[X]),
    let d := @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'
rw₁₂ :
  ∀ (a b c : k[X]) (hc : c ≠ 0) (a' b' : k[X]),
    let d := @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'
rw₁₃ :
  ∀ (a b c a' b' : k[X]),
    let d := @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'
rw₁₄ :
  ∀ (a b c a' b' : k[X]),
    let d := @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'
⊢ FermatLastTheoremWith'.{u_1} k[X] n
have rw₁₅ : ∀ (a b c a' b' : k[X]),
  let d := @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'
Tactic: classical
  rw [FermatLastTheoremWith']
  intro a b c ha hb hc heq
  obtain ⟨a', eq_a⟩ := gcd_dvd_left a b
  obtain ⟨b', eq_b⟩ := gcd_dvd_right a b
  set d := gcd a b
  have hd : d ≠ 0 := gcd_ne_zero_of_left ha
  rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq
  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
  obtain ⟨c', eq_c⟩ := hdc
  rw [eq_a, mul_ne_zero_iff] at ha
  rw [eq_b, mul_ne_zero_iff] at hb
  rw [eq_c, mul_ne_zero_iff] at hc
  rw [mul_comm] at eq_a eq_b eq_c
  refine ⟨d, a', b', c', ⟨eq_a, eq_b, eq_c⟩, ?_⟩
  rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq
  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⟩
  apply flt hn chn ha.right hb.right hc.right _ heq
  convert! isCoprime_div_gcd_div_gcd _
  · exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm
  · exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm
  · rw [eq_b]
    exact mul_ne_zero hb.right hb.left