-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
zero :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X f.natDegree *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
zero₁ :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree) *
          HPow.hPow (α := R[X]) X f.natDegree)) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
zero₂ :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X g.natDegree * HPow.hPow (α := R[X]) X f.natDegree))) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
zero₃ :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (g.natDegree + f.natDegree)))) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
zero₄ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
        (reflect (N + O) (HPow.hPow (α := R[X]) X (g.natDegree + f.natDegree)))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (reflect N (HPow.hPow (α := R[X]) X f.natDegree)) *
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
        (reflect O (HPow.hPow (α := R[X]) X g.natDegree))
zero₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt (N + O) : (a : ℕ) → ℕ) (g.natDegree + f.natDegree) : ℕ))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) f.natDegree : ℕ)) *
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt O : (a : ℕ) → ℕ) g.natDegree : ℕ))
zero₆ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt (N + O) : (a : ℕ) → ℕ) (f.natDegree + g.natDegree) : ℕ))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) f.natDegree : ℕ)) *
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt O : (a : ℕ) → ℕ) g.natDegree : ℕ))
⊢ reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
have zero₇ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
      (HPow.hPow (α := R[X]) X
        (HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt N : (a : ℕ) → ℕ) f.natDegree : ℕ)
          ((revAt O : (a : ℕ) → ℕ) g.natDegree : ℕ)))) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) f.natDegree : ℕ)) *
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt O : (a : ℕ) → ℕ) g.natDegree : ℕ))
Tactic: simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul,
        reflect_monomial, add_comm, revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ←
        pow_add (X : R[X]), add_comm]