awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
pos : ∀ (h : p.degree = (↑i : WithBot ℕ)), 1 * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
⊢ (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
have neg : ∀ (h : ¬p.degree = (↑i : WithBot ℕ)),
  p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
have neg : p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
Tactic: simp only [mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
have pos : ∀ (h' : (↑i : WithBot ℕ) < p.degree),
  p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
Tactic: by_cases h' : i < p.degree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
pos :
  ∀ (h' : (↑i : WithBot ℕ) < p.degree),
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
have neg : ∀ (h' : ¬(↑i : WithBot ℕ) < p.degree),
  p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
Tactic: by_cases h' : i < p.degree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
have pos : i ≤ p.natDegree - 1
Tactic: rw [tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
⊢ i ≤ p.natDegree - 1
have pos : i < p.natDegree
Tactic: rw [le_tsub_iff_right hp, Nat.succ_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ HMul.hMul (β := R[X]) p.integralNormalization ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) =
    p.scaleRoots p.leadingCoeff
have a : ∀ (i : ℕ),
  (HMul.hMul (β := R[X]) p.integralNormalization ((C : (a : R) → R[X]) p.leadingCoeff : R[X])).coeff i =
    (p.scaleRoots p.leadingCoeff).coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
⊢ (HMul.hMul (β := R[X]) p.integralNormalization ((C : (a : R) → R[X]) p.leadingCoeff : R[X])).coeff i =
    (p.scaleRoots p.leadingCoeff).coeff i
have a : (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff =
  (p.scaleRoots p.leadingCoeff).coeff i
Tactic: rw [coeff_mul_C, integralNormalization_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
⊢ (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff =
    (p.scaleRoots p.leadingCoeff).coeff i
have pos : ∀ (h : p.degree = (↑i : WithBot ℕ)), 1 * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
pos : ∀ (h : p.degree = (↑i : WithBot ℕ)), 1 * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i
⊢ (if p.degree = (↑i : WithBot ℕ) then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff =
    (p.scaleRoots p.leadingCoeff).coeff i
have neg : ∀ (h : ¬p.degree = (↑i : WithBot ℕ)),
  p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i
have neg : p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
Tactic: simp only [coeff_scaleRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
have pos : ∀ (h' : (↑i : WithBot ℕ) < p.degree),
  p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
Tactic: by_cases h' : i < p.degree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
pos :
  ∀ (h' : (↑i : WithBot ℕ) < p.degree),
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
have neg : ∀ (h' : ¬(↑i : WithBot ℕ) < p.degree),
  p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
Tactic: by_cases h' : i < p.degree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = p.coeff i * p.leadingCoeff ^ (p.natDegree - i)
have pos : 1 ≤ p.natDegree - i
Tactic: rw [mul_assoc, ← pow_succ, tsub_right_comm, tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = (↑i : WithBot ℕ)
h' : (↑i : WithBot ℕ) < p.degree
⊢ 1 ≤ p.natDegree - i
have pos : i < p.natDegree
Tactic: rw [le_tsub_iff_left (coe_lt_degree.mp h').le, Nat.succ_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
S : Type v
inst : CommSemiring S
p : S[X]
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff
have rw : HMul.hMul (α := S[X]) ((algebraMap S S[X] : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization =
  p.scaleRoots p.leadingCoeff
Tactic: rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
S : Type v
inst : CommSemiring S
p : S[X]
rw :
  HMul.hMul (α := S[X]) ((algebraMap S S[X] : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization =
    p.scaleRoots p.leadingCoeff
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff
have rw₁ : HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization = p.scaleRoots p.leadingCoeff
Tactic: rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
S : Type v
inst : CommSemiring S
p : S[X]
rw :
  HMul.hMul (α := S[X]) ((algebraMap S S[X] : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization =
    p.scaleRoots p.leadingCoeff
rw₁ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization =
    p.scaleRoots p.leadingCoeff
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff
have rw₂ : HMul.hMul (β := S[X]) p.integralNormalization ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) = p.scaleRoots p.leadingCoeff
Tactic: rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
Goal:
S : Type v
inst : CommSemiring S
p : S[X]
rw :
  HMul.hMul (α := S[X]) ((algebraMap S S[X] : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization =
    p.scaleRoots p.leadingCoeff
rw₁ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) p.integralNormalization =
    p.scaleRoots p.leadingCoeff
rw₂ :
  HMul.hMul (β := S[X]) p.integralNormalization ((C : (a : S) → S[X]) p.leadingCoeff : S[X]) =
    p.scaleRoots p.leadingCoeff
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff
have rw₃ : p.scaleRoots p.leadingCoeff = p.scaleRoots p.leadingCoeff
Tactic: rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x) p.integralNormalization =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) * eval₂ f x p
have rw : Eq.{u_1 + 1} (α := A)
  (∑ i ∈ Finset.range (p.integralNormalization.natDegree + 1),
    HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff i) : A)
      (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ i))
  (∑ i ∈ Finset.range (p.natDegree + 1),
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff i) : A) (x ^ i))
Tactic: rw [eval₂_eq_sum_range, eval₂_eq_sum_range, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ i ∈ Finset.range (p.integralNormalization.natDegree + 1),
      HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff i) : A)
        (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ i))
    (∑ i ∈ Finset.range (p.natDegree + 1),
      HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
        HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff i) : A) (x ^ i))
have h₃ : Finset.range (p.integralNormalization.natDegree + 1) = Finset.range (p.natDegree + 1)
Tactic: apply Finset.sum_congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
h₃ : Finset.range (p.integralNormalization.natDegree + 1) = Finset.range (p.natDegree + 1)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ i ∈ Finset.range (p.integralNormalization.natDegree + 1),
      HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff i) : A)
        (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ i))
    (∑ i ∈ Finset.range (p.natDegree + 1),
      HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
        HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff i) : A) (x ^ i))
have a : ∀ x_1 ∈ Finset.range (p.natDegree + 1),
  HMul.hMul (α := A) ((f : (a : R) → A) (p.integralNormalization.coeff x_1) : A)
      (HMul.hMul (α := A) ((f : (a : R) → A) p.leadingCoeff : A) x ^ x_1) =
    HPow.hPow (α := A) ((f : (a : R) → A) p.leadingCoeff : A) (p.natDegree - 1) *
      HMul.hMul (α := A) ((f : (a : R) → A) (p.coeff x_1) : A) (x ^ x_1)
Tactic: apply Finset.sum_congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ Finset.range (p.integralNormalization.natDegree + 1) = Finset.range (p.natDegree + 1)
have h₃ : Finset.range (p.natDegree + 1) = Finset.range (p.natDegree + 1)
Tactic: rw [natDegree_eq_of_degree_eq p.degree_integralNormalization]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IntegralNormalization (goal)
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)
⊢ 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)
have 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)
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]