[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
⊢ (sum l).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ l
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
⊢ (sum []).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ (sum (hd :: tl)).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
[PROOFSTEP]
simp only [List.sum_cons, Finset.union_comm]
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ (hd + sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
[PROOFSTEP]
refine' Finsupp.support_add.trans (Finset.union_subset_union _ IH)
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ hd.support ⊆ hd.support
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
⊢ (sum s).support ⊆ sup (map Finsupp.support s)
[PROOFSTEP]
induction s using Quot.inductionOn
[GOAL]
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a✝ : List (ι →₀ M)
⊢ (sum (Quot.mk Setoid.r a✝)).support ⊆ sup (map Finsupp.support (Quot.mk Setoid.r a✝))
[PROOFSTEP]
simpa only [Multiset.quot_mk_to_coe'', Multiset.coe_sum, Multiset.coe_map, Multiset.sup_coe, List.foldr_map] using
  List.support_sum_subset _
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (Finset.sum s id).support ⊆ sup s Finsupp.support
[PROOFSTEP]
classical convert Multiset.support_sum_subset s.1; simp
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (Finset.sum s id).support ⊆ sup s Finsupp.support
[PROOFSTEP]
convert Multiset.support_sum_subset s.1
[GOAL]
case h.e'_3.h.e'_4
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ Finset.sum s id = Multiset.sum s.val
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ l ↔ ∃ f x_1, x ∈ f.support
[PROOFSTEP]
simp only [Finset.sup_eq_union, List.foldr_map, Finsupp.mem_support_iff, exists_prop]
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ l ↔ ∃ f, f ∈ l ∧ ↑f x ≠ 0
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
⊢ x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ [] ↔ ∃ f, f ∈ [] ∧ ↑f x ≠ 0
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
hd : ι →₀ M
tl : List (ι →₀ M)
IH : x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ tl ↔ ∃ f, f ∈ tl ∧ ↑f x ≠ 0
⊢ x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ (hd :: tl) ↔ ∃ f, f ∈ hd :: tl ∧ ↑f x ≠ 0
[PROOFSTEP]
simp only [foldr, Function.comp_apply, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH, find?, mem_cons,
  exists_eq_or_imp]
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
s : Multiset (ι →₀ M)
x : ι
x✝ : List (ι →₀ M)
⊢ x ∈ sup (map Finsupp.support (Quot.mk Setoid.r x✝)) ↔ ∃ f x_1, x ∈ f.support
[PROOFSTEP]
simpa only [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.sup_coe, List.foldr_map] using
  List.mem_foldr_sup_support_iff
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl : Pairwise (_root_.Disjoint on Finsupp.support) l
⊢ (sum l).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ l
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hl : Pairwise (_root_.Disjoint on Finsupp.support) []
⊢ (sum []).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)
⊢ (sum (hd :: tl)).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
[PROOFSTEP]
simp only [List.pairwise_cons] at hl
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (sum (hd :: tl)).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
[PROOFSTEP]
simp only [List.sum_cons, List.foldr_cons, Function.comp_apply]
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (hd + sum tl).support = hd.support ⊔ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
[PROOFSTEP]
rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support (sum tl).support
[PROOFSTEP]
suffices _root_.Disjoint hd.support (tl.foldr (fun x y ↦ (Finsupp.support x ⊔ y)) ∅) by
  exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
this : _root_.Disjoint hd.support (foldr (fun x y => x.support ⊔ y) ∅ tl)
⊢ _root_.Disjoint hd.support (sum tl).support
[PROOFSTEP]
exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support (foldr (fun x y => x.support ⊔ y) ∅ tl)
[PROOFSTEP]
rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset, Finset.disjoint_sup_right]
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ ∀ ⦃i : Finset ι⦄, i ∈ toFinset (map (fun x => x.support) tl) → _root_.Disjoint hd.support (id i)
[PROOFSTEP]
intro f hf
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : f ∈ toFinset (map (fun x => x.support) tl)
⊢ _root_.Disjoint hd.support (id f)
[PROOFSTEP]
simp only [List.mem_toFinset, List.mem_map] at hf
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : ∃ a, a ∈ tl ∧ a.support = f
⊢ _root_.Disjoint hd.support (id f)
[PROOFSTEP]
obtain ⟨f, hf, rfl⟩ := hf
[GOAL]
case cons.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
f : ι →₀ M
hf : f ∈ tl
⊢ _root_.Disjoint hd.support (id f.support)
[PROOFSTEP]
exact hl.left _ hf
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
⊢ (sum s).support = sup (map Finsupp.support s)
[PROOFSTEP]
induction' s using Quot.inductionOn with a
[GOAL]
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs✝ : Pairwise (_root_.Disjoint on Finsupp.support) s
a : List (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) (Quot.mk Setoid.r a)
⊢ (sum (Quot.mk Setoid.r a)).support = sup (map Finsupp.support (Quot.mk Setoid.r a))
[PROOFSTEP]
obtain ⟨l, hl, hd⟩ := hs
[GOAL]
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
⊢ (sum (Quot.mk Setoid.r a)).support = sup (map Finsupp.support (Quot.mk Setoid.r a))
[PROOFSTEP]
suffices : a.Pairwise (_root_.Disjoint on Finsupp.support)
[GOAL]
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
this : List.Pairwise (_root_.Disjoint on Finsupp.support) a
⊢ (sum (Quot.mk Setoid.r a)).support = sup (map Finsupp.support (Quot.mk Setoid.r a))
[PROOFSTEP]
convert List.support_sum_eq a this
[GOAL]
case h.e'_2.h.e'_4
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
this : List.Pairwise (_root_.Disjoint on Finsupp.support) a
⊢ sum (Quot.mk Setoid.r a) = List.sum a
[PROOFSTEP]
simp only [Multiset.quot_mk_to_coe'', Multiset.coe_sum]
[GOAL]
case h.e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
this : List.Pairwise (_root_.Disjoint on Finsupp.support) a
⊢ sup (map Finsupp.support (Quot.mk Setoid.r a)) = List.foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ a
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case h.e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
this : List.Pairwise (_root_.Disjoint on Finsupp.support) a
⊢ sup (map Finsupp.support (Quot.mk Setoid.r a)) = List.foldr (fun x x_1 => x.support ⊔ x_1) ∅ a
[PROOFSTEP]
simp only [quot_mk_to_coe'', coe_map, sup_coe, ge_iff_le, Finset.le_eq_subset, Finset.sup_eq_union, Finset.bot_eq_empty,
  List.foldr_map]
