awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (b + coeff a f) : S)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff a f) : S)
have pos : 0 ∈ s
Tactic: rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h_1 : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
i : σ →₀ ℕ
h : ¬a = i
this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (0 + coeff i f) : S)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
have neg : ∀ (this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)),
  Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
Tactic: rwa [zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
⊢ eval₂ f v p ∈ s
have C : ∀ (a : R)
  (hs :
    ∀ (i : σ →₀ ℕ),
      Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i ((C : (a : R) → MvPolynomial σ R) a)) : S)),
  eval₂ f v ((C : (a : R) → MvPolynomial σ R) a) ∈ s
Tactic: induction p using MvPolynomial.monomial_add_induction_on with
  | C a =>
    simpa using hs 0
  | monomial_add a b f ha _ ih =>
    rw [eval₂_add, eval₂_monomial]
    refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
    · simpa [MvPolynomial.notMem_support_iff.1 ha] using hs a
    have := hs i
    rw [coeff_add, coeff_monomial] at this
    split_ifs at this with h
    · subst h
      rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]
      exact zero_mem _
    · rwa [zero_add] at this
Cleared hypotheses: p, hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
C :
  ∀ (a : R)
    (hs :
      ∀ (i : σ →₀ ℕ),
        Membership.mem.{u_2, u_3} (α := S) s
          ((f : (a : R) → S) (coeff i ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S)),
    eval₂ f v ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) ∈ s
⊢ eval₂ f v p ∈ s
have monomial_add : ∀ (a : σ →₀ ℕ) (b : R) (f_1 : MvPolynomial σ R) (ha : a ∉ f_1.support),
  b ≠ 0 →
    ∀
      (ih :
        ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i f_1) : S)),
          eval₂ f v f_1 ∈ s)
      (hs :
        ∀ (i : σ →₀ ℕ),
          Membership.mem.{u_2, u_3} (α := S) s
            ((f : (a : R) → S)
                (coeff i
                  (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
                    f_1)) :
              S)),
      eval₂ f v
          (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f_1) ∈
        s
Tactic: induction p using MvPolynomial.monomial_add_induction_on with
  | C a =>
    simpa using hs 0
  | monomial_add a b f ha _ ih =>
    rw [eval₂_add, eval₂_monomial]
    refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
    · simpa [MvPolynomial.notMem_support_iff.1 ha] using hs a
    have := hs i
    rw [coeff_add, coeff_monomial] at this
    split_ifs at this with h
    · subst h
      rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]
      exact zero_mem _
    · rwa [zero_add] at this
Cleared hypotheses: p, hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
v : σ → S
hv : ∀ (i : σ), v i ∈ s
⊢ eval₂ f v p ∈ s
have replace : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
Tactic: classical
  replace hs : ∀ i, f (p.coeff i) ∈ s := by
    intro i
    by_cases hi : i ∈ p.support
    · exact hs i hi
    · rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
      exact zero_mem s
  induction p using MvPolynomial.monomial_add_induction_on with
  | C a =>
    simpa using hs 0
  | monomial_add a b f ha _ ih =>
    rw [eval₂_add, eval₂_monomial]
    refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
    · simpa [MvPolynomial.notMem_support_iff.1 ha] using hs a
    have := hs i
    rw [coeff_add, coeff_monomial] at this
    split_ifs at this with h
    · subst h
      rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]
      exact zero_mem _
    · rwa [zero_add] at this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
v : σ → S
hv : ∀ (i : σ), v i ∈ s
replace : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
⊢ eval₂ f v p ∈ s
have replace₁ : ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)), eval₂ f v p ∈ s
Tactic: classical
  replace hs : ∀ i, f (p.coeff i) ∈ s := by
    intro i
    by_cases hi : i ∈ p.support
    · exact hs i hi
    · rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
      exact zero_mem s
  induction p using MvPolynomial.monomial_add_induction_on with
  | C a =>
    simpa using hs 0
  | monomial_add a b f ha _ ih =>
    rw [eval₂_add, eval₂_monomial]
    refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
    · simpa [MvPolynomial.notMem_support_iff.1 ha] using hs a
    have := hs i
    rw [coeff_add, coeff_monomial] at this
    split_ifs at this with h
    · subst h
      rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]
      exact zero_mem _
    · rwa [zero_add] at this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
T : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
i : σ ⊕ τ
h :
  Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) p : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S) :
      T)
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) (p * X i) : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p * X i) :
          MvPolynomial σ S) :
      T)
have mul_X : ∀ (val : σ),
  Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T)
        (p * X (Sum.inl val)) :
      T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p * X (Sum.inl val)) :
          MvPolynomial σ S) :
      T)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
T : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
i : σ ⊕ τ
h :
  Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) p : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S) :
      T)
mul_X :
  ∀ (val : σ),
    Eq.{u_3 + 1} (α := T)
      ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T)
          (p * X (Sum.inl val)) :
        T)
      ((aeval g : (a : MvPolynomial σ S) → T)
          ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              (p * X (Sum.inl val)) :
            MvPolynomial σ S) :
        T)
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) (p * X i) : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p * X i) :
          MvPolynomial σ S) :
      T)
have mul_X₁ : ∀ (val : τ),
  Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T)
        (p * X (Sum.inr val)) :
      T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p * X (Sum.inr val)) :
          MvPolynomial σ S) :
      T)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
T : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
g : σ → T
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) p : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S) :
      T)
have C : ∀ (r : R),
  Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T)
        ((C : (a : R) → MvPolynomial (σ ⊕ τ) R) r : MvPolynomial (σ ⊕ τ) R) :
      T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            ((C : (a : R) → MvPolynomial (σ ⊕ τ) R) r) :
          MvPolynomial σ S) :
      T)
Tactic: induction p using MvPolynomial.induction_on with
  | C r => simp [← IsScalarTower.algebraMap_apply]
  | add p q hp hq => simp [hp, hq]
  | mul_X p i h => cases i <;> simp [h]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
T : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
g : σ → T
C :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := T)
      ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T)
          ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ τ) R) r : MvPolynomial (σ ⊕ τ) R) :
        T)
      ((aeval g : (a : MvPolynomial σ S) → T)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ τ) R) r) :
            MvPolynomial σ S) :
        T)
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) p : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S) :
      T)
have add : ∀ (p q : MvPolynomial (σ ⊕ τ) R)
  (hp :
    Eq.{u_3 + 1} (α := T)
      ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) p : T)
      ((aeval g : (a : MvPolynomial σ S) → T)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p :
            MvPolynomial σ S) :
        T))
  (hq :
    Eq.{u_3 + 1} (α := T)
      ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) q : T)
      ((aeval g : (a : MvPolynomial σ S) → T)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              q :
            MvPolynomial σ S) :
        T)),
  Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) (p + q) : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p + q) :
          MvPolynomial σ S) :
      T)
Tactic: induction p using MvPolynomial.induction_on with
  | C r => simp [← IsScalarTower.algebraMap_apply]
  | add p q hp hq => simp [hp, hq]
  | mul_X p i h => cases i <;> simp [h]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R_1 : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R_1
e : ℕ
n m : σ_1
s : σ_1 →₀ ℕ
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := R →+* MvPolynomial σ S) (algebraMap R (MvPolynomial σ S))
    (@RingHom.comp _ (MvPolynomial σ R) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) (algebraMap R (MvPolynomial σ R)))
