-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m
mul_eq : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g = p
this : (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0 = eval t g
inr :
  eval t g =
    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g).comp
        (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₁ :
  eval t g =
    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m).comp
          (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₂ :
  eval t g =
    ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])).comp
            (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ^
          m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₃ :
  eval t g =
    ((comp X (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) -
            comp ((C : (a : R) → R[X]) t) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) ^
          m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₄ :
  eval t g =
    ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) -
            comp ((C : (a : R) → R[X]) t) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) ^
          m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₅ :
  eval t g =
    (HSub.hSub (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))
            ((C : (a : R) → R[X]) t : R[X]) ^
          m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₆ :
  eval t g =
    (HPow.hPow (α := R[X]) X m *
        g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₇ :
  eval t g =
    (HPow.hPow (α := R[X]) X m *
          g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).reverse.leadingCoeff
inr₈ : eval t g = (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).reverse.leadingCoeff
inr₉ : eval t g = (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr₁₀ :
  eval t g =
    (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff
      (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).natTrailingDegree
⊢ eval t g = (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
have inr₁₁ : eval t g = (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0
Tactic: rw [← congr_arg (comp · <| X + C t) mul_eq, mul_comp, pow_comp, sub_comp, X_comp, C_comp,
    add_sub_cancel_right, ← reverse_leadingCoeff, reverse_X_pow_mul, reverse_leadingCoeff,
    trailingCoeff, Nat.le_zero.1 (natTrailingDegree_le_of_ne_zero <|
      this ▸ eval_divByMonic_pow_rootMultiplicity_ne_zero t hp), this]