[GOAL]
case this
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
⊢ List.Pairwise (_root_.Disjoint on Finsupp.support) a
[PROOFSTEP]
simp only [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.coe_eq_coe] at hl
[GOAL]
case this
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
hl : a ~ l
⊢ List.Pairwise (_root_.Disjoint on Finsupp.support) a
[PROOFSTEP]
exact hl.symm.pairwise hd fun _ _ h ↦ _root_.Disjoint.symm h
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ (Finset.sum s id).support = sup s Finsupp.support
[PROOFSTEP]
classical
suffices : s.1.Pairwise (_root_.Disjoint on Finsupp.support)
· convert Multiset.support_sum_eq s.1 this
  · exact (Finset.sum_val _).symm
· obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup :=
    by
    refine' ⟨s.toList, _, Finset.nodup_toList _⟩
    simp
  subst hl
  rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
    List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
  intro x y hxy
  exact symmetric_disjoint hxy
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ (Finset.sum s id).support = sup s Finsupp.support
[PROOFSTEP]
suffices : s.1.Pairwise (_root_.Disjoint on Finsupp.support)
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ (Finset.sum s id).support = sup s Finsupp.support
[PROOFSTEP]
convert Multiset.support_sum_eq s.1 this
[GOAL]
case h.e'_2.h.e'_4
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ Finset.sum s id = Multiset.sum s.val
[PROOFSTEP]
exact (Finset.sum_val _).symm
[GOAL]
case this
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
[PROOFSTEP]
obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup :=
  by
  refine' ⟨s.toList, _, Finset.nodup_toList _⟩
  simp
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ ∃ l, List.toFinset l = s ∧ List.Nodup l
[PROOFSTEP]
refine' ⟨s.toList, _, Finset.nodup_toList _⟩
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ List.toFinset (toList s) = s
[PROOFSTEP]
simp
[GOAL]
case this.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
l : List (ι →₀ M)
hl : List.toFinset l = s
hn : List.Nodup l
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
[PROOFSTEP]
subst hl
[GOAL]
case this.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : List.Nodup l
hs : Set.PairwiseDisjoint (↑(List.toFinset l)) Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) (List.toFinset l).val
[PROOFSTEP]
rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
  List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
