ι : Type u_2
M : Type u_1
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
ι : Type u_2
M : Type u_1
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
simp only [Finset.sup_eq_union, List.foldr_map, Finsupp.mem_support_iff, exists_prop]
case nil
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
⊢ x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ [] ↔ ∃ f, f ∈ [] ∧ ↑f x ≠ 0

case cons
ι : Type u_2
M : Type u_1
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
ι : Type u_2
M : Type u_1
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
induction' l with hd tl IH
no goals
case nil
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
⊢ x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ [] ↔ ∃ f, f ∈ [] ∧ ↑f x ≠ 0
simp
no goals
case cons
ι : Type u_2
M : Type u_1
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
simp only [foldr, Function.comp_apply, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH,
  find?, mem_cons, exists_eq_or_imp]