awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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)
⊢ 0 ∈ s

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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)
⊢ 0 ∈ s

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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)
neg neg₁ neg₂ 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)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)

Tactic:
rwa [zero_add] at this

Premises used: zero_add
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
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
⊢ eval₂ f v p ∈ 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

Premises used: map_zero, zero_add, MvPolynomial.eval₂_add, MvPolynomial.coeff_add, MvPolynomial.coeff_monomial, MvPolynomial.eval₂_monomial, ZeroMemClass.zero_mem, OfNat.ofNat, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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)
replace₁ :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)), eval₂ f v p ∈ s
replace₂ : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
replace₃ replace₄ :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)), eval₂ f v 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

Premises used: map_zero, zero_add, MvPolynomial.eval₂_add, MvPolynomial.coeff_add, MvPolynomial.coeff_monomial, MvPolynomial.eval₂_monomial, ZeroMemClass.zero_mem, OfNat.ofNat, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
σ : Type u_1
S : Type u_2
subS : Type u_3
inst : CommSemiring S
inst_1 : SetLike subS S
inst_2 : SubsemiringClass subS S
p : MvPolynomial σ S
s : subS
hs : ∀ i ∈ p.support, coeff i p ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
⊢ Membership.mem.{u_2, u_3} (α := S) s ((eval v : (a : MvPolynomial σ S) → S) p : S)

Tactic:
eval₂_mem hs hv

Premises used: Multiset.sum, Multiset.foldr, Set.Mem, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_mem, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
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:
simp [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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 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 ((⇑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 ((⇑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 ((⇑C : (a : S) → MvPolynomial σ S) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p + q) :
          MvPolynomial σ S) :
      T)

Tactic:
simp [hp, hq]
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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)
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)
⊢ 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)

Tactic:
cases i
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
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)
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:
simp [h]
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
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)
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:
simp [h]
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ S) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S))
    (map (algebraMap R S))

Tactic:
rfl

Premises used: MvPolynomial.map, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
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))
⊢ Eq (α := R →+* MvPolynomial σ S) (algebraMap R (MvPolynomial σ S))
    (@RingHom.comp _ (MvPolynomial σ R) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) (algebraMap R (MvPolynomial σ R)))

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
x : R
m_1 : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S) (coeff m_1 ((algebraMap R (MvPolynomial σ S) : (a : R) → MvPolynomial σ S) x))
    (coeff m_1
      ((@RingHom.comp _ (MvPolynomial σ R) _ _ Semiring.toNonAssocSemiring _
            (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) (algebraMap R (MvPolynomial σ R)) :
          (a : R) → MvPolynomial σ S)
        x))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
inst_3 : FaithfulSMul R S
⊢ FaithfulSMul (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
(faithfulSMul_iff_algebraMap_injective ..).mpr
    (map_injective _ <| FaithfulSMul.algebraMap_injective ..)

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, MvPolynomial.map_injective, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
⊢ (⇑(expand p) : (a : MvPolynomial σ R) → MvPolynomial σ R) =
    eval₂ C (HPow.hPow (α := (s : σ) → MvPolynomial σ R) (fun (s : σ) ↦ X s) p)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
r : R
⊢ Eq (α := MvPolynomial σ R)
    ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r) : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
eval₂Hom_C _ _ _

Premises used: MvPolynomial.eval₂Hom_C
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
i : σ
⊢ (expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) = HPow.hPow (α := MvPolynomial σ R) (X i) p

Tactic:
eval₂Hom_X' _ _ _

Premises used: MvPolynomial.eval₂Hom_X'
-- Module: Mathlib.Algebra.MvPolynomial.Expand
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)
h : ∀ i ∈ d.support, HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1
⊢ 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)

Tactic:
rw [expand, bind₁_monomial, monomial_eq, Finsupp.prod_of_support_subset _ Finsupp.support_smul]

Premises used: Finsupp.prod_of_support_subset, MvPolynomial.expand, Finsupp.support_smul, MvPolynomial.monomial_eq, MvPolynomial.bind₁_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ 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:
simp [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ ∀ i ∈ d.support, HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
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)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (expand 0)
    (AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval 1))

Tactic:
ext1 i
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R) ((expand 0 : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) ((eval 1 : (a : MvPolynomial σ R) → R) f) : MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
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)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (expand 1) (AlgHom.id R (MvPolynomial σ R))

Tactic:
ext1 i
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPolynomial σ R
⊢ (expand 1 : (a : MvPolynomial σ R) → MvPolynomial σ R) f = f

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p q : ℕ
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)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (expand (p * q)) (AlgHom.comp (expand p) (expand q))

Tactic:
ext1 i
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p q : ℕ
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:
simp [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p q : ℕ
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R) ((expand (p * q) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)
    ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((expand q : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) :
      MvPolynomial σ R)

Tactic:
DFunLike.congr_fun (expand_mul_eq_comp p q) φ

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.expand_mul_eq_comp, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Expand
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))
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)
⊢ coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = coeff m φ

Tactic:
induction φ using induction_on'
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
m 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:
simp [*, nsmul_right_inj hp]

Premises used: nsmul_right_inj