awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
S₁ : Type v
σ : Type u_1
inst : CommSemiring S₁
f : σ → S₁
⊢ (↑(aeval f) : MvPolynomial σ S₁ →+* S₁) = eval f

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, MonoidHomClass.toMonoidHom, MvPolynomial.eval, RingHomClass.toRingHom, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
S₁ : Type v
σ : Type u_1
inst : CommSemiring S₁
f : σ → S₁
⊢ Eq (α := (a : MvPolynomial σ S₁) → S₁) (⇑(aeval f) : (a : MvPolynomial σ S₁) → S₁)
    (⇑(eval f) : (a : MvPolynomial σ S₁) → S₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
s : σ
⊢ (aeval f : (a : MvPolynomial σ R) → S₁) (X s) = f s

Tactic:
eval₂_X _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_X, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
r : R
⊢ Eq.{v + 1} (α := S₁)
    ((aeval f : (a : MvPolynomial σ R) → S₁) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : S₁)
    ((algebraMap R S₁ : (a : R) → S₁) r : S₁)

Tactic:
eval₂_C _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_C, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
n : ℕ
inst_3 : n.AtLeastTwo
⊢ Eq.{v + 1} (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) (OfNat.ofNat n) : S₁) (OfNat.ofNat n : S₁)

Tactic:
map_ofNat _ _

Premises used: map_ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
φ : MvPolynomial σ R →ₐ[R] S₁
hf :
  ∀ (i : σ),
    Eq.{v + 1} (α := S₁) ((φ : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
      ((aeval (comp (β := MvPolynomial σ R) (⇑φ : (a : MvPolynomial σ R) → S₁) X) : (a : MvPolynomial σ R) → S₁) (X i) :
        S₁)
⊢ φ = aeval (comp (β := MvPolynomial σ R) (⇑φ : (a : MvPolynomial σ R) → S₁) X)

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
φ : MvPolynomial σ R →ₐ[R] S₁
i : σ
⊢ Eq.{v + 1} (α := S₁) ((φ : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
    ((aeval (comp (β := MvPolynomial σ R) (⇑φ : (a : MvPolynomial σ R) → S₁) X) : (a : MvPolynomial σ R) → S₁) (X i) :
      S₁)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (aeval X) (AlgHom.id R (MvPolynomial σ R))

Tactic:
(aeval_unique (AlgHom.id R _)).symm

Premises used: AlgHom.id, MvPolynomial.X, MvPolynomial.aeval_unique, Eq.symm, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (aeval X : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p

Tactic:
AlgHom.congr_fun aeval_X_left p

Premises used: MvPolynomial.aeval_X_left, AlgHom.congr_fun
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
B : Type u_2
inst_3 : CommSemiring B
inst_4 : Algebra R B
φ : S₁ →ₐ[R] B
hf :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := B) ((φ.comp (aeval f) : (a : MvPolynomial σ R) → B) (X i) : B)
      ((aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i) : (a : MvPolynomial σ R) → B) (X i) : B)
⊢ φ.comp (aeval f) = aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i)

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
B : Type u_2
inst_3 : CommSemiring B
inst_4 : Algebra R B
φ : S₁ →ₐ[R] B
i : σ
⊢ Eq.{u_2 + 1} (α := B) ((φ.comp (aeval f) : (a : MvPolynomial σ R) → B) (X i) : B)
    ((aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i) : (a : MvPolynomial σ R) → B) (X i) : B)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
B : Type u_2
inst_3 : CommSemiring B
inst_4 : Algebra R B
φ : S₁ →ₐ[R] B
p : MvPolynomial σ R
rw :
  Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((φ.comp (aeval f) : (a : MvPolynomial σ R) → B) p : B)
rw₁ :
  Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    (comp (β := S₁) (⇑φ : (a : S₁) → B) (⇑(aeval f) : (a : MvPolynomial σ R) → S₁) p : B)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i) : (a : MvPolynomial σ R) → B) p : B)

Tactic:
rw [← comp_aeval, AlgHom.coe_comp, comp_apply]

Premises used: MvPolynomial.comp_aeval, AlgHom.coe_comp, Function.comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
B : Type u_2
inst_3 : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
rw :
  Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval g : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((φ.comp (eval₂Hom (algebraMap R S₁) g) : (a : MvPolynomial σ R) → B) p : B)
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval g : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((eval₂Hom (φ.comp (algebraMap R S₁)) fun (i : σ) ↦ (φ : (a : S₁) → B) (g i) : (a : MvPolynomial σ R) → B) p : B)

Tactic:
rw [← comp_eval₂Hom]

