awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
⊢ (f * single x r).support = image (fun (x_1 : G) ↦ x_1 * x) f.support
have refine : ∀ (y : G) (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) y),
  y ∈ (f * single x r).support
Tactic: refine subset_antisymm (support_mul_single_subset f _ _) fun y hy => ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) y
⊢ y ∈ (f * single x r).support
have obtain : ∀ (y : G) (yf : y ∈ f.support)
  (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) (y * x)),
  y * x ∈ (f * single x r).support
Tactic: obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by grind
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support
have h : ∀ (a : G), a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support
have h : ∀ (a : G), a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
Tactic: classical
    ext
    simp only [support_mul_single_eq_image f hr (IsRightRegular.all x),
      mem_image, mem_map, mulRightEmbedding_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support
have h : ∀ (a : G), a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support
have h : ∀ (a : G), a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support
Tactic: classical
    ext
    simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image,
      mem_map, mulLeftEmbedding_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : MulOneClass G
f : k[G]
⊢ Membership.mem (γ := Submodule k k[G]) (Submodule.span k ((fun (m : G) ↦ single m 1) '' (↑f.support : Set G))) f
have rw : Membership.mem (γ := Submodule k k[G]) (Finsupp.supported k k (↑f.support : Set G)) f
Tactic: rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : MulOneClass G
f : k[G]
rw : Membership.mem (γ := Submodule k k[G]) (Finsupp.supported k k (↑f.support : Set G)) f
⊢ Membership.mem (γ := Submodule k k[G]) (Submodule.span k ((fun (m : G) ↦ single m 1) '' (↑f.support : Set G))) f
have rw₁ : (↑f.support : Set G) ⊆ (↑f.support : Set G)
Tactic: rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
f : k[G]
⊢ Membership.mem (γ := Submodule k k[G]) (Submodule.span k ((fun (a : G) ↦ single a 1) '' (↑f.support : Set G))) f
have rw : Membership.mem (γ := Submodule k k[G]) (Finsupp.supported k k (↑f.support : Set G)) f
Tactic: rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
f : k[G]
rw : Membership.mem (γ := Submodule k k[G]) (Finsupp.supported k k (↑f.support : Set G)) f
⊢ Membership.mem (γ := Submodule k k[G]) (Submodule.span k ((fun (a : G) ↦ single a 1) '' (↑f.support : Set G))) f
have rw₁ : (↑f.support : Set G) ⊆ (↑f.support : Set G)
Tactic: rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.ToDirectSum (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
f g : M[ι]
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ (f * g).toDirectSum = f.toDirectSum * g.toDirectSum
have change : (to_hom : (a : M[ι]) → ⨁ (x : ι), M) (f * g) =
  HMul.hMul (α := ⨁ (x : ι), M) (β := ⨁ (x : ι), M) ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) f : ⨁ (x : ι), M)
    ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) g : ⨁ (x : ι), M)
Tactic: change to_hom (f * g) = to_hom f * to_hom g
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.ToDirectSum (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
f g : M[ι]
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ (to_hom : (a : M[ι]) → ⨁ (x : ι), M) (f * g) =
    HMul.hMul (α := ⨁ (x : ι), M) (β := ⨁ (x : ι), M) ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) f : ⨁ (x : ι), M)
      ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) g : ⨁ (x : ι), M)
have revert : ∀ (f g : M[ι]),
  (to_hom : (a : M[ι]) → ⨁ (x : ι), M) (f * g) =
    HMul.hMul (α := ⨁ (x : ι), M) (β := ⨁ (x : ι), M) ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) f : ⨁ (x : ι), M)
      ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) g : ⨁ (x : ι), M)
Tactic: revert f g
Cleared hypotheses: f, g
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.ToDirectSum (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (f g : M[ι]),
    (to_hom : (a : M[ι]) → ⨁ (x : ι), M) (f * g) =
      HMul.hMul (α := ⨁ (x : ι), M) (β := ⨁ (x : ι), M) ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) f : ⨁ (x : ι), M)
        ((to_hom : (a : M[ι]) → ⨁ (x : ι), M) g : ⨁ (x : ι), M)
