-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
a : R
monomial :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((Polynomial.monomial n : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
monomial₁ :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) Y n)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
monomial₂ :
  Eq (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
          (HPow.hPow (α := R[X][Y]) Y n)) :
      R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
      R[X][Y])
monomial₃ :
  HMul.hMul (α := R[X][Y]) (β := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) (HPow.hPow (α := R[X][Y]) Y n) : R[X][Y]) =
    (C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
monomial₄ :
  HMul.hMul (α := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      (HPow.hPow (α := R[X][Y]) ((swap : (a : R[X][Y]) → R[X][Y]) Y : R[X][Y]) n) =
    (C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
monomial₅ :
  HMul.hMul (α := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      (HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n) =
    (C : (a : R[X]) → R[X][Y]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
monomial₆ :
  HMul.hMul (α := R[X][Y])
      ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
      (HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n) =
    HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
      ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) X n) : R[X][Y])
⊢ Eq.{u_1 + 1} (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) (map C ((Polynomial.monomial n : (a : R) → R[X]) a)) : R[X][Y])
    ((C : (a : R[X]) → R[X][Y]) ((Polynomial.monomial n : (a : R) → R[X]) a) : R[X][Y])
have monomial₇ : HMul.hMul (α := R[X][Y])
    ((swap : (a : R[X][Y]) → R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a)) : R[X][Y])
    (HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n) =
  HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) a) : R[X][Y])
    (HPow.hPow (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) n)
Tactic: rw [map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
    map_mul, map_pow, swap_Y, C_mul, C_pow, Bivariate.swap_C_C]