Premises used: MvPolynomial.comp_eval₂Hom
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
B : Type u_2
inst_3 : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval g : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((φ.comp (eval₂Hom (algebraMap R S₁) g) : (a : MvPolynomial σ R) → B) p : B)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
a : LE.le (α := Subalgebra R S₁) (AlgHom.range (aeval f)) (Algebra.adjoin R (range f))
a₁ : LE.le (α := Subalgebra R S₁) (Algebra.adjoin R (range f)) (AlgHom.range (aeval f))
⊢ Eq (α := Subalgebra R S₁) (AlgHom.range (aeval f)) (Algebra.adjoin R (range f))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
a :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((AlgHom.toRingHom (aeval f) : (a : MvPolynomial σ R) → S₁) p : S₁)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]

Premises used: RingHom.coe_coe, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
a : R
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : S₁)

Tactic:
aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))

Premises used: Set.mem_range_self, Set.Mem, Subsemiring.subset_closure, Eq.rec, MvPolynomial.aeval_C, Or.inl, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
a : R
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : S₁)

Tactic:
exact aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p q : MvPolynomial σ R
hp :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
hq :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁)
a :
  Membership.mem (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    (HAdd.hAdd (α := S₁) (β := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
      ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁))
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) (p + q) : S₁)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p q : MvPolynomial σ R
hp :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
hq :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁)
⊢ Membership.mem (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    (HAdd.hAdd (α := S₁) (β := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
      ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁))

Tactic:
Subalgebra.add_mem _ hp hq

Premises used: Subalgebra.add_mem
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p q : MvPolynomial σ R
hp :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
hq :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁)
⊢ Membership.mem (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    (HAdd.hAdd (α := S₁) (β := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
      ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁))

Tactic:
exact Subalgebra.add_mem _ hp hq

Premises used: Subalgebra.add_mem
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
n : σ
h :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
a :
  Membership.mem (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    (HMul.hMul (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) (f n))
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) (p * X n) : S₁)

Tactic:
simp only [map_mul, aeval_X]

Premises used: MvPolynomial.aeval_X, map_mul
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
n : σ
h :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
⊢ Membership.mem (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    (HMul.hMul (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) (f n))

Tactic:
Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))

Premises used: Subalgebra.mul_mem, Set.mem_range_self, Algebra.subset_adjoin
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
n : σ
h :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
⊢ Membership.mem (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    (HMul.hMul (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) (f n))

Tactic:
exact Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))

Premises used: Subalgebra.mul_mem, Set.mem_range_self, Algebra.subset_adjoin
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
a :
  ∀ (a : R),
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : S₁)
a₁ :
  ∀ (p q : MvPolynomial σ R)
    (hp :
      Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
        ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁))
    (hq :
      Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
        ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁)),
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) (p + q) : S₁)
a₂ :
  ∀ (p : MvPolynomial σ R) (n : σ)
    (h :
      Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
        ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)),
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) (p * X n) : S₁)
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)

Tactic:
induction p using induction_on with
    | C a => exact aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))
    | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
    | mul_X p n h =>
      simp only [map_mul, aeval_X]
      exact Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))

Premises used: MvPolynomial.aeval_X, map_add, MvPolynomial.induction_on, map_mul, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
a : range f ⊆ (↑(AlgHom.range (aeval f)) : Set S₁)
⊢ LE.le (α := Subalgebra R S₁) (Algebra.adjoin R (range f)) (AlgHom.range (aeval f))

Tactic:
rw [Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
i : σ
⊢ (AlgHom.toRingHom (aeval f) : (a : MvPolynomial σ R) → S₁) (X i) = f i

Tactic:
aesop
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
i : σ
w : MvPolynomial σ R
h : (AlgHom.toRingHom (aeval f) : (a : MvPolynomial σ R) → S₁) (X i) = f i
⊢ f i ∈ (↑(AlgHom.range (aeval f)) : Set S₁)

Tactic:
use X i, by aesop

Premises used: MvPolynomial.X
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
hC :
  ∀ (x : R),
    Eq.{w + 1} (α := S₂) ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom f 0) C : (a : R) → S₂) x : S₂)
      ((RingHom.comp (β := MvPolynomial σ R) (f.comp constantCoeff) C : (a : R) → S₂) x : S₂)
hX :
  ∀ (i : σ),
    Eq.{w + 1} (α := S₂) ((eval₂Hom f 0 : (a : MvPolynomial σ R) → S₂) (X i) : S₂)
      ((f.comp constantCoeff : (a : MvPolynomial σ R) → S₂) (X i) : S₂)
⊢ Eq (α := MvPolynomial σ R →+* S₂) (eval₂Hom f 0) (f.comp constantCoeff)

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
x : R
⊢ Eq.{w + 1} (α := S₂) ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom f 0) C : (a : R) → S₂) x : S₂)
    ((RingHom.comp (β := MvPolynomial σ R) (f.comp constantCoeff) C : (a : R) → S₂) x : S₂)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
i : σ
⊢ Eq.{w + 1} (α := S₂) ((eval₂Hom f 0 : (a : MvPolynomial σ R) → S₂) (X i) : S₂)
    ((f.comp constantCoeff : (a : MvPolynomial σ R) → S₂) (X i) : S₂)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