have rw : AddMonoidHom.compr₂ AddMonoidHom.mul to_hom = (AddMonoidHom.comp AddMonoidHom.mul to_hom).compl₂ to_hom
Tactic: rw [AddMonoidHom.map_mul_iff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.ToDirectSum (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul to_hom = (AddMonoidHom.comp AddMonoidHom.mul to_hom).compl₂ to_hom
have hfg : ∀ (xi : ι) (xv : M) (yi : ι) (yv : M),
  Eq (α := ⨁ (x : ι), M)
    ((AddMonoidHom.comp
            (((AddMonoidHom.compr₂ AddMonoidHom.mul to_hom).comp (singleAddHom xi) : (a : M) → M[ι] →+ ⨁ (x : ι), M) xv)
            (singleAddHom yi) :
          (a : M) → ⨁ (x : ι), M)
        yv :
      ⨁ (x : ι), M)
    ((AddMonoidHom.comp
            ((((AddMonoidHom.comp AddMonoidHom.mul to_hom).compl₂ to_hom).comp (singleAddHom xi) :
                (a : M) → M[ι] →+ ⨁ (x : ι), M)
              xv)
            (singleAddHom yi) :
          (a : M) → ⨁ (x : ι), M)
        yv :
      ⨁ (x : ι), M)
Tactic: ext xi xv yi yv : 4
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.ToDirectSum (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra
have apply_fun : (f * g).toAddMonoidAlgebra.toDirectSum = (f.toAddMonoidAlgebra * g.toAddMonoidAlgebra).toDirectSum
Tactic: apply_fun AddMonoidAlgebra.toDirectSum
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.ToDirectSum (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
apply_fun : (f * g).toAddMonoidAlgebra.toDirectSum = (f.toAddMonoidAlgebra * g.toAddMonoidAlgebra).toDirectSum
⊢ (f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra
have inj : Function.Injective (α := AddMonoidAlgebra M ι) AddMonoidAlgebra.toDirectSum
Tactic: apply_fun AddMonoidAlgebra.toDirectSum
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.ToDirectSum (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective (α := AddMonoidAlgebra M ι) AddMonoidAlgebra.toDirectSum
have inj : Function.LeftInverse (α := AddMonoidAlgebra M ι) toAddMonoidAlgebra AddMonoidAlgebra.toDirectSum
Tactic: apply Function.LeftInverse.injective
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.ToDirectSum (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
inj : Function.LeftInverse (α := AddMonoidAlgebra M ι) toAddMonoidAlgebra AddMonoidAlgebra.toDirectSum
⊢ Function.Injective (α := AddMonoidAlgebra M ι) AddMonoidAlgebra.toDirectSum
have inj₁ : (⨁ (x : ι), M) → AddMonoidAlgebra M ι
Tactic: apply Function.LeftInverse.injective
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst : CommSemiring R
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a' : MvPolynomial σ R) =
    (monomial s : (a : R) → MvPolynomial σ R) (a * a')
have this : HMul.hMul (α := AddMonoidAlgebra.{u, u_1} R (σ →₀ ℕ)) (AddMonoidAlgebra.single 0 a) (AddMonoidAlgebra.single s a') =
  AddMonoidAlgebra.single (0 + s) (a * a')
Tactic: have := single_mul_single 0 s a a'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst : CommSemiring R
this :
  HMul.hMul (α := AddMonoidAlgebra.{u, u_1} R (σ →₀ ℕ)) (AddMonoidAlgebra.single 0 a) (AddMonoidAlgebra.single s a') =
    AddMonoidAlgebra.single (0 + s) (a * a')
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a' : MvPolynomial σ R) =
    (monomial s : (a : R) → MvPolynomial σ R) (a * a')
have this₁ : HMul.hMul (α := AddMonoidAlgebra.{u, u_1} R (σ →₀ ℕ)) (AddMonoidAlgebra.single 0 a) (AddMonoidAlgebra.single s a') =
  AddMonoidAlgebra.single s (a * a')
Tactic: rw [zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : IsEmpty σ
⊢ Surjective (α := R) (β := MvPolynomial σ R) (⇑C : (a : R) → MvPolynomial σ R)
have refine : ∀ (p : MvPolynomial σ R) (a : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((((C : (a : R) → MvPolynomial σ R) (p.toFun 0) : MvPolynomial σ R) : (a : σ →₀ ℕ) → R) a : R)
    ((p : (a : σ →₀ ℕ) → R) a : R)
Tactic: refine fun p => ⟨p.toFun 0, Finsupp.ext fun a => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((((C : (a : R) → MvPolynomial σ R) (p.toFun 0) : MvPolynomial σ R) : (a : σ →₀ ℕ) → R) a : R)
    ((p : (a : σ →₀ ℕ) → R) a : R)
have simp : p.toFun 0 = (p : (a : σ →₀ ℕ) → R) 0
Tactic: simp only [C_apply, ← single_eq_monomial, (Finsupp.ext isEmptyElim (α := σ) : a = 0),
    single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) (0 : MvPolynomial σ R) ↔ a = 0
have rw : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) 0 : MvPolynomial σ R) ↔
  a = 0
Tactic: rw [← map_zero C, C_inj]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
rw :
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) 0 : MvPolynomial σ R) ↔
    a = 0
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) (0 : MvPolynomial σ R) ↔ a = 0
have rw₁ : a = 0 ↔ a = 0
Tactic: rw [← map_zero C, C_inj]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) (↑n : MvPolynomial σ R)
have zero : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑0 : R)) (↑0 : MvPolynomial σ R)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
zero : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑0 : R)) (↑0 : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) (↑n : MvPolynomial σ R)
have succ : ∀ (n : ℕ),
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) (↑n : MvPolynomial σ R) →
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑(n + 1) : R)) (↑(n + 1) : MvPolynomial σ R)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
⊢ (C : (a : R) → MvPolynomial σ R) a = HSMul.hSMul (β := MvPolynomial σ R) a 1
have rw : (C : (a : R) → MvPolynomial σ R) a =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (1 : MvPolynomial σ R)
Tactic: rw [← C_mul', mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
rw :
  (C : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (1 : MvPolynomial σ R)
⊢ (C : (a : R) → MvPolynomial σ R) a = HSMul.hSMul (β := MvPolynomial σ R) a 1
have rw₁ : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
Tactic: rw [← C_mul', mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ (monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) e)
have rw : (monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
Tactic: rw [X_pow_eq_monomial, monomial_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst : CommSemiring R
rw :
  (monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
⊢ (monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) e)
have rw₁ : Eq (α := MvPolynomial σ R) ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
Tactic: rw [X_pow_eq_monomial, monomial_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst : CommSemiring R
rw :
  (monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R) ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
⊢ (monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) e)
have rw₂ : Eq (α := MvPolynomial σ R) ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
Tactic: rw [X_pow_eq_monomial, monomial_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ (monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (β := MvPolynomial σ R) (HPow.hPow (α := MvPolynomial σ R) (X n) e)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
have rw : (monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
    ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
Tactic: rw [X_pow_eq_monomial, monomial_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst : CommSemiring R
rw :
  (monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
⊢ (monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (β := MvPolynomial σ R) (HPow.hPow (α := MvPolynomial σ R) (X n) e)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
have rw₁ : Eq (α := MvPolynomial σ R) ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) (1 * a) : MvPolynomial σ R)
Tactic: rw [X_pow_eq_monomial, monomial_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst : CommSemiring R
rw :
  (monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R) ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) (1 * a) : MvPolynomial σ R)
⊢ (monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (β := MvPolynomial σ R) (HPow.hPow (α := MvPolynomial σ R) (X n) e)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
have rw₂ : Eq (α := MvPolynomial σ R) ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
Tactic: rw [X_pow_eq_monomial, monomial_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
a : R
n : ℕ
⊢ HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    (monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) a
have rw : HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
  (monomial (HAdd.hAdd (α := σ →₀ ℕ) 0 (Finsupp.single s n)) : (a : R) → MvPolynomial σ R) a
Tactic: rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
a : R
n : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    (monomial (HAdd.hAdd (α := σ →₀ ℕ) 0 (Finsupp.single s n)) : (a : R) → MvPolynomial σ R) a
⊢ HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    (monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) a
have rw₁ : HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
  HMul.hMul (α := MvPolynomial σ R) ((monomial 0 : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (HPow.hPow (α := MvPolynomial σ R) (X s) n)
Tactic: rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
a : R
n : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    (monomial (HAdd.hAdd (α := σ →₀ ℕ) 0 (Finsupp.single s n)) : (a : R) → MvPolynomial σ R) a
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    HMul.hMul (α := MvPolynomial σ R) ((monomial 0 : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n)
⊢ HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    (monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) a
have rw₂ : HMul.hMul (α := MvPolynomial σ R) ((monomial 0 : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
  HMul.hMul (α := MvPolynomial σ R) ((monomial 0 : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (HPow.hPow (α := MvPolynomial σ R) (X s) n)
Tactic: rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
a : R
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (X s) =
    (monomial (Finsupp.single s 1) : (a : R) → MvPolynomial σ R) a
have rw : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (X s) =
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X s) 1)
Tactic: rw [← C_mul_X_pow_eq_monomial, pow_one]