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
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))
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))
⊢ 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) +
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) 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 : P[X]
n : ℕ
b : P
h :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)))
⊢ map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
have rw : map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
  HSMul.hSMul (β := Q[X]) m
    (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
Tactic: rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
-- 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]
n : ℕ
b : P
h :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)))
rw :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
⊢ map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
have rw₁ : map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X]) * m • HPow.hPow (α := P[X]) X (n + 1)) =
  HSMul.hSMul (β := Q[X]) m
    (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
Tactic: rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
-- 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]
n : ℕ
b : P
h :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)))
rw :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₁ :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X]) * m • HPow.hPow (α := P[X]) X (n + 1)) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
⊢ map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
have rw₂ : map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (m • HPow.hPow (α := P[X]) X (n + 1))) =
  HSMul.hSMul (β := Q[X]) m
    (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
Tactic: rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
-- 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]
n : ℕ
b : P
h :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)))
rw :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₁ :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X]) * m • HPow.hPow (α := P[X]) X (n + 1)) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₂ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (m • HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
⊢ map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
have rw₃ : map (↑g : P →+* Q)
    (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HSMul.hSMul (β := P[X]) m X ^ (n + 1))) =
  HSMul.hSMul (β := Q[X]) m
    (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
Tactic: rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
-- 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]
n : ℕ
b : P
h :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)))
rw :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₁ :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X]) * m • HPow.hPow (α := P[X]) X (n + 1)) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₂ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (m • HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₃ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HSMul.hSMul (β := P[X]) m X ^ (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
⊢ map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
have rw₄ : map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
  HSMul.hSMul (β := Q[X]) m
    (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
Tactic: rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
-- 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]
n : ℕ
b : P
h :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)))
rw :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₁ :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X]) * m • HPow.hPow (α := P[X]) X (n + 1)) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₂ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (m • HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₃ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HSMul.hSMul (β := P[X]) m X ^ (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₄ :
  map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
⊢ map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
have rw₅ : HMul.hMul (α := Q[X]) (map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)))
    (map (↑g : P →+* Q) (HPow.hPow (α := P[X]) X (n + 1))) =
  HSMul.hSMul (β := Q[X]) m
    (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
Tactic: rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
-- 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]
n : ℕ
b : P
h :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X n)))
rw :
  map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₁ :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X]) * m • HPow.hPow (α := P[X]) X (n + 1)) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₂ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (m • HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₃ :
  map (↑g : P →+* Q)
      (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HSMul.hSMul (β := P[X]) m X ^ (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₄ :
  map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) (m • b) : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
rw₅ :
  HMul.hMul (α := Q[X]) (map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)))
      (map (↑g : P →+* Q) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (β := Q[X]) m
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
⊢ map (↑g : P →+* Q) (m • HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
have rw₆ : HMul.hMul (α := Q[X]) (β := Q[X]) ((C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) : Q[X])
    (map (↑g : P →+* Q) (HPow.hPow (α := P[X]) X (n + 1))) =
  HSMul.hSMul (β := Q[X]) m
    (map (↑g : P →+* Q) (HMul.hMul (α := P[X]) ((C : (a : P) → P[X]) b : P[X]) (HPow.hPow (α := P[X]) X (n + 1))))
Tactic: rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) f : R[X])
    (f.sum fun (i : ℕ) (r : R) ↦ (monomial (i - k) : (a : R) → R[X]) ((↑(i.choose k) : R) * r) : R[X])
have dsimp : Eq (α := R[X]) (f.sum fun (x1 : ℕ) (x2 : R) ↦ (monomial (x1 - k) : (a : R) → R[X]) (x1.choose k • x2))
  (f.sum fun (i : ℕ) (r : R) ↦ (monomial (i - k) : (a : R) → R[X]) ((↑(i.choose k) : R) * r))
Tactic: dsimp [hasseDeriv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ coeff ((hasseDeriv k : (a : R[X]) → R[X]) f) n = (↑((n + k).choose k) : R) * f.coeff (n + k)
have rw : (if n + k - k = n then (↑((n + k).choose k) : R) * f.coeff (n + k) else 0) = (↑((n + k).choose k) : R) * f.coeff (n + k)
Tactic: rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n : ℕ
rw :
  (if n + k - k = n then (↑((n + k).choose k) : R) * f.coeff (n + k) else 0) =
    (↑((n + k).choose k) : R) * f.coeff (n + k)
⊢ coeff ((hasseDeriv k : (a : R[X]) → R[X]) f) n = (↑((n + k).choose k) : R) * f.coeff (n + k)
have h₀ : ∀ b ∈ f.support,
  b ≠ n + k → Eq.{u_1 + 1} (α := R) (coeff ((monomial (b - k) : (a : R) → R[X]) ((↑(b.choose k) : R) * f.coeff b)) n) 0
Tactic: rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n : ℕ
rw :
  (if n + k - k = n then (↑((n + k).choose k) : R) * f.coeff (n + k) else 0) =
    (↑((n + k).choose k) : R) * f.coeff (n + k)
h₀ :
  ∀ b ∈ f.support,
    b ≠ n + k →
      Eq.{u_1 + 1} (α := R) (coeff ((monomial (b - k) : (a : R) → R[X]) ((↑(b.choose k) : R) * f.coeff b)) n) 0
⊢ coeff ((hasseDeriv k : (a : R[X]) → R[X]) f) n = (↑((n + k).choose k) : R) * f.coeff (n + k)
have h₁ : n + k ∉ f.support →
  Eq.{u_1 + 1} (α := R)
    (coeff ((monomial (n + k - k) : (a : R) → R[X]) ((↑((n + k).choose k) : R) * f.coeff (n + k))) n) 0
Tactic: rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
⊢ Eq.{u_1 + 1} (α := R) (coeff ((monomial (i - k) : (a : R) → R[X]) ((↑(i.choose k) : R) * f.coeff i)) n) 0
have h₀ : (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
Tactic: rw [coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
⊢ (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
have pos : ∀ (hik : i < k), (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
Tactic: by_cases hik : i < k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
pos : ∀ (hik : i < k), (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
⊢ (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
have neg : ∀ (hik : ¬i < k), (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
Tactic: by_cases hik : i < k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ Eq (α := R[X]) ((hasseDeriv n : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
have rw : Eq.{u_1 + 1} (α := R[X])
  (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) 0
Tactic: rw [hasseDeriv_apply, sum_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) 0
have refine : ∀ (x : ℕ) (hx : x ∈ p.support),
  Eq (α := R[X]) ((monomial (x - n) : (a : R) → R[X]) ((↑(x.choose n) : R) * p.coeff x) : R[X]) (0 : R[X])
Tactic: refine Finset.sum_eq_zero fun x hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) r) : R[X])
    ((monomial (n - k) : (a : R) → R[X]) ((↑(n.choose k) : R) * r) : R[X])
have a : ∀ (i : ℕ),
  Eq.{u_1 + 1} (α := R) (coeff ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) r)) i)
    (coeff ((monomial (n - k) : (a : R) → R[X]) ((↑(n.choose k) : R) * r)) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) r)) i)
    (coeff ((monomial (n - k) : (a : R) → R[X]) ((↑(n.choose k) : R) * r)) i)
have a : ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
Tactic: simp only [hasseDeriv_coeff, coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
⊢ ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
have pos : ∀ (hnik : n = i + k),
  ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
Tactic: by_cases hnik : n = i + k