have a₃ : ∀ (x : R) (m : σ →₀ ℕ),
  Eq.{u_3 + 1} (α := S) (coeff m ((algebraMap R (MvPolynomial σ S) : (a : R) → MvPolynomial σ S) x))
    (coeff m
      ((@RingHom.comp _ (MvPolynomial σ R) _ _ Semiring.toNonAssocSemiring _
            (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) (algebraMap R (MvPolynomial σ R)) :
          (a : R) → MvPolynomial σ S)
        x))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ Eq (α := MvPolynomial σ R)
    ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial σ R)
    ((monomial (p • d) : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
have rw : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    (∏ i ∈ d.support, HPow.hPow (β := ℕ) (HPow.hPow (α := MvPolynomial σ R) (X i) p) ((d : (a : σ) → ℕ) i : ℕ) :
      MvPolynomial σ R) =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    (∏ x ∈ d.support, HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x) ((p • d : (a : σ) → ℕ) x : ℕ) : MvPolynomial σ R)
Tactic: rw [expand, bind₁_monomial, monomial_eq, Finsupp.prod_of_support_subset _ Finsupp.support_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (HPow.hPow (α := MvPolynomial σ R) (X i) p) ((d : (a : σ) → ℕ) i : ℕ) :
        MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      (∏ x ∈ d.support, HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x) ((p • d : (a : σ) → ℕ) x : ℕ) :
        MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial d : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial σ R)
    ((monomial (p • d) : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
have h : ∀ i ∈ d.support, HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1
Tactic: rw [expand, bind₁_monomial, monomial_eq, Finsupp.prod_of_support_subset _ Finsupp.support_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (expand 0)
    (AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval 1))
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial σ R) ((expand 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    ((AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval 1) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) :
      MvPolynomial σ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (expand 1) (AlgHom.id R (MvPolynomial σ R))
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial σ R) ((expand 1 : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p q : ℕ
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (expand (p * q)) (AlgHom.comp (expand p) (expand q))
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial σ R) ((expand (p * q) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    ((AlgHom.comp (expand p) (expand q) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = coeff m φ
have monomial : ∀ (u : σ →₀ ℕ) (a : R),
  Eq.{u_3 + 1} (α := R)
    (coeff (p • m)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial u : (a : R) → MvPolynomial σ R) a)))
    (coeff m ((monomial u : (a : R) → MvPolynomial σ R) a))
Tactic: induction φ using induction_on'
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
m : σ →₀ ℕ
monomial :
  ∀ (u : σ →₀ ℕ) (a : R),
    Eq.{u_3 + 1} (α := R)
      (coeff (p • m)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a)))
      (coeff m ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a))
⊢ coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = coeff m φ
have add : ∀ (p_1 q : MvPolynomial σ R),
  coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) p_1) = coeff m p_1 →
    coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) q) = coeff m q →
      coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (p_1 + q)) = coeff m (p_1 + q)
Tactic: induction φ using induction_on'
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = coeff m φ
have monomial : ∀ (u : σ →₀ ℕ) (a : R),
  Eq.{u_3 + 1} (α := R)
    (coeff (p • m)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((monomial u : (a : R) → MvPolynomial σ R) a)))
    (coeff m ((monomial u : (a : R) → MvPolynomial σ R) a))
Tactic: classical
  induction φ using induction_on' <;> simp [*, nsmul_right_inj hp]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
m : σ →₀ ℕ
monomial :
  ∀ (u : σ →₀ ℕ) (a : R),
    Eq.{u_3 + 1} (α := R)
      (coeff (p • m)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a)))
      (coeff m ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a))
⊢ coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = coeff m φ
have add : ∀ (p_1 q : MvPolynomial σ R),
  coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) p_1) = coeff m p_1 →
    coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) q) = coeff m q →
      coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (p_1 + q)) = coeff m (p_1 + q)
Tactic: classical
  induction φ using induction_on' <;> simp [*, nsmul_right_inj hp]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
⊢ Eq.{u_3 + 1} (α := R) (coeff.{u_3, u_1} (σ := σ) 0 ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff (HSMul.hSMul (β := σ →₀ ℕ) p 0) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
have rw : Eq.{u_3 + 1} (α := R) (coeff.{u_3, u_1} (σ := σ) 0 ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
  (coeff.{u_3, u_1} (σ := σ) 0 ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
⊢ coeff (HSMul.hSMul (β := σ →₀ ℕ) p 0) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = coeff 0 φ
have rw : coeff 0 φ = coeff 0 φ
Tactic: rw [coeff_expand_smul p hp]