α : Type u
β : Type v
γ : Type w
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b
let ⟨b', mb', ab'⟩ := l ma
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b
rw [mem_unique mb mb']
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'
exact ab'