no goals
α : Type u_1
β : Type u_3
γ : Type ?u.66990
δ : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
m₂ : β → δ
⊢ ∀ (x : α × δ), x ∈ univ ×ˢ range m₂ ↔ x ∈ range fun p => (p.fst, m₂ p.snd)
simp [range]