α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ ∀ (b : β), LiftRelAux R C (Sum.inl a) (destruct (pure b)) ↔ ∃ b_1, b_1 ∈ pure b ∧ R a b_1

α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ ∀ (cb : Computation β), LiftRelAux R C (Sum.inl a) (destruct (think cb)) ↔ ∃ b, b ∈ think cb ∧ R a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) (destruct cb) ↔ ∃ b, b ∈ cb ∧ R a b
apply cb.recOn (fun b => _) fun cb => _
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
b : β
⊢ LiftRelAux R C (Sum.inl a) (destruct (pure b)) ↔ ∃ b_1, b_1 ∈ pure b ∧ R a b_1
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ ∀ (b : β), LiftRelAux R C (Sum.inl a) (destruct (pure b)) ↔ ∃ b_1, b_1 ∈ pure b ∧ R a b_1
intro b
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
b : β
⊢ LiftRelAux R C (Sum.inl a) (destruct (pure b)) ↔ ∃ b_1, b_1 ∈ pure b ∧ R a b_1
exact
  ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb] ; exact h⟩
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (destruct (pure b'))
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (destruct (pure b))
rw [mem_unique (ret_mem _) mb]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (destruct (pure b'))
exact h
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb cb✝ : Computation β
⊢ LiftRelAux R C (Sum.inl a) (destruct (think cb✝)) ↔ ∃ b, b ∈ think cb✝ ∧ R a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ ∀ (cb : Computation β), LiftRelAux R C (Sum.inl a) (destruct (think cb)) ↔ ∃ b, b ∈ think cb ∧ R a b
intro
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb cb✝ : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb✝) ↔ ∃ b, b ∈ think cb✝ ∧ R a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb cb✝ : Computation β
⊢ LiftRelAux R C (Sum.inl a) (destruct (think cb✝)) ↔ ∃ b, b ∈ think cb✝ ∧ R a b
rw [destruct_think]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb cb✝ : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb✝) ↔ ∃ b, b ∈ think cb✝ ∧ R a b
exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