-- Mathlib/Data/Seq/Computation.lean
theorem LiftRelAux.ret_left (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a cb) :
    LiftRelAux R C (Sum.inl a) (destruct cb) ↔ ∃ b, b ∈ cb ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ b, b ∈ cb ∧ R a b

Tactic:
apply cb.recOn (fun b => _) fun cb => _

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

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

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

Tactic:
exact
  ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb cb✝ : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb✝.think.destruct ↔ ∃ b, b ∈ cb✝.think ∧ R a b

Tactic:
rw [destruct_think]

Result:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb cb✝ : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb✝) ↔ ∃ b, b ∈ cb✝.think ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb cb✝ : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb✝) ↔ ∃ b, b ∈ cb✝.think ∧ R a b

Tactic:
exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
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) (pure b').destruct

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
β : Type v
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) (pure b).destruct

Tactic:
rw [mem_unique (ret_mem _) mb]

Result:
α : Type u
β : Type v
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) (pure b').destruct

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

Tactic:
intro b

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

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

Tactic:
intro

Result:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb cb✝ : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb✝.think.destruct ↔ ∃ b, b ∈ cb✝.think ∧ R a b