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

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