no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type u_4
ε : Type ?u.65395
ι : Type ?u.65398
f✝ : α →. β
f : α →. γ
g : β →. δ
a : α × β
⊢ ∀ (b : γ × δ), b ∈ prodLift (comp f ↑Prod.fst) (comp g ↑Prod.snd) a ↔ b ∈ prodMap f g a
simp