awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₁ : eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
  m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₂ : eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
  m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₃ : eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
  m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₄ : eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
  m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₄ :
  eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₅ : m • r * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
  m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₄ :
  eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₅ :
  m • r * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₆ : m • r * (m • x) ^ (n + 1) =
  m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₄ :
  eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₅ :
  m • r * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₆ :
  m • r * (m • x) ^ (n + 1) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₇ : m • r * (m • x) ^ (n + 1) = m • (eval x ((C : (a : S) → S[X]) r) * eval x (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₄ :
  eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₅ :
  m • r * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₆ :
  m • r * (m • x) ^ (n + 1) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₇ : m • r * (m • x) ^ (n + 1) = m • (eval x ((C : (a : S) → S[X]) r) * eval x (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₈ : m • r * (m • x) ^ (n + 1) = m • (r * eval x (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₄ :
  eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₅ :
  m • r * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₆ :
  m • r * (m • x) ^ (n + 1) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₇ : m • r * (m • x) ^ (n + 1) = m • (eval x ((C : (a : S) → S[X]) r) * eval x (HPow.hPow (α := S[X]) X (n + 1)))
rw₈ : m • r * (m • x) ^ (n + 1) = m • (r * eval x (HPow.hPow (α := S[X]) X (n + 1)))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₉ : m • r * (m • x) ^ (n + 1) = m • (r * x ^ (n + 1))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₄ :
  eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₅ :
  m • r * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₆ :
  m • r * (m • x) ^ (n + 1) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₇ : m • r * (m • x) ^ (n + 1) = m • (eval x ((C : (a : S) → S[X]) r) * eval x (HPow.hPow (α := S[X]) X (n + 1)))
rw₈ : m • r * (m • x) ^ (n + 1) = m • (r * eval x (HPow.hPow (α := S[X]) X (n + 1)))
rw₉ : m • r * (m • x) ^ (n + 1) = m • (r * x ^ (n + 1))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₁₀ : m • r * (m • x) ^ (n + 1) = m • r * m • x ^ (n + 1)
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
rw :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₁ :
  eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * HSMul.hSMul (β := S[X]) m X ^ (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₂ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HSMul.hSMul (β := S[X]) m X ^ (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₃ :
  eval (m • x) (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (m • r) : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₄ :
  eval (m • x) ((C : (a : S) → S[X]) (m • r)) * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₅ :
  m • r * eval (m • x) (HPow.hPow (α := S[X]) X (n + 1)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₆ :
  m • r * (m • x) ^ (n + 1) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
rw₇ : m • r * (m • x) ^ (n + 1) = m • (eval x ((C : (a : S) → S[X]) r) * eval x (HPow.hPow (α := S[X]) X (n + 1)))
rw₈ : m • r * (m • x) ^ (n + 1) = m • (r * eval x (HPow.hPow (α := S[X]) X (n + 1)))
rw₉ : m • r * (m • x) ^ (n + 1) = m • (r * x ^ (n + 1))
rw₁₀ : m • r * (m • x) ^ (n + 1) = m • r * m • x ^ (n + 1)
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw₁₁ : m • r * (m • x) ^ (n + 1) = m • r * (m • x) ^ (n + 1)
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
S : Type u_3
inst : CommSemiring S
G : Type u_4
inst_1 : Group G
inst_2 : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval (g • x) f = g • eval x (g⁻¹ • f)
have rw : eval (g • x) f = eval (g • x) (g • g⁻¹ • f)
Tactic: rw [← smul_eval_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
S : Type u_3
inst : CommSemiring S
G : Type u_4
inst_1 : Group G
inst_2 : MulSemiringAction G S
g : G
f : S[X]
x : S
rw : eval (g • x) f = eval (g • x) (g • g⁻¹ • f)
⊢ eval (g • x) f = g • eval x (g⁻¹ • f)
have rw₁ : eval (g • x) f = eval (g • x) f
Tactic: rw [← smul_eval_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
S : Type u_3
inst : CommSemiring S
G : Type u_4
inst_1 : Group G
inst_2 : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval x (g • f) = g • eval (g⁻¹ • x) f
have rw : eval x (g • f) = eval (g • g⁻¹ • x) (g • f)
Tactic: rw [← smul_eval_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
S : Type u_3
inst : CommSemiring S
G : Type u_4
inst_1 : Group G
inst_2 : MulSemiringAction G S
g : G
f : S[X]
x : S
rw : eval x (g • f) = eval (g • g⁻¹ • x) (g • f)
⊢ eval x (g • f) = g • eval (g⁻¹ • x) f
have rw₁ : eval x (g • f) = eval x (g • f)
Tactic: rw [← smul_eval_smul, smul_inv_smul]