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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ p.leadingTerms ≠ 0
Tactic:
classical
rw [leadingTerms_apply]
apply sum_monomial_ne_zero_of_exists_mem_ne_zero
simp only [exists_prop, mem_support_iff, Finset.mem_filter]
obtain ⟨f, hf, hf0⟩ := exists_coeff_ne_zero_totalDegree hp
exact ⟨f, ⟨hf0, hf⟩,  hf0⟩
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ p.leadingTerms ≠ 0
Tactic:
rw [leadingTerms_apply]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) ≠ 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) ≠ 0
Tactic:
apply sum_monomial_ne_zero_of_exists_mem_ne_zero
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, ∃ (_ : s ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support), coeff s p ≠ 0

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, ∃ (_ : s ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support), coeff s p ≠ 0
Tactic:
simp only [exists_prop, mem_support_iff, Finset.mem_filter]
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0
Tactic:
obtain ⟨f, hf, hf0⟩ := exists_coeff_ne_zero_totalDegree hp
State after:
case h.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
f : ι →₀ ℕ
hf : (f.sum fun x e => e) = p.totalDegree
hf0 : coeff f p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0

State before:
case h.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
f : ι →₀ ℕ
hf : (f.sum fun x e => e) = p.totalDegree
hf0 : coeff f p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0
Tactic:
exact ⟨f, ⟨hf0, hf⟩,  hf0⟩
State after:
no goals