[GOAL]
case this.intro.intro.hr
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : List.Nodup l
hs : Set.PairwiseDisjoint (↑(List.toFinset l)) Finsupp.support
⊢ Symmetric (Disjoint on Finsupp.support)
[PROOFSTEP]
intro x y hxy
[GOAL]
case this.intro.intro.hr
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : List.Nodup l
hs : Set.PairwiseDisjoint (↑(List.toFinset l)) Finsupp.support
x y : ι →₀ M
hxy : (Disjoint on Finsupp.support) x y
⊢ (Disjoint on Finsupp.support) y x
[PROOFSTEP]
exact symmetric_disjoint hxy


[GOAL]
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ (a : α), a ∈ x.support → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a
⊢ Acc (Finsupp.Lex r s) x
[PROOFSTEP]
rw [lex_eq_invImage_dfinsupp_lex]
[GOAL]
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ (a : α), a ∈ x.support → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a
⊢ Acc (InvImage (DFinsupp.Lex r fun x => s) toDFinsupp) x
[PROOFSTEP]
classical
refine' InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ _)
simpa only [toDFinsupp_support] using h
[GOAL]
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ (a : α), a ∈ x.support → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a
⊢ Acc (InvImage (DFinsupp.Lex r fun x => s) toDFinsupp) x
[PROOFSTEP]
refine' InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ _)
[GOAL]
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ (a : α), a ∈ x.support → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a
⊢ ∀ (i : α), i ∈ DFinsupp.support (toDFinsupp x) → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) i
[PROOFSTEP]
simpa only [toDFinsupp_support] using h


[GOAL]
α : Type u
inst✝ : DecidableEq α
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
⊢ p ∈ antidiagonal f ↔ p.fst + p.snd = f
[PROOFSTEP]
rcases p with ⟨p₁, p₂⟩
[GOAL]
case mk
α : Type u
inst✝ : DecidableEq α
f p₁ p₂ : α →₀ ℕ
⊢ (p₁, p₂) ∈ antidiagonal f ↔ (p₁, p₂).fst + (p₁, p₂).snd = f
[PROOFSTEP]
simp [antidiagonal, antidiagonal', ← and_assoc, Multiset.toFinsupp_eq_iff, ← Multiset.toFinsupp_eq_iff (f := f)]
[GOAL]
α : Type u
inst✝ : DecidableEq α
n : α →₀ ℕ
f : (α →₀ ℕ) × (α →₀ ℕ)
⊢ Prod.swap f ∈ antidiagonal n ↔ f ∈ antidiagonal n
[PROOFSTEP]
simp only [mem_antidiagonal, add_comm, Prod.swap]
[GOAL]
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)
⊢ Finset.filter (fun p => p.fst = g) (antidiagonal f) = if g ≤ f then {(g, f - g)} else ∅
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)
a b : α →₀ ℕ
⊢ (a, b) ∈ Finset.filter (fun p => p.fst = g) (antidiagonal f) ↔ (a, b) ∈ if g ≤ f then {(g, f - g)} else ∅
[PROOFSTEP]
suffices a = g → (a + b = f ↔ g ≤ f ∧ b = f - g) by
  simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton, Prod.mk.inj_iff, ← and_assoc,
    @and_right_comm _ (a = _), and_congr_left_iff]
