awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G x)
⊢ g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x (g • g')) : R[X])
have rw : g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
Tactic: rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G x)
rw :
  g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
⊢ g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x (g • g')) : R[X])
have rw₁ : HSMul.hSMul (β := R[X]) g X - HSMul.hSMul (β := R[X]) g ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
Tactic: rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G x)
rw :
  g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
rw₁ :
  HSMul.hSMul (β := R[X]) g X - HSMul.hSMul (β := R[X]) g ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
⊢ g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x (g • g')) : R[X])
have rw₂ : X - HSMul.hSMul (β := R[X]) g ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
Tactic: rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G x)
rw :
  g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
rw₁ :
  HSMul.hSMul (β := R[X]) g X - HSMul.hSMul (β := R[X]) g ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
rw₂ :
  X - HSMul.hSMul (β := R[X]) g ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
⊢ g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x (g • g')) : R[X])
have rw₃ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X]) =
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
Tactic: rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
g : G
n : ℕ
⊢ g • Polynomial.coeff (prodXSubSMul G R x) n = Polynomial.coeff (prodXSubSMul G R x) n
have rw : (HSMul.hSMul (β := R[X]) g (prodXSubSMul G R x)).coeff n = Polynomial.coeff (prodXSubSMul G R x) n
Tactic: rw [← Polynomial.coeff_smul, prodXSubSMul.smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
g : G
n : ℕ
rw : (HSMul.hSMul (β := R[X]) g (prodXSubSMul G R x)).coeff n = Polynomial.coeff (prodXSubSMul G R x) n
⊢ g • Polynomial.coeff (prodXSubSMul G R x) n = Polynomial.coeff (prodXSubSMul G R x) n
have rw₁ : Polynomial.coeff (prodXSubSMul G R x) n = Polynomial.coeff (prodXSubSMul G R x) n
Tactic: rw [← Polynomial.coeff_smul, prodXSubSMul.smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
have rw : map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
  HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
Tactic: rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
rw :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
have rw₁ : map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)) =
  HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
Tactic: rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
rw :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₁ :
  map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
have rw₂ : (C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) =
  HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
Tactic: rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
rw :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₁ :
  map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₂ :
  (C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
have rw₃ : (C : (a : Q) → Q[X]) ((g : (a : P) → Q) (m • b)) =
  HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
Tactic: rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
rw :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₁ :
  map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₂ :
  (C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₃ :
  (C : (a : Q) → Q[X]) ((g : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
have rw₄ : (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
  HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
Tactic: rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
rw :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₁ :
  map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₂ :
  (C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₃ :
  (C : (a : Q) → Q[X]) ((g : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₄ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
have rw₅ : (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
  HSMul.hSMul (β := Q[X]) m ((C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) b) : Q[X])
Tactic: rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
rw :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₁ :
  map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₂ :
  (C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₃ :
  (C : (a : Q) → Q[X]) ((g : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₄ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₅ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m ((C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) b) : Q[X])
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
have rw₆ : (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
  HSMul.hSMul (β := Q[X]) m ((C : (a : Q) → Q[X]) ((g : (a : P) → Q) b) : Q[X])
Tactic: rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
rw :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₁ :
  map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₂ :
  (C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₃ :
  (C : (a : Q) → Q[X]) ((g : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₄ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₅ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m ((C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) b) : Q[X])
rw₆ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m ((C : (a : Q) → Q[X]) ((g : (a : P) → Q) b) : Q[X])
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
have rw₇ : Eq (α := Q[X]) ((C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) : Q[X])
  ((C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) : Q[X])
Tactic: rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p_1 p q : P[X]
ihp :
  map (↑g : P →+* Q) (m • p) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p)
ihq :
  map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q)
⊢ map (↑g : P →+* Q) (m • (p + q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
have rw : map (↑g : P →+* Q) (m • p + m • q) =
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
Tactic: rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p_1 p q : P[X]
ihp :
  map (↑g : P →+* Q) (m • p) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p)
ihq :
  map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q)
rw :
  map (↑g : P →+* Q) (m • p + m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
⊢ map (↑g : P →+* Q) (m • (p + q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
have rw₁ : HAdd.hAdd (α := Q[X]) (map (↑g : P →+* Q) (m • p)) (map (↑g : P →+* Q) (m • q)) =
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
Tactic: rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p_1 p q : P[X]
ihp :
  map (↑g : P →+* Q) (m • p) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p)
ihq :
  map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q)
rw :
  map (↑g : P →+* Q) (m • p + m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₁ :
  HAdd.hAdd (α := Q[X]) (map (↑g : P →+* Q) (m • p)) (map (↑g : P →+* Q) (m • q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
⊢ map (↑g : P →+* Q) (m • (p + q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
have rw₂ : HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
    map (↑g : P →+* Q) (m • q) =
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
Tactic: rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p_1 p q : P[X]
ihp :
  map (↑g : P →+* Q) (m • p) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p)
ihq :
  map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q)
rw :
  map (↑g : P →+* Q) (m • p + m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₁ :
  HAdd.hAdd (α := Q[X]) (map (↑g : P →+* Q) (m • p)) (map (↑g : P →+* Q) (m • q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₂ :
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
      map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
⊢ map (↑g : P →+* Q) (m • (p + q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
have rw₃ : HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q) =
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
Tactic: rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p_1 p q : P[X]
ihp :
  map (↑g : P →+* Q) (m • p) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p)
ihq :
  map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q)
rw :
  map (↑g : P →+* Q) (m • p + m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₁ :
  HAdd.hAdd (α := Q[X]) (map (↑g : P →+* Q) (m • p)) (map (↑g : P →+* Q) (m • q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₂ :
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
      map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₃ :
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
      HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
⊢ map (↑g : P →+* Q) (m • (p + q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
have rw₄ : HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q) =
  HSMul.hSMul (α := M) ((MonoidHom.id M : (a : M) → M) m : M)
    (HAdd.hAdd (α := Q[X]) (map (↑g : P →+* Q) p) (map (↑g : P →+* Q) q))
Tactic: rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]