Theorem: MvPolynomial.sum_monomial_ne_zero_of_exists_mem_ne_zero (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
h : ∃ s, ∃ (_ : s ∈ S), f s ≠ 0
⊢ ∑ s ∈ S, (monomial s) (f s) ≠ 0
Tactic:
classical
simp only [← support_eq_empty, support_sum_monomial_eq, Ne]
rcases h with ⟨s, h_S, h_s⟩
exact ne_empty_of_mem (mem_filter.mpr ⟨h_S, h_s⟩)
State after:
no goals

State before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
h : ∃ s, ∃ (_ : s ∈ S), f s ≠ 0
⊢ ∑ s ∈ S, (monomial s) (f s) ≠ 0
Tactic:
simp only [← support_eq_empty, support_sum_monomial_eq, Ne]
State after:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
h : ∃ s, ∃ (_ : s ∈ S), f s ≠ 0
⊢ ¬filter (fun v => ¬f v = 0) S = ∅

State before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
h : ∃ s, ∃ (_ : s ∈ S), f s ≠ 0
⊢ ¬filter (fun v => ¬f v = 0) S = ∅
Tactic:
rcases h with ⟨s, h_S, h_s⟩
State after:
case intro.intro
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
s : ι →₀ ℕ
h_S : s ∈ S
h_s : f s ≠ 0
⊢ ¬filter (fun v => ¬f v = 0) S = ∅

State before:
case intro.intro
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
s : ι →₀ ℕ
h_S : s ∈ S
h_s : f s ≠ 0
⊢ ¬filter (fun v => ¬f v = 0) S = ∅
Tactic:
exact ne_empty_of_mem (mem_filter.mpr ⟨h_S, h_s⟩)
State after:
no goals