[GOAL]
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)
a b : α →₀ ℕ
this : a = g → (a + b = f ↔ g ≤ f ∧ b = f - g)
⊢ (a, b) ∈ Finset.filter (fun p => p.fst = g) (antidiagonal f) ↔ (a, b) ∈ if g ≤ f then {(g, f - g)} else ∅
[PROOFSTEP]
simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton, Prod.mk.inj_iff, ← and_assoc,
  @and_right_comm _ (a = _), and_congr_left_iff]
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)
a b : α →₀ ℕ
⊢ a = g → (a + b = f ↔ g ≤ f ∧ b = f - g)
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a + b = f ↔ a ≤ f ∧ b = f - a
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a + b = f → a ≤ f ∧ b = f - a
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a ≤ a + b ∧ b = a + b - a
[PROOFSTEP]
exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
[GOAL]
case a.mk.mpr
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a ≤ f ∧ b = f - a → a + b = f
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case a.mk.mpr.intro
α : Type u
inst✝ : DecidableEq α
f a : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
h : a ≤ f
⊢ a + (f - a) = f
[PROOFSTEP]
exact add_tsub_cancel_of_le h
[GOAL]
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
⊢ Finset.filter (fun p => p.snd = g) (antidiagonal f) = if g ≤ f then {(f - g, g)} else ∅
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
a b : α →₀ ℕ
⊢ (a, b) ∈ Finset.filter (fun p => p.snd = g) (antidiagonal f) ↔ (a, b) ∈ if g ≤ f then {(f - g, g)} else ∅
[PROOFSTEP]
suffices b = g → (a + b = f ↔ g ≤ f ∧ a = f - g) by
  simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton, Prod.mk.inj_iff, ← and_assoc,
    and_congr_left_iff]
