awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : σ
hi : i ∈ d.support
hgi : g i = 0
rw : Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0

Tactic:
rw [hgi, zero_pow]

Premises used: zero_pow
-- 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 : σ
hi : i ∈ d.support
hgi : g i = 0
rwa rwa₁ rwa₂ rwa₃ : i ∈ d.support
⊢ Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
rwa [← Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
inst_2 : Algebra R S₂
f : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, f i = 0
⊢ Eq.{w + 1} (α := S₂) ((aeval f : (a : MvPolynomial σ R) → S₂) φ : S₂) (0 : S₂)

Tactic:
eval₂Hom_eq_zero _ _ _ h

Premises used: MvPolynomial.eval₂Hom_eq_zero
-- 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₁
ι : Type u_2
s : Finset ι
φ : ι → MvPolynomial σ R
⊢ Eq.{v + 1} (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) (∑ i ∈ s, φ i) : S₁)
    (∑ i ∈ s, (aeval f : (a : MvPolynomial σ R) → S₁) (φ i) : S₁)

Tactic:
map_sum (MvPolynomial.aeval f) _ _

Premises used: MvPolynomial.aeval, map_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₁
ι : Type u_2
s : Finset ι
φ : ι → MvPolynomial σ R
⊢ Eq.{v + 1} (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) (∏ i ∈ s, φ i) : S₁)
    (∏ i ∈ s, (aeval f : (a : MvPolynomial σ R) → S₁) (φ i) : S₁)

Tactic:
map_prod (MvPolynomial.aeval f) _ _

Premises used: MvPolynomial.aeval, map_prod
-- 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₁
⊢ Eq (α := Subalgebra R S₁) (Algebra.adjoin R (range f)) (AlgHom.range (aeval f))

Tactic:
simp only [← Algebra.map_top, ← MvPolynomial.adjoin_range_X, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, MvPolynomial.aeval_X]

