no goals
α : Type u_2
β : Type u_3
γ✝ : Type ?u.148439
ι : Sort ?u.148442
ι' : Sort ?u.148445
ι₂ : Sort ?u.148448
κ : ι → Sort ?u.148453
κ₁ : ι → Sort ?u.148458
κ₂ : ι → Sort ?u.148463
κ' : ι' → Sort ?u.148468
γ : α → Type u_1
f : Sigma γ → β
⊢ ∀ (x : β), x ∈ range f ↔ x ∈ ⋃ (a : α), range fun b => f { fst := a, snd := b }
simp