[GOAL]
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
a b : α →₀ ℕ
this : b = g → (a + b = f ↔ g ≤ f ∧ a = f - g)
⊢ (a, b) ∈ Finset.filter (fun p => p.snd = g) (antidiagonal f) ↔ (a, b) ∈ if g ≤ f then {(f - g, g)} else ∅
[PROOFSTEP]
simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton, Prod.mk.inj_iff, ← and_assoc,
  and_congr_left_iff]
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
a b : α →₀ ℕ
⊢ b = g → (a + b = f ↔ g ≤ f ∧ a = f - g)
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ a + b = f ↔ b ≤ f ∧ a = f - b
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ a + b = f → b ≤ f ∧ a = f - b
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ b ≤ a + b ∧ a = a + b - b
[PROOFSTEP]
exact ⟨le_add_left le_rfl, (add_tsub_cancel_right _ _).symm⟩
[GOAL]
case a.mk.mpr
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ b ≤ f ∧ a = f - b → a + b = f
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case a.mk.mpr.intro
α : Type u
inst✝ : DecidableEq α
f b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
h : b ≤ f
⊢ f - b + b = f
[PROOFSTEP]
exact tsub_add_cancel_of_le h
[GOAL]
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ antidiagonal (single a n) =
    map
      (Function.Embedding.prodMap { toFun := single a, inj' := (_ : Function.Injective (single a)) }
        { toFun := single a, inj' := (_ : Function.Injective (single a)) })
      (Nat.antidiagonal n)
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ (x, y) ∈ antidiagonal (single a n) ↔
    (x, y) ∈
      map
        (Function.Embedding.prodMap { toFun := single a, inj' := (_ : Function.Injective (single a)) }
          { toFun := single a, inj' := (_ : Function.Injective (single a)) })
        (Nat.antidiagonal n)
[PROOFSTEP]
simp only [mem_antidiagonal, mem_map, Nat.mem_antidiagonal, Function.Embedding.coe_prodMap, Function.Embedding.coeFn_mk,
  Prod_map, Prod.mk.injEq, Prod.exists]
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n ↔ ∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n → ∃ a_2 b, a_2 + b = n ∧ single a a_2 = x ∧ single a b = y
[PROOFSTEP]
intro h
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ ∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
[PROOFSTEP]
refine ⟨x a, y a, FunLike.congr_fun h a |>.trans single_eq_same, ?_⟩
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ single a (↑x a) = x ∧ single a (↑y a) = y
[PROOFSTEP]
simp_rw [FunLike.ext_iff, ← forall_and]
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ ∀ (x_1 : α), ↑(single a (↑x a)) x_1 = ↑x x_1 ∧ ↑(single a (↑y a)) x_1 = ↑y x_1
[PROOFSTEP]
intro i
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
i : α
⊢ ↑(single a (↑x a)) i = ↑x i ∧ ↑(single a (↑y a)) i = ↑y i
[PROOFSTEP]
replace h := FunLike.congr_fun h i
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : ↑(x + y) i = ↑(single a n) i
⊢ ↑(single a (↑x a)) i = ↑x i ∧ ↑(single a (↑y a)) i = ↑y i
[PROOFSTEP]
simp_rw [single_apply, Finsupp.add_apply] at h ⊢
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : ↑x i + ↑y i = if a = i then n else 0
⊢ (if a = i then ↑x a else 0) = ↑x i ∧ (if a = i then ↑y a else 0) = ↑y i
[PROOFSTEP]
obtain rfl | hai := Decidable.eq_or_ne a i
[GOAL]
case a.mk.mp.inl
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : ↑x a + ↑y a = if a = a then n else 0
⊢ (if a = a then ↑x a else 0) = ↑x a ∧ (if a = a then ↑y a else 0) = ↑y a
[PROOFSTEP]
exact ⟨if_pos rfl, if_pos rfl⟩
[GOAL]
case a.mk.mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : ↑x i + ↑y i = if a = i then n else 0
hai : a ≠ i
⊢ (if a = i then ↑x a else 0) = ↑x i ∧ (if a = i then ↑y a else 0) = ↑y i
[PROOFSTEP]
simp_rw [if_neg hai, _root_.add_eq_zero_iff] at h ⊢
[GOAL]
case a.mk.mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : ↑x i = 0 ∧ ↑y i = 0
⊢ 0 = ↑x i ∧ 0 = ↑y i
[PROOFSTEP]
exact h.imp Eq.symm Eq.symm
[GOAL]
case a.mk.mpr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ (∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y) → x + y = single a n
[PROOFSTEP]
rintro ⟨a, b, rfl, rfl, rfl⟩
[GOAL]
case a.mk.mpr.intro.intro.intro.intro
α : Type u
inst✝ : DecidableEq α
a✝ : α
a b : ℕ
⊢ single a✝ a + single a✝ b = single a✝ (a + b)
[PROOFSTEP]
exact (single_add _ _ _).symm


[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
⊢ toDFinsupp (single i m) = DFinsupp.single i m
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
i✝ : ι
⊢ ↑(toDFinsupp (single i m)) i✝ = ↑(DFinsupp.single i m) i✝
[PROOFSTEP]
simp [Finsupp.single_apply, DFinsupp.single_apply]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
⊢ DFinsupp.support (Finsupp.toDFinsupp f) = f.support
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a✝ : ι
⊢ a✝ ∈ DFinsupp.support (Finsupp.toDFinsupp f) ↔ a✝ ∈ f.support
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
i : ι
⊢ i ∈ support f ↔ ↑f i ≠ 0
[PROOFSTEP]
simp only [DFinsupp.mem_support_iff]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ (toFinsupp f).support = support f
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a✝ : ι
⊢ a✝ ∈ (toFinsupp f).support ↔ a✝ ∈ support f
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ toFinsupp (single i m) = Finsupp.single i m
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a✝ : ι
⊢ ↑(toFinsupp (single i m)) a✝ = ↑(Finsupp.single i m) a✝
[PROOFSTEP]
simp [Finsupp.single_apply, DFinsupp.single_apply]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : (m : M) → Decidable (m ≠ 0)
inst✝ : Module R M
⊢ ↑(finsuppLequivDFinsupp R) = Finsupp.toDFinsupp
[PROOFSTEP]
simp only [@LinearEquiv.coe_coe]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : (m : M) → Decidable (m ≠ 0)
inst✝ : Module R M
⊢ ↑(finsuppLequivDFinsupp R) = Finsupp.toDFinsupp
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ i ∈ (splitSupport f).val ∨ split f i = 0
[PROOFSTEP]
rw [← Finset.mem_def, mem_splitSupport_iff_nonzero]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ split f i ≠ 0 ∨ split f i = 0
[PROOFSTEP]
exact (em _).symm
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
⊢ (i : ι) × η i →₀ N
[PROOFSTEP]
haveI := Classical.decEq ι
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this : DecidableEq ι
⊢ (i : ι) × η i →₀ N
[PROOFSTEP]
haveI := fun i => Classical.decEq (η i →₀ N)
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
⊢ (i : ι) × η i →₀ N
[PROOFSTEP]
refine'
  onFinset (Finset.sigma f.support fun j => (f j).support) (fun ji => f ji.1 ji.2) fun g hg =>
    Finset.mem_sigma.mpr ⟨_, mem_support_iff.mpr hg⟩
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0
⊢ g.fst ∈ DFinsupp.support f
[PROOFSTEP]
simp only [Ne.def, DFinsupp.mem_support_toFun]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0
⊢ ¬↑f g.fst = 0
[PROOFSTEP]
intro h
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0
h : ↑f g.fst = 0
⊢ False
[PROOFSTEP]
dsimp at hg
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : ¬↑(↑f g.fst) g.snd = 0
h : ↑f g.fst = 0
⊢ False
[PROOFSTEP]
rw [h] at hg
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : ¬↑0 g.snd = 0
h : ↑f g.fst = 0
⊢ False
[PROOFSTEP]
simp only [coe_zero, Pi.zero_apply, not_true] at hg
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
⊢ (fun f =>
        onFinset (Finset.sigma (DFinsupp.support f) fun j => (↑f j).support) (fun ji => ↑(↑f ji.fst) ji.snd)
          (_ :
            ∀ (g : (i : ι) × η i),
              (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0 → g ∈ Finset.sigma (DFinsupp.support f) fun j => (↑f j).support))
      ((fun f =>
          { toFun := split f,
            support' :=
              Trunc.mk
                { val := (splitSupport f).val,
                  property := (_ : ∀ (i : ι), i ∈ (splitSupport f).val ∨ split f i = 0) } })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
a✝ : (i : ι) × η i
⊢ ↑((fun f =>
            onFinset (Finset.sigma (DFinsupp.support f) fun j => (↑f j).support) (fun ji => ↑(↑f ji.fst) ji.snd)
              (_ :
                ∀ (g : (i : ι) × η i),
                  (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0 →
                    g ∈ Finset.sigma (DFinsupp.support f) fun j => (↑f j).support))
          ((fun f =>
              { toFun := split f,
                support' :=
                  Trunc.mk
                    { val := (splitSupport f).val,
                      property := (_ : ∀ (i : ι), i ∈ (splitSupport f).val ∨ split f i = 0) } })
            f))
      a✝ =
    ↑f a✝
[PROOFSTEP]
simp [split]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
⊢ (fun f =>
        { toFun := split f,
          support' :=
            Trunc.mk
              { val := (splitSupport f).val, property := (_ : ∀ (i : ι), i ∈ (splitSupport f).val ∨ split f i = 0) } })
      ((fun f =>
          onFinset (Finset.sigma (DFinsupp.support f) fun j => (↑f j).support) (fun ji => ↑(↑f ji.fst) ji.snd)
            (_ :
              ∀ (g : (i : ι) × η i),
                (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0 → g ∈ Finset.sigma (DFinsupp.support f) fun j => (↑f j).support))
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑((fun f =>
                { toFun := split f,
                  support' :=
                    Trunc.mk
                      { val := (splitSupport f).val,
                        property := (_ : ∀ (i : ι), i ∈ (splitSupport f).val ∨ split f i = 0) } })
              ((fun f =>
                  onFinset (Finset.sigma (DFinsupp.support f) fun j => (↑f j).support) (fun ji => ↑(↑f ji.fst) ji.snd)
                    (_ :
                      ∀ (g : (i : ι) × η i),
                        (fun ji => ↑(↑f ji.fst) ji.snd) g ≠ 0 →
                          g ∈ Finset.sigma (DFinsupp.support f) fun j => (↑f j).support))
                f))
          i✝)
      a✝ =
    ↑(↑f i✝) a✝
[PROOFSTEP]
simp [split]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
⊢ DFinsupp.support (↑sigmaFinsuppEquivDFinsupp f) = splitSupport f
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ a✝ ∈ DFinsupp.support (↑sigmaFinsuppEquivDFinsupp f) ↔ a✝ ∈ splitSupport f
[PROOFSTEP]
rw [DFinsupp.mem_support_toFun]
[GOAL]
case a
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ ↑(↑sigmaFinsuppEquivDFinsupp f) a✝ ≠ 0 ↔ a✝ ∈ splitSupport f
[PROOFSTEP]
exact (Finsupp.mem_splitSupport_iff_nonzero _ _).symm
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
a : (i : ι) × η i
n : N
⊢ ↑sigmaFinsuppEquivDFinsupp (single a n) = DFinsupp.single a.fst (single a.snd n)
[PROOFSTEP]
obtain ⟨i, a⟩ := a
[GOAL]
case mk
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
⊢ ↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n) =
    DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)
[PROOFSTEP]
ext j b
[GOAL]
case mk.h.h
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) i) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) i) b
[PROOFSTEP]
classical simp [split_apply, Finsupp.single_apply]
[GOAL]
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) i) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) i) b
[PROOFSTEP]
simp [split_apply, Finsupp.single_apply]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
[PROOFSTEP]
suffices Finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
this : ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (single { fst := i, snd := a } n)) j) b =
    ↑(↑(DFinsupp.single { fst := i, snd := a }.fst (single { fst := i, snd := a }.snd n)) j) b