Premises used: Set.range_comp, MvPolynomial.aeval_X, MvPolynomial.adjoin_range_X, AlgHom.map_adjoin, Function.comp_def, Algebra.map_top
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
s : Set S₁
rw :
  Eq (α := Subalgebra R S₁) (Algebra.adjoin R s)
    (Algebra.adjoin R (range (ι := { x : S₁ // x ∈ s }) (Subtype.val (p := fun (x : S₁) ↦ x ∈ s))))
rw₁ rw₂ : Eq (α := Subalgebra R S₁) (Algebra.adjoin R s) (Algebra.adjoin R s)
⊢ Eq (α := Subalgebra R S₁) (Algebra.adjoin R s)
    (AlgHom.range (A := MvPolynomial.{v, u} { x : S₁ // x ∈ s } R) (aeval (Subtype.val (p := fun (x : S₁) ↦ x ∈ s))))

Tactic:
rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]

Premises used: Subtype.range_coe, Algebra.adjoin_range_eq_range_aeval
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
S : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring S
inst_3 : CommSemiring A
inst_4 : CommSemiring B
inst_5 : Algebra S R
inst_6 : Algebra S A
inst_7 : Algebra S B
f : R →ₐ[S] A
X : σ → A
r : S
⊢ OneHom.toFun (M := MvPolynomial σ R)
      (↑(↑(eval₂Hom (↑f : R →+* A) X) : MvPolynomial σ R →* A) : OneHom (MvPolynomial σ R) A)
      ((algebraMap S (MvPolynomial σ R) : (a : S) → MvPolynomial σ R) r) =
    (algebraMap S A : (a : S) → A) r

Tactic:
simp [IsScalarTower.algebraMap_eq S R (MvPolynomial σ R), algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, MvPolynomial.algebraMap_eq, MvPolynomial
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
A : Type u_3
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra S R
inst_4 : Algebra S A
g : R →ₐ[S] A
y : σ → A
i : σ
⊢ (aevalTower g y : (a : MvPolynomial σ R) → A) (X i) = y i

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
σ : Type u_1
inst : CommSemiring R
S : Type u_2
A : Type u_3
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra S R
inst_4 : Algebra S A
g : R →ₐ[S] A
y : σ → A
x : R
⊢ Eq.{u_3 + 1} (α := A)
    ((aevalTower g y : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R) : A)
    ((g : (a : R) → A) x : A)

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
σ : Type u_1
inst : CommSemiring R
S : Type u_2
A : Type u_3
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra S R
inst_4 : Algebra S A
g : R →ₐ[S] A
y : σ → A
n : ℕ
inst_5 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := A) ((aevalTower g y : (a : MvPolynomial σ R) → A) (OfNat.ofNat n) : A) (OfNat.ofNat n : A)

Tactic:
_root_.map_ofNat _ _

Premises used: map_ofNat
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
A : Type u_3
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra S R
inst_4 : Algebra S A
g : R →ₐ[S] A
y : σ → A
⊢ Eq (α := R →+* A) (RingHom.comp (↑(aevalTower g y) : MvPolynomial σ R →+* A) C) (↑g : R →+* A)

Tactic:
RingHom.ext <| aevalTower_C _ _

Premises used: MvPolynomial.aevalTower_C, RingHom.ext
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
A : Type u_3
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra S R
inst_4 : Algebra S A
g : R →ₐ[S] A
y : σ → A
x : R
⊢ Eq.{u_3 + 1} (α := A)
    ((aevalTower g y : (a : MvPolynomial σ R) → A)
        ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R) :
      A)
    ((g : (a : R) → A) x : A)

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
σ : Type u_1
inst : CommSemiring R
S : Type u_2
A : Type u_3
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra S R
inst_4 : Algebra S A
g : R →ₐ[S] A
y : σ → A
⊢ Eq (α := R →+* A)
    (@RingHom.comp _ _ _ _ nonAssocSemiring _ (↑(aevalTower g y) : MvPolynomial σ R →+* A)
      (algebraMap R (MvPolynomial σ R)))
    (↑g : R →+* A)

Tactic:
aevalTower_comp_C _ _

Premises used: MvPolynomial.aevalTower_comp_C, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
A : Type u_3
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra S R
inst_4 : Algebra S A
g : R →ₐ[S] A
y : σ → A
x : R
⊢ Eq.{u_3 + 1} (α := A)
    ((aevalTower g y : (a : MvPolynomial σ R) → A)
        ((IsScalarTower.toAlgHom S R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R) :
      A)
    ((g : (a : R) → A) x : A)

Tactic:
aevalTower_algebraMap _ _ _

Premises used: MvPolynomial.aevalTower_algebraMap
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
A : Type u_3
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : Algebra S R
inst_4 : Algebra S A
g : R →ₐ[S] A
y : σ → A
⊢ (aevalTower g y).comp (IsScalarTower.toAlgHom S R (MvPolynomial σ R)) = g

Tactic:
AlgHom.coe_ringHom_injective <| aevalTower_comp_algebraMap _ _

Premises used: AlgHom.coe_ringHom_injective, MvPolynomial.aevalTower_comp_algebraMap
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
σ : Type u_1
S : Type u_2
inst : CommSemiring S
h :
  ∀ (x : σ → S) (i : σ),
    Eq.{u_2 + 1} (α := S) ((aevalTower (AlgHom.id S S) x : (a : MvPolynomial σ S) → S) (X i) : S)
      ((aeval x : (a : MvPolynomial σ S) → S) (X i) : S)
⊢ Eq (α := (X : σ → S) → MvPolynomial σ S →ₐ[S] S) (aevalTower (AlgHom.id S S)) aeval

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
σ : Type u_1
S : Type u_2
inst : CommSemiring S
x : σ → S
i : σ
⊢ Eq.{u_2 + 1} (α := S) ((aevalTower (AlgHom.id S S) x : (a : MvPolynomial σ S) → S) (X i) : S)
    ((aeval x : (a : MvPolynomial σ S) → S) (X i) : S)

Tactic:
simp only [aevalTower_X, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.aevalTower_X
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
σ : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring A
inst_2 : Algebra S A
h :
  ∀ (x : σ → A) (i : σ),
    Eq.{u_3 + 1} (α := A) ((aevalTower (Algebra.ofId S A) x : (a : MvPolynomial σ S) → A) (X i) : A)
      ((aeval x : (a : MvPolynomial σ S) → A) (X i) : A)
⊢ Eq (α := (X : σ → A) → MvPolynomial σ S →ₐ[S] A) (aevalTower (Algebra.ofId S A)) aeval

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
σ : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring A
inst_2 : Algebra S A
x : σ → A
i : σ
⊢ Eq.{u_3 + 1} (α := A) ((aevalTower (Algebra.ofId S A) x : (a : MvPolynomial σ S) → A) (X i) : A)
    ((aeval x : (a : MvPolynomial σ S) → A) (X i) : A)

Tactic:
simp only [aeval_X, aevalTower_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.aevalTower_X
-- 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
i : σ →₀ ℕ
pos : ∀ (hi : i ∈ p.support), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
neg : ∀ (hi : i ∉ p.support), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)

Tactic:
by_cases hi : i ∈ p.support

Premises used: MvPolynomial.support
-- 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
i : σ →₀ ℕ
hi : i ∈ p.support
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)

Tactic:
hs i hi
-- 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
i : σ →₀ ℕ
hi : i ∈ p.support
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)

Tactic:
exact hs i hi
-- 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
i : σ →₀ ℕ
hi : i ∉ p.support
neg : 0 ∈ s
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)

Tactic:
rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]

Premises used: MvPolynomial.notMem_support_iff, RingHom.map_zero, Iff.mp
-- 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
i : σ →₀ ℕ
hi : i ∉ p.support
⊢ 0 ∈ s

Tactic:
zero_mem s

Premises used: Set.Mem, 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 : 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
i : σ →₀ ℕ
hi : i ∉ p.support
⊢ 0 ∈ s

Tactic:
exact zero_mem s

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 : 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
⊢ ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)

Tactic:
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
-- 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
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
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:
simpa using hs 0

Premises used: OfNat.ofNat
-- 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)
monomial_add :
  HMul.hMul (α := S) (β := S) ((f_1 : (a : R) → S) b : S) (a.prod fun (n : σ) (e : ℕ) ↦ v n ^ e : S) + eval₂ f_1 v f ∈ s
⊢ eval₂ f_1 v (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f) ∈ s

Tactic:
rw [eval₂_add, eval₂_monomial]

Premises used: MvPolynomial.eval₂_add, MvPolynomial.eval₂_monomial
-- 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)
⊢ HMul.hMul (α := S) (β := S) ((f_1 : (a : R) → S) b : S) (a.prod fun (n : σ) (e : ℕ) ↦ v n ^ e : S) + eval₂ f_1 v f ∈ s

