-- Module: Mathlib.RingTheory.Polynomial.IntegralNormalization
Goal:
R : Type u
inst : Semiring R
p : R[X]
A : Type u_1
inst_1 : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute ((f : (a : R) → A) p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute.{u_1} (S := A) ((f : (a : R) → A) r : A) ((f : (a : R) → A) r' : A)
n : ℕ
_hn : n ∈ Finset.range (p.natDegree + 1)
a :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
      (HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) n * x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₁ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
        (HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) n) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₂ :
  HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
        ((f : (a : R) → A) (p.leadingCoeff ^ n) : A) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₃ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n * p.leadingCoeff ^ n) : A) (x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₄ :
  HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n * p.leadingCoeff ^ (p.natDegree - 1)) : A) (x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₅ :
  HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (p.coeff n) : A)
        ((f : (a : R) → A) (p.leadingCoeff ^ (p.natDegree - 1)) : A) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₆ :
  HMul.hMul (α := A) (β := A) ((f : (a : R) → A) (p.leadingCoeff ^ (p.natDegree - 1)) : A)
        ((f : (a : R) → A) (p.coeff n) : A) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₇ :
  HMul.hMul (β := A) (HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1))
        ((f : (a : R) → A) (p.coeff n) : A) *
      x ^ n =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
a₈ a₉ :
  HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)
⊢ HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff n) : A)
      (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ n) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff n) : A) (x ^ n)

Tactic:
rw [h₁.mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
    integralNormalization_coeff_mul_leadingCoeff_pow _ h, f.map_mul, h₂.eq, f.map_pow, mul_assoc]

Premises used: mul_assoc, Commute.mul_pow, Polynomial.integralNormalization_coeff_mul_leadingCoeff_pow, RingHom.map_mul, Commute.eq, RingHom.map_pow