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

State before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
Tactic:
letI := Classical.decEq ι
State after:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S

State before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
Tactic:
induction' S using Finset.induction with s S hs hsi
State after:
case empty
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ ∅, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) ∅

case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ (∑ v ∈ insert s S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) (insert s S)

State before:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ (∑ v ∈ insert s S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) (insert s S)
Tactic:
rw [Finset.sum_insert hs, support_add_eq]
State after:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ ((monomial s) (f s)).support ∪ (∑ x ∈ S, (monomial x) (f x)).support = filter (fun v => f v ≠ 0) (insert s S)

case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ Disjoint ((monomial s) (f s)).support (∑ x ∈ S, (monomial x) (f x)).support

State before:
case empty
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ ∅, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) ∅
Tactic:
simp
State after:
no goals

State before:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ ((monomial s) (f s)).support ∪ (∑ x ∈ S, (monomial x) (f x)).support = filter (fun v => f v ≠ 0) (insert s S)
Tactic:
rw [hsi, filter_insert, support_monomial]
State after:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ (if f s = 0 then ∅ else {s}) ∪ filter (fun v => f v ≠ 0) S =
    if f s ≠ 0 then insert s (filter (fun v => f v ≠ 0) S) else filter (fun v => f v ≠ 0) S

State before:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ (if f s = 0 then ∅ else {s}) ∪ filter (fun v => f v ≠ 0) S =
    if f s ≠ 0 then insert s (filter (fun v => f v ≠ 0) S) else filter (fun v => f v ≠ 0) S
Tactic:
split_ifs with h h' <;> simp [h, insert_eq]
State after:
case pos
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
h : f s = 0
h' : f s ≠ 0
⊢ False

State before:
case pos
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
h : f s = 0
h' : f s ≠ 0
⊢ False
Tactic:
exact h' h
State after:
no goals

State before:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ Disjoint ((monomial s) (f s)).support (∑ x ∈ S, (monomial x) (f x)).support
Tactic:
apply disjoint_of_subset_left support_monomial_subset
State after:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ Disjoint {s} (∑ x ∈ S, (monomial x) (f x)).support

State before:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ Disjoint {s} (∑ x ∈ S, (monomial x) (f x)).support
Tactic:
simp [hsi, hs]
State after:
no goals