Tactic:
add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)

Premises used: pow_mem, AddMemClass.add_mem, DFunLike.coe, prod_mem, MulMemClass.mul_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)
monomial_add : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) b : S)
monomial_add₁ : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
⊢ HMul.hMul (α := S) (β := S) ((f_1 : (a : R) → S) b : S) (a.prod fun (n : σ) (e : ℕ) ↦ v n ^ e : S) + eval₂ f_1 v f ∈ s

Tactic:
refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)

Premises used: pow_mem, AddMemClass.add_mem, prod_mem, MulMemClass.mul_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)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) b : S)

Tactic:
simpa [MvPolynomial.notMem_support_iff.1 ha] using hs a

Premises used: MvPolynomial.notMem_support_iff, Iff.mp
-- 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)
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)

Tactic:
have := hs i
-- 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)
i : σ →₀ ℕ
this :
  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)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) ((if a = i then b else 0) + coeff i f) : S)

Tactic:
rw [coeff_add, coeff_monomial] at this

Premises used: MvPolynomial.coeff_add, MvPolynomial.coeff_monomial
-- 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)
i : σ →₀ ℕ
this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) ((if a = i then b else 0) + coeff i f) : S)
pos :
  ∀ (h : a = i) (this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (b + coeff i f) : S)),
    Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
neg :
  ∀ (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)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)

Tactic:
split_ifs at this with h
-- 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) (b + coeff i f) : S)
pos :
  ∀ (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)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)

Tactic:
subst h
-- 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)
pos : 0 ∈ s
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff a f) : S)

Tactic:
rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]

Premises used: MvPolynomial.notMem_support_iff, map_zero, Iff.mp