⊢ Eq (α := MvPolynomial σ R →+* S₂) (eval₂Hom f fun (x : σ) ↦ 0) (f.comp constantCoeff)

Tactic:
eval₂Hom_zero f

Premises used: MvPolynomial.eval₂Hom_zero
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
p : MvPolynomial σ R
⊢ Eq.{w + 1} (α := S₂) ((eval₂Hom f 0 : (a : MvPolynomial σ R) → S₂) p : S₂)
    ((f : (a : R) → S₂) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S₂)

Tactic:
RingHom.congr_fun (eval₂Hom_zero f) p

Premises used: RingHom.congr_fun, MvPolynomial.eval₂Hom_zero
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
p : MvPolynomial σ R
⊢ Eq.{w + 1} (α := S₂) ((eval₂Hom f fun (x : σ) ↦ 0 : (a : MvPolynomial σ R) → S₂) p : S₂)
    ((f : (a : R) → S₂) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S₂)

Tactic:
eval₂Hom_zero_apply f p

Premises used: MvPolynomial.eval₂Hom_zero_apply
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
p : MvPolynomial σ R
⊢ eval₂ f 0 p = (f : (a : R) → S₂) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)

Tactic:
eval₂Hom_zero_apply _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂Hom_zero_apply, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
p : MvPolynomial σ R
⊢ eval₂ f (fun (x : σ) ↦ 0) p = (f : (a : R) → S₂) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)

Tactic:
eval₂_zero_apply f p

Premises used: MvPolynomial.eval₂_zero_apply
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
p : MvPolynomial σ R
⊢ Eq.{v + 1} (α := S₁) ((aeval 0 : (a : MvPolynomial σ R) → S₁) p : S₁)
    ((algebraMap R S₁ : (a : R) → S₁) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S₁)

Tactic:
eval₂Hom_zero_apply (algebraMap R S₁) p

Premises used: Algebra.algebraMap, MvPolynomial.eval₂Hom_zero_apply
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
p : MvPolynomial σ R
⊢ Eq.{v + 1} (α := S₁) ((aeval fun (x : σ) ↦ 0 : (a : MvPolynomial σ R) → S₁) p : S₁)
    ((algebraMap R S₁ : (a : R) → S₁) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S₁)

Tactic:
aeval_zero p

Premises used: MvPolynomial.aeval_zero
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R →+* R) (eval 0) constantCoeff

Tactic:
eval₂Hom_zero _

Premises used: MvPolynomial.coeff, MvPolynomial.eval, MvPolynomial.eval₂Hom_zero, MvPolynomial.constantCoeff
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R →+* R) (eval fun (x : σ) ↦ 0) constantCoeff

Tactic:
eval₂Hom_zero _

Premises used: MvPolynomial.coeff, MvPolynomial.eval, MvPolynomial.eval₂Hom_zero, MvPolynomial.constantCoeff
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
g : σ → S₁
d : σ →₀ ℕ
r : R
⊢ (aeval g : (a : MvPolynomial σ R) → S₁) ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) =
    HMul.hMul (α := S₁) (β := S₁) ((algebraMap R S₁ : (a : R) → S₁) r : S₁) (d.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S₁)

Tactic:
eval₂Hom_monomial _ _ _ _

Premises used: MvPolynomial.eval₂Hom_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
rw :
  Eq.{w + 1} (α := S₂)
    (∑ x ∈ φ.support,
      (eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
        ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R))
    0
⊢ Eq.{w + 1} (α := S₂) ((eval₂Hom f g : (a : MvPolynomial σ R) → S₂) φ : S₂) (0 : S₂)

Tactic:
rw [φ.as_sum, map_sum]

Premises used: MvPolynomial.as_sum, map_sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ Eq.{w + 1} (α := S₂)
    (∑ x ∈ φ.support,
      (eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
        ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R))
    0

Tactic:
Finset.sum_eq_zero fun d hd => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
refine :
  ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support),
    Eq.{w + 1} (α := S₂)
      ((eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
          ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R) :
        S₂)
      (0 : S₂)
⊢ Eq.{w + 1} (α := S₂)
    (∑ x ∈ φ.support,
      (eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
        ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R))
    0

Tactic:
refine Finset.sum_eq_zero fun d hd => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ ∃ i ∈ d.support, g i = 0

Tactic:
h d (Finsupp.mem_support_iff.mp hd)

Premises used: Finsupp.mem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
obtain :
  ∀ (i : σ) (hi : i ∈ d.support) (hgi : g i = 0),
    Eq.{w + 1} (α := S₂)
      ((eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
          ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R) :
        S₂)
      (0 : S₂)
⊢ Eq.{w + 1} (α := S₂)
    ((eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
        ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R) :
      S₂)
    (0 : S₂)

Tactic:
obtain ⟨i, hi, hgi⟩ : ∃ i ∈ d.support, g i = 0 := h d (Finsupp.mem_support_iff.mp hd)

Premises used: Finsupp.mem_support_iff, Finsupp.support, Iff.mp