[PROOFSTEP]
simp [split_apply, dif_neg h, this]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
[PROOFSTEP]
have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ { fst := i, snd := a } ≠ { fst := j, snd := b }
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : { fst := i, snd := a } ≠ { fst := j, snd := b }
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
[PROOFSTEP]
classical rw [Finsupp.single_apply, if_neg H]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : { fst := i, snd := a } ≠ { fst := j, snd := b }
⊢ ↑(single { fst := i, snd := a } n) { fst := j, snd := b } = 0
[PROOFSTEP]
rw [Finsupp.single_apply, if_neg H]
[GOAL]
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
⊢ ↑sigmaFinsuppEquivDFinsupp (f + g) = ↑sigmaFinsuppEquivDFinsupp f + ↑sigmaFinsuppEquivDFinsupp g
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (f + g)) i✝) a✝ =
    ↑(↑(↑sigmaFinsuppEquivDFinsupp f + ↑sigmaFinsuppEquivDFinsupp g) i✝) a✝
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R✝ : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R✝
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
⊢ ↑sigmaFinsuppEquivDFinsupp (r • f) = SMul.smul r (↑sigmaFinsuppEquivDFinsupp f)
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
R✝ : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝³ : Semiring R✝
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ↑(↑(↑sigmaFinsuppEquivDFinsupp (r • f)) i✝) a✝ = ↑(↑(SMul.smul r (↑sigmaFinsuppEquivDFinsupp f)) i✝) a✝
[PROOFSTEP]
rfl


[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s✝ : Finset ι
f✝ : (i : ι) → i ∈ s✝ → α
i✝ : ι
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ i ∈ map (Embedding.subtype fun x => x ∈ s) (filter (fun i => f ↑i (_ : ↑i ∈ s) ≠ 0) (attach s)) ↔
    (fun i => if H : i ∈ s then f i H else 0) i ≠ 0
[PROOFSTEP]
classical simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s✝ : Finset ι
f✝ : (i : ι) → i ∈ s✝ → α
i✝ : ι
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ i ∈ map (Embedding.subtype fun x => x ∈ s) (filter (fun i => f ↑i (_ : ↑i ∈ s) ≠ 0) (attach s)) ↔
    (fun i => if H : i ∈ s then f i H else 0) i ≠ 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ ↑(indicator s f) i = if hi : i ∈ s then f i hi else 0
[PROOFSTEP]
simp only [indicator, ne_eq, coe_mk]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (if H : i ∈ s then f i H else 0) = if hi : i ∈ s then f i hi else 0
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ Injective fun f => indicator s f
[PROOFSTEP]
intro a b h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
⊢ a = b
[PROOFSTEP]
ext i hi
[GOAL]
case h.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ : ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
i : ι
hi : i ∈ s
⊢ a i hi = b i hi
[PROOFSTEP]
rw [← indicator_of_mem hi a, ← indicator_of_mem hi b]
[GOAL]
case h.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ : ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
i : ι
hi : i ∈ s
⊢ ↑(indicator s a) i = ↑(indicator s b) i
[PROOFSTEP]
exact FunLike.congr_fun h i
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ ↑(indicator s f).support ⊆ ↑s
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : i ∈ ↑(indicator s f).support
⊢ i ∈ ↑s
[PROOFSTEP]
rw [mem_coe, mem_support_iff] at hi
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : ↑(indicator s f) i ≠ 0
⊢ i ∈ ↑s
[PROOFSTEP]
by_contra h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : ↑(indicator s f) i ≠ 0
h : ¬i ∈ ↑s
⊢ False
[PROOFSTEP]
exact hi (indicator_of_not_mem h _)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
b : α
⊢ single i b = indicator {i} fun x x => b
[PROOFSTEP]
classical
ext j
simp [single_apply, indicator_apply, @eq_comm _ j]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
b : α
⊢ single i b = indicator {i} fun x x => b
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
b : α
j : ι
⊢ ↑(single i b) j = ↑(indicator {i} fun x x => b) j
[PROOFSTEP]
simp [single_apply, indicator_apply, @eq_comm _ j]


[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f✝ g✝ f g : α →₀ N
a : α
⊢ a ∈ neLocus f g ↔ ↑f a ≠ ↑g a
[PROOFSTEP]
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff, and_iff_right_iff_imp] using Ne.ne_or_ne _
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ ↑(neLocus f g) = {x | ↑f x ≠ ↑g x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
x✝ : α
⊢ x✝ ∈ ↑(neLocus f g) ↔ x✝ ∈ {x | ↑f x ≠ ↑g x}
[PROOFSTEP]
exact mem_neLocus
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f✝ g✝ f g : α →₀ N
h : f = g
⊢ neLocus f f = ∅
[PROOFSTEP]
simp only [neLocus, Ne.def, eq_self_iff_true, not_true, Finset.filter_False]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ neLocus f g = neLocus g f
[PROOFSTEP]
simp_rw [neLocus, Finset.union_comm, ne_comm]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ neLocus f 0 = f.support
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
a✝ : α
⊢ a✝ ∈ neLocus f 0 ↔ a✝ ∈ f.support
[PROOFSTEP]
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : Zero N
inst✝¹ : DecidableEq M
inst✝ : Zero M
f g : α →₀ N
F : N → M
F0 : F 0 = 0
x : α
⊢ x ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) → x ∈ neLocus f g
[PROOFSTEP]
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
⊢ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) = neLocus g₁ g₂
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
a✝ : α
⊢ a✝ ∈ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) ↔ a✝ ∈ neLocus g₁ g₂
[PROOFSTEP]
simpa only [mem_neLocus] using (hF _).ne_iff
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f => F f g
⊢ neLocus (zipWith F F0 f₁ g) (zipWith F F0 f₂ g) = neLocus f₁ f₂
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f => F f g
a✝ : α
⊢ a✝ ∈ neLocus (zipWith F F0 f₁ g) (zipWith F F0 f₂ g) ↔ a✝ ∈ neLocus f₁ f₂
[PROOFSTEP]
simpa only [mem_neLocus] using (hF _).ne_iff
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
⊢ neLocus (mapRange F F0 f) (mapRange F F0 g) = neLocus f g
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
a✝ : α
⊢ a✝ ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) ↔ a✝ ∈ neLocus f g
[PROOFSTEP]
simpa only [mem_neLocus] using hF.ne_iff
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (-f) g = neLocus f (-g)
[PROOFSTEP]
rw [← neLocus_neg_neg, neg_neg]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus f g = (f - g).support
[PROOFSTEP]
rw [← neLocus_add_right _ _ (-g), add_right_neg, neLocus_zero_right, sub_eq_add_neg]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂
[PROOFSTEP]
simp only [sub_eq_add_neg, neLocus_add_left, neLocus_neg_neg]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂
[PROOFSTEP]
simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus f (f + g) = g.support
[PROOFSTEP]
rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f + g) f = g.support
[PROOFSTEP]
rw [neLocus_comm, neLocus_self_add_right]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus f (f - g) = g.support
[PROOFSTEP]
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
[GOAL]
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f - g) f = g.support
[PROOFSTEP]
rw [neLocus_comm, neLocus_self_sub_right]