α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type u_4
ε : Type ?u.63784
ι : Type ?u.63787
f✝ : α →. β
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ prodMap f g x ↔ ∃ hp hq, Part.get (f x.fst) hp = y.fst ∧ Part.get (g x.snd) hq = y.snd

α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type u_4
ε : Type ?u.63784
ι : Type ?u.63787
f✝ : α →. β
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ hp hq, Part.get (f x.fst) hp = y.fst ∧ Part.get (g x.snd) hq = y.snd) ↔ y.fst ∈ f x.fst ∧ y.snd ∈ g x.snd
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type u_4
ε : Type ?u.63784
ι : Type ?u.63787
f✝ : α →. β
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ prodMap f g x ↔ y.fst ∈ f x.fst ∧ y.snd ∈ g x.snd
trans ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type u_4
ε : Type ?u.63784
ι : Type ?u.63787
f✝ : α →. β
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ prodMap f g x ↔ ∃ hp hq, Part.get (f x.fst) hp = y.fst ∧ Part.get (g x.snd) hq = y.snd
simp only [prodMap, Part.mem_mk_iff, And.exists, Prod.ext_iff]