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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ ((homogeneousComponent n) p).support = filter (fun d => (d.sum fun x m => m) = n) p.support
Tactic:
ext x
State after:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ x ∈ ((homogeneousComponent n) p).support ↔ x ∈ filter (fun d => (d.sum fun x m => m) = n) p.support

State before:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ x ∈ ((homogeneousComponent n) p).support ↔ x ∈ filter (fun d => (d.sum fun x m => m) = n) p.support
Tactic:
simp only [mem_support_iff, ne_eq, mem_filter]
State after:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ ¬coeff x ((homogeneousComponent n) p) = 0 ↔ ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n

State before:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ ¬coeff x ((homogeneousComponent n) p) = 0 ↔ ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
Tactic:
refine ⟨fun hx ↦ ⟨fun h ↦ hx <| by simp [coeff_homogeneousComponent, h], ?_⟩,
  fun ⟨h₁, h₂⟩ ↦ fun h ↦ h₁ ?_⟩
State after:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬coeff x ((homogeneousComponent n) p) = 0
⊢ (x.sum fun x m => m) = n

case a.refine_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
x✝ : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
h₁ : ¬coeff x p = 0
h₂ : (x.sum fun x m => m) = n
h : coeff x ((homogeneousComponent n) p) = 0
⊢ coeff x p = 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬coeff x ((homogeneousComponent n) p) = 0
h : coeff x p = 0
⊢ coeff x ((homogeneousComponent n) p) = 0
Tactic:
simp [coeff_homogeneousComponent, h]
State after:
no goals

State before:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬coeff x ((homogeneousComponent n) p) = 0
⊢ (x.sum fun x m => m) = n
Tactic:
simp only [coeff_homogeneousComponent, ite_eq_right_iff] at hx
State after:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬(degree x = n → coeff x p = 0)
⊢ (x.sum fun x m => m) = n

State before:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬(degree x = n → coeff x p = 0)
⊢ (x.sum fun x m => m) = n
Tactic:
contrapose! hx
State after:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
⊢ degree x = n → coeff x p = 0

State before:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
⊢ degree x = n → coeff x p = 0
Tactic:
intro h₁
State after:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
h₁ : degree x = n
⊢ coeff x p = 0

State before:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
h₁ : degree x = n
⊢ coeff x p = 0
Tactic:
contradiction
State after:
no goals

State before:
case a.refine_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
x✝ : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
h₁ : ¬coeff x p = 0
h₂ : (x.sum fun x m => m) = n
h : coeff x ((homogeneousComponent n) p) = 0
⊢ coeff x p = 0
Tactic:
simp only [coeff_homogeneousComponent, ite_eq_right_iff] at h
State after:
case a.refine_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
x✝ : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
h₁ : ¬coeff x p = 0
h₂ : (x.sum fun x m => m) = n
h : degree x = n → coeff x p = 0
⊢ coeff x p = 0

State before:
case a.refine_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
x✝ : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
h₁ : ¬coeff x p = 0
h₂ : (x.sum fun x m => m) = n
h : degree x = n → coeff x p = 0
⊢ coeff x p = 0
Tactic:
exact h h₂
State after:
no goals