-- 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:
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
v : σ → S
hv : ∀ (i : σ), v i ∈ s
hs : ∀ (i : σ →₀ ℕ), f (coeff i p) ∈ s
⊢ eval₂ f v p ∈ s

Tactic:
induction' p using MvPolynomial.induction_on''' with a a b f ha _ ih

Result:
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

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

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
⊢ f✝ (coeff a f) ∈ s

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

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
this : f✝ (b + coeff a f) ∈ s
⊢ 0 ∈ s

Proof state:
case h_add_weak.refine_1
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 ∈ s

Tactic:
have := hs a

Result:
case h_add_weak.refine_1
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✝
      (coeff a
        ((let_fun this := (monomial a) b;
          this) +
          f)) ∈
    s
⊢ f✝ b ∈ 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
i : σ →₀ ℕ
h : a = i
this : f✝ (b + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s

Tactic:
subst 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
this : f✝ (b + coeff a f) ∈ s
⊢ f✝ (coeff a f) ∈ s

Proof state:
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 : σ →₀ ℕ
⊢ f (coeff i p) ∈ s

Tactic:
by_cases hi : i ∈ p.support

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
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

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
⊢ f (coeff i p) ∈ 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
⊢ (f✝ b * a.prod fun n e => v n ^ e) + eval₂ f✝ v f ∈ s

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

Result:
case h_add_weak.refine_1
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 ∈ s

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