-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
rw :
  reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X (natTrailingDegree (trinomial k m n u v w)) =
    trinomial k (n - m + k) n w v u
rw₁ : reverse (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₂ :
  reflect (natDegree (trinomial k m n u v w)) (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₃ : reflect n (trinomial k m n u v w) * HPow.hPow (α := R[X]) X k = trinomial k (n - m + k) n w v u
rw₄ :
  reflect n
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₅ :
  (reflect n
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₆ :
  (reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k)) +
          reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₇ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) k : ℕ)) +
          reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₈ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) k : ℕ)) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) m : ℕ)) +
        reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₉ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) k : ℕ)) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) m : ℕ)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₁₀ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k)) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) m : ℕ)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₁₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k)) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₁₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k)) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X (n - n))) *
      HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₁₃ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k)) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m))) *
        HPow.hPow (α := R[X]) X k +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X (n - n)) *
        HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₁₄ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k)) * HPow.hPow (α := R[X]) X k +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m)) *
          HPow.hPow (α := R[X]) X k +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X (n - n)) *
        HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₁₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k) * HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m)) *
          HPow.hPow (α := R[X]) X k +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X (n - n)) *
        HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₁₆ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k) * HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X])
          (HPow.hPow (α := R[X]) X (n - m) * HPow.hPow (α := R[X]) X k) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X (n - n)) *
        HPow.hPow (α := R[X]) X k =
    trinomial k (n - m + k) n w v u
rw₁₇ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k) * HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X])
          (HPow.hPow (α := R[X]) X (n - m) * HPow.hPow (α := R[X]) X k) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X])
        (HPow.hPow (α := R[X]) X (n - n) * HPow.hPow (α := R[X]) X k) =
    trinomial k (n - m + k) n w v u
rw₁₈ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k + k)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X])
          (HPow.hPow (α := R[X]) X (n - m) * HPow.hPow (α := R[X]) X k) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X])
        (HPow.hPow (α := R[X]) X (n - n) * HPow.hPow (α := R[X]) X k) =
    trinomial k (n - m + k) n w v u
rw₁₉ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k + k)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m + k)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X])
        (HPow.hPow (α := R[X]) X (n - n) * HPow.hPow (α := R[X]) X k) =
    trinomial k (n - m + k) n w v u
rw₂₀ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X (n - k + k)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m + k)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X (n - n + k)) =
    trinomial k (n - m + k) n w v u
rw₂₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X n) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m + k)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X (n - n + k)) =
    trinomial k (n - m + k) n w v u
rw₂₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X n) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m + k)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X (0 + k)) =
    trinomial k (n - m + k) n w v u
rw₂₃ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X n) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m + k)) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X k) =
    trinomial k (n - m + k) n w v u
rw₂₄ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X k) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X n) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m + k))) =
    trinomial k (n - m + k) n w v u
rw₂₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X k) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m + k)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X n)) =
    trinomial k (n - m + k) n w v u
⊢ Eq (α := R[X]) (mirror (trinomial k m n u v w)) (trinomial k (n - m + k) n w v u)
have rw₂₆ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X k) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X (n - m + k)) +
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X n) =
  trinomial k (n - m + k) n w v u
Tactic: rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw,
    trinomial_def, reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
    reflect_C_mul_X_pow, revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul,
    add_mul, mul_assoc, mul_assoc, mul_assoc, ← pow_add, ← pow_add, ← pow_add,
    Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm, add_comm (C u * X ^ n),
    ← add_assoc, ← trinomial_def]