-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_mem {f : R →+* S} {p : MvPolynomial σ R} {s : subS}
    (hs : ∀ i ∈ p.support, f (p.coeff i) ∈ s) {v : σ → S} (hv : ∀ i, v i ∈ s) :
    MvPolynomial.eval₂ f v p ∈ s

Proof state:
case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
this : f✝ (b + coeff a f) ∈ s
⊢ 0 ∈ s

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
case h_C
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : R
hs : ∀ (i : σ →₀ ℕ), f (coeff i (C a)) ∈ s
⊢ eval₂ f v (C a) ∈ s

Tactic:
simpa using hs 0

Result:
no goals

Proof state:
case h_add_weak.refine_2
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
i : σ →₀ ℕ
this :
  f✝
      (coeff i
        ((let_fun this := (monomial a) b;
          this) +
          f)) ∈
    s
⊢ f✝ (coeff i f) ∈ s

Tactic:
rw [coeff_add, coeff_monomial] at this

Result:
case h_add_weak.refine_2
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
i : σ →₀ ℕ
this : f✝ ((if a = i then b else 0) + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s

Proof state:
case h_add_weak
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
⊢ eval₂ f✝ v
      ((let_fun this := (monomial a) b;
        this) +
        f) ∈
    s

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

Result:
case h_add_weak
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
⊢ (f✝ b * a.prod fun n e => v n ^ e) + eval₂ f✝ v f ∈ s

Proof state:
case h_add_weak.refine_2
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
i : σ →₀ ℕ
⊢ f✝ (coeff i f) ∈ s

Tactic:
have := hs i

Result:
case h_add_weak.refine_2
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
i : σ →₀ ℕ
this :
  f✝
      (coeff i
        ((let_fun this := (monomial a) b;
          this) +
          f)) ∈
    s
⊢ f✝ (coeff i f) ∈ s

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
hi : i ∉ p.support
⊢ 0 ∈ s

Tactic:
exact zero_mem s

Result:
no goals

Proof state:
case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
hi : i ∈ p.support
⊢ f (coeff i p) ∈ s

Tactic:
exact hs i hi

Result:
no goals

Proof state:
case h_add_weak.refine_2
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
i : σ →₀ ℕ
this : f✝ ((if a = i then b else 0) + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s

Tactic:
split_ifs at this with h

Result:
case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
i : σ →₀ ℕ
h : a = i
this : f✝ (b + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s

case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
i : σ →₀ ℕ
h : ¬a = i
this : f✝ (0 + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s