awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
h :
  Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      R[X])
simp_rw :
  HMul.hMul (α := R[X]) (β := R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)) : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
⊢ Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      R[X])
have simp_rw₂ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
    (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) X) : R[X]) (n + 1)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
    (HPow.hPow (α := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) X : R[X]) (n + 1))
Tactic: simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
h :
  Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      R[X])
simp_rw :
  HMul.hMul (α := R[X]) (β := R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)) : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) X) : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) X : R[X]) (n + 1))
⊢ Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      R[X])
have simp_rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
    (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) (n + 1)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
Tactic: simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
h :
  Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      R[X])
simp_rw :
  HMul.hMul (α := R[X]) (β := R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)) : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) X) : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) X : R[X]) (n + 1))
simp_rw₃ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
⊢ Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      R[X])
have simp_rw₄ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
    (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) X : R[X]) q ^ (n + 1)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
Tactic: simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
h :
  Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      R[X])
simp_rw :
  HMul.hMul (α := R[X]) (β := R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)) : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) X) : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) X : R[X]) (n + 1))
simp_rw₃ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
simp_rw₄ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) X : R[X]) q ^ (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
⊢ Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      R[X])
have simp_rw₅ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((HPow.hPow (α := R[X]) X p ^ q) ^ (n + 1)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
Tactic: simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
r : R
⊢ Eq (α := R[X]) ((expand R 1 : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) ((C : (a : R) → R[X]) r : R[X])
have rw : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) r : R[X])
Tactic: rw [expand_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f_1 f g : R[X]
ihf : (expand R 1 : (a : R[X]) → R[X]) f = f
ihg : (expand R 1 : (a : R[X]) → R[X]) g = g
⊢ (expand R 1 : (a : R[X]) → R[X]) (f + g) = f + g
have rw : HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) f : R[X])
    ((expand R 1 : (a : R[X]) → R[X]) g : R[X]) =
  f + g
Tactic: rw [map_add, ihf, ihg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f_1 f g : R[X]
ihf : (expand R 1 : (a : R[X]) → R[X]) f = f
ihg : (expand R 1 : (a : R[X]) → R[X]) g = g
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) f : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) g : R[X]) =
    f + g
⊢ (expand R 1 : (a : R[X]) → R[X]) (f + g) = f + g
have rw₁ : HAdd.hAdd (β := R[X]) f ((expand R 1 : (a : R[X]) → R[X]) g : R[X]) = f + g
Tactic: rw [map_add, ihf, ihg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f_1 f g : R[X]
ihf : (expand R 1 : (a : R[X]) → R[X]) f = f
ihg : (expand R 1 : (a : R[X]) → R[X]) g = g
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) f : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) g : R[X]) =
    f + g
rw₁ : HAdd.hAdd (β := R[X]) f ((expand R 1 : (a : R[X]) → R[X]) g : R[X]) = f + g
⊢ (expand R 1 : (a : R[X]) → R[X]) (f + g) = f + g
have rw₂ : f + g = f + g
Tactic: rw [map_add, ihf, ihg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
r : R
h :
  (expand R 1 : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)
⊢ (expand R 1 : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
have rw : HMul.hMul (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
    ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
Tactic: rw [map_mul, expand_C, map_pow, expand_X, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
r : R
h :
  (expand R 1 : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
⊢ (expand R 1 : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
have rw₁ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
    ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
Tactic: rw [map_mul, expand_C, map_pow, expand_X, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
r : R
h :
  (expand R 1 : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
⊢ (expand R 1 : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
have rw₂ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
    (HPow.hPow (α := R[X]) ((expand R 1 : (a : R[X]) → R[X]) X : R[X]) (n + 1)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
Tactic: rw [map_mul, expand_C, map_pow, expand_X, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
r : R
h :
  (expand R 1 : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R 1 : (a : R[X]) → R[X]) X : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
⊢ (expand R 1 : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
have rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1 ^ (n + 1)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
Tactic: rw [map_mul, expand_C, map_pow, expand_X, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
r : R
h :
  (expand R 1 : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R 1 : (a : R[X]) → R[X]) X : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₃ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1 ^ (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
⊢ (expand R 1 : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
have rw₄ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
Tactic: rw [map_mul, expand_C, map_pow, expand_X, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
⊢ (expand R (p ^ Nat.zero) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
have rw : (expand R 1 : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
Tactic: rw [pow_zero, expand_one, Function.iterate_zero, id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
rw : (expand R 1 : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
⊢ (expand R (p ^ Nat.zero) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
have rw₁ : f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
Tactic: rw [pow_zero, expand_one, Function.iterate_zero, id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
rw : (expand R 1 : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
rw₁ : f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
⊢ (expand R (p ^ Nat.zero) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
have rw₂ : f = id f
Tactic: rw [pow_zero, expand_one, Function.iterate_zero, id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
rw : (expand R 1 : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
rw₁ : f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
rw₂ : f = id f
⊢ (expand R (p ^ Nat.zero) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
have rw₃ : f = f
Tactic: rw [pow_zero, expand_one, Function.iterate_zero, id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n] f
⊢ (expand R (p ^ n.succ) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n.succ] f
have rw : Eq (α := R[X]) ((expand R (p ^ n.succ) : (a : R[X]) → R[X]) f : R[X])
  ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
Tactic: rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n] f
rw :
  Eq (α := R[X]) ((expand R (p ^ n.succ) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
⊢ (expand R (p ^ n.succ) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n.succ] f
have rw₁ : Eq (α := R[X]) ((expand R (p * p ^ n) : (a : R[X]) → R[X]) f : R[X])
  ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
Tactic: rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n] f
rw :
  Eq (α := R[X]) ((expand R (p ^ n.succ) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
rw₁ :
  Eq (α := R[X]) ((expand R (p * p ^ n) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
⊢ (expand R (p ^ n.succ) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n.succ] f
have rw₂ : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) f) : R[X])
  ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
Tactic: rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n] f
rw :
  Eq (α := R[X]) ((expand R (p ^ n.succ) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
rw₁ :
  Eq (α := R[X]) ((expand R (p * p ^ n) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
rw₂ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) f) : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
⊢ (expand R (p ^ n.succ) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n.succ] f
have rw₃ : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
  ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
Tactic: rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
⊢ (derivative : (a : R[X]) → R[X]) ((expand R p : (a : R[X]) → R[X]) f) =
    HMul.hMul (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) f) : R[X])
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
have rw : (derivative : (a : R[X]) → R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) f) =
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
    ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
Tactic: rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]