α : Type ?u.741366
β : Type ?u.741369
γ : Type ?u.741372
ι : Type u_1
M : Type u_3
M' : Type ?u.741381
N : Type ?u.741384
P : Type ?u.741387
G : Type ?u.741390
H : Type ?u.741393
R : Type ?u.741396
S : Type ?u.741399
αs : ι → Type u_2
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a),
    { fst := a, snd := b } ∈ l.support ↔ (∃ a_1, a_1 ∈ l.support ∧ a_1.fst = a) ∧ { fst := a, snd := b } ∈ l.support
α : Type ?u.741366
β : Type ?u.741369
γ : Type ?u.741372
ι : Type u_1
M : Type u_3
M' : Type ?u.741381
N : Type ?u.741384
P : Type ?u.741387
G : Type ?u.741390
H : Type ?u.741393
R : Type ?u.741396
S : Type ?u.741399
αs : ι → Type u_2
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ l.support = Finset.sigma (splitSupport l) fun i => (split l i).support
simp only [Finset.ext_iff, splitSupport, split, comapDomain, @mem_image _ _ (Classical.decEq _),
  mem_preimage, Sigma.forall, mem_sigma]
no goals
α : Type ?u.741366
β : Type ?u.741369
γ : Type ?u.741372
ι : Type u_1
M : Type u_3
M' : Type ?u.741381
N : Type ?u.741384
P : Type ?u.741387
G : Type ?u.741390
H : Type ?u.741393
R : Type ?u.741396
S : Type ?u.741399
αs : ι → Type u_2
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a),
    { fst := a, snd := b } ∈ l.support ↔ (∃ a_1, a_1 ∈ l.support ∧ a_1.fst = a) ∧ { fst := a, snd := b } ∈ l.support
tauto