awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
⊢ IsTrans (Computation α) (LiftRel R)

Tactic:
⟨fun _ _ _ ⟨l1, r1⟩ ⟨l2, r2⟩ =>
  ⟨fun {_a} a1 =>
    let ⟨_b, b2, ab⟩ := l1 a1
    let ⟨c, c3, bc⟩ := l2 b2
    ⟨c, c3, trans_of R ab bc⟩,
    fun {_c} c3 =>
    let ⟨_b, b2, bc⟩ := r2 c3
    let ⟨a, a1, ab⟩ := r1 b2
    ⟨a, a1, trans_of R ab bc⟩⟩⟩

Premises used: _private.0.Computation.LiftRel.symm.match_2, _private.0.Computation.LiftRel.symm.match_1, IsTrans.mk, Membership.mem, Exists, _private.0.Computation.LiftRel.symm.match_3, And, And.intro, Exists.intro, trans_of, Computation.LiftRel
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
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
let : ∀ (b' : β) (mb' : b' ∈ cb) (ab' : R a b'), R a b
⊢ R a b

Tactic:
let ⟨b', mb', ab'⟩ := l ma
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
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'
rw : R a b'
⊢ R a b

Tactic:
rw [mem_unique mb mb']

Premises used: Computation.mem_unique
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
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'

Tactic:
ab'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
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'

Tactic:
exact ab'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
rw : ∃ (b : β), b ∈ cb ∧ R a b
⊢ ∃ (b : β), b ∈ cb ∧ R a' b

Tactic:
rw [mem_unique ma' ma]

Premises used: Computation.mem_unique
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ (b : β), b ∈ cb ∧ R a b

Tactic:
⟨b, mb, ab⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ (b : β), b ∈ cb ∧ R a b

Tactic:
exact ⟨b, mb, ab⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
rw : ∃ (a : α), a ∈ ca ∧ R a b
⊢ ∃ (a : α), a ∈ ca ∧ R a b'

Tactic:
rw [mem_unique mb' mb]

Premises used: Computation.mem_unique
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ (a : α), a ∈ ca ∧ R a b

Tactic:
⟨a, ma, ab⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ (a : α), a ∈ ca ∧ R a b

Tactic:
exact ⟨a, ma, ab⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
H : LiftRel R ca cb
a : α
h : a ∈ ca
⊢ ∃ (b : β), b ∈ cb ∧ R a b

Tactic:
H.left h

Premises used: And.left
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
H : LiftRel R ca cb
b : β
h : b ∈ cb
⊢ ∃ (a : α), a ∈ ca ∧ R a b

Tactic:
H.right h

Premises used: And.right
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
let : ∀ (b' : β) (mb' : b' ∈ cb) (ab : R a b'), R a b
⊢ R a b

Tactic:
let ⟨b', mb', ab⟩ := h.left ma
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab : R a b'
rwa rwa₁ rwa₂ rwa₃ : R a b'
⊢ R a b

Tactic:
rwa [mem_unique mb mb']

Premises used: Computation.mem_unique
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → Computation γ
f2 : β → Computation δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → LiftRel S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind f1) (s2.bind f2)

Tactic:
let ⟨l1, r1⟩ := h1
  ⟨fun {_} cB =>
    let ⟨_, a1, c₁⟩ := exists_of_mem_bind cB
    let ⟨_, b2, ab⟩ := l1 a1
    let ⟨l2, _⟩ := h2 ab
    let ⟨_, d2, cd⟩ := l2 c₁
    ⟨_, mem_bind b2 d2, cd⟩,
    fun {_} dB =>
    let ⟨_, b1, d1⟩ := exists_of_mem_bind dB
    let ⟨_, a2, ab⟩ := r1 b1
    let ⟨_, r2⟩ := h2 ab
    let ⟨_, c₂, cd⟩ := r2 d1
    ⟨_, mem_bind a2 c₂, cd⟩⟩

Premises used: _private.0.Computation.liftRel_bind.match_1, _private.0.Computation.liftRel_bind.match_7, _private.0.Computation.liftRel_bind.match_4, Membership.mem, Exists, _private.0.Computation.liftRel_bind.match_6, _private.0.Computation.liftRel_bind.match_3, Computation.exists_of_mem_bind, And, _private.0.Computation.LiftRel.imp.match_3, _private.0.Computation.liftRel_bind.match_2, And.intro, Exists.intro, Computation.bind, _private.0.Computation.liftRel_bind.match_5, Computation.LiftRel, Computation.mem_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
h : ∃ (b : β), b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
rw : ∃ (b : β), b ∈ cb ∧ R a b
⊢ ∃ (b : β), b ∈ cb ∧ R a' b

Tactic:
rw [eq_of_pure_mem ma']

Premises used: Computation.eq_of_pure_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
h : ∃ (b : β), b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ (b : β), b ∈ cb ∧ R a b

Tactic:
⟨b, mb, ab⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
h : ∃ (b : β), b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ (b : β), b ∈ cb ∧ R a b

Tactic:
exact ⟨b, mb, ab⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
h : ∃ (b : β), b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
rw : R a b
⊢ R a b'

Tactic:
rw [mem_unique mb' mb]

Premises used: Computation.mem_unique
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
h : ∃ (b : β), b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b

Tactic:
ab
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
h : ∃ (b : β), b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b

Tactic:
exact ab
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
b : β
rw : LiftRel (fun (x : β) (y : α) ↦ R y x) (pure b) ca ↔ ∃ (a : α), a ∈ ca ∧ R a b
rw₁ rw₂ : (∃ (b_1 : α), b_1 ∈ ca ∧ R b_1 b) ↔ ∃ (a : α), a ∈ ca ∧ R a b
⊢ LiftRel R ca (pure b) ↔ ∃ (a : α), a ∈ ca ∧ R a b

Tactic:
rw [LiftRel.swap, liftRel_pure_left]

Premises used: Computation.liftRel_pure_left, Computation.LiftRel.swap
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
⊢ LiftRel R (pure a) (pure b) ↔ R a b

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel R ca.think cb ↔ LiftRel R ca cb

Tactic:
and_congr (forall_congr' fun _ => imp_congr ⟨of_think_mem, think_mem⟩ Iff.rfl)
    (forall_congr' fun _ =>
      imp_congr Iff.rfl <| exists_congr fun _ => and_congr ⟨of_think_mem, think_mem⟩ Iff.rfl)

Premises used: Computation.think_mem, Iff.rfl, exists_congr, imp_congr, Iff.intro, forall_congr', Computation.of_think_mem, and_congr, Computation.LiftRel
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
rw :
  LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) cb.think ca ↔
    LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) cb ca
⊢ LiftRel R ca cb.think ↔ LiftRel R ca cb

Tactic:
rw [← LiftRel.swap R, ← LiftRel.swap R]

Premises used: Computation.LiftRel.swap
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) cb.think ca ↔
    LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) cb ca

Tactic:
apply liftRel_think_left

Premises used: Computation.liftRel_think_left
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
Ha : ∀ (a : α), a ∈ ca → LiftRel R ca cb
Hb : ∀ (b : β), b ∈ cb → LiftRel R ca cb
⊢ LiftRel R ca cb

Tactic:
⟨fun {_} ma => (Ha _ ma).left ma, fun {_} mb => (Hb _ mb).right mb⟩

Premises used: And.right, And.left, And.intro, Computation.LiftRel
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca ca' : Computation α
cb cb' : Computation β
ha : ca ~ ca'
hb : cb ~ cb'
⊢ LiftRel R ca cb ↔ LiftRel R ca' cb'

Tactic:
and_congr
    (forall_congr' fun _ => imp_congr (ha _) <| exists_congr fun _ => and_congr (hb _) Iff.rfl)
    (forall_congr' fun _ => imp_congr (hb _) <| exists_congr fun _ => and_congr (ha _) Iff.rfl)

Premises used: Iff.rfl, exists_congr, imp_congr, forall_congr', and_congr, Computation.LiftRel
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
rw : LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))
⊢ LiftRel S (map f1 s1) (map f2 s2)

Tactic:
rw [← bind_pure, ← bind_pure]

Premises used: Computation.bind_pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
apply : ∀ {a : α} {b : β}, R a b → LiftRel S ((pure ∘ f1) a) ((pure ∘ f2) b)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))

Tactic:
apply liftRel_bind _ _ h1

Premises used: Computation.liftRel_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ ∀ {a : α} {b : β}, R a b → LiftRel S ((pure ∘ f1) a) ((pure ∘ f2) b)

Tactic:
simpa
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
rw : LiftRel (fun (x1 x2 : β) ↦ x1 = x2) (map f s1) (map f s2)
⊢ map f s1 ~ map f s2

Tactic:
rw [← lift_eq_iff_equiv]

Premises used: Computation.lift_eq_iff_equiv
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun (x1 x2 : β) ↦ x1 = x2) (map f s1) (map f s2)

Tactic:
liftRel_map Eq _ ((lift_eq_iff_equiv _ _).2 h1) fun {a} b => congr_arg _

Premises used: Iff.mpr, congr_arg, Computation.lift_eq_iff_equiv, Computation.liftRel_map, Eq
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun (x1 x2 : β) ↦ x1 = x2) (map f s1) (map f s2)

Tactic:
exact liftRel_map Eq _ ((lift_eq_iff_equiv _ _).2 h1) fun {a} b => congr_arg _

Premises used: Iff.mpr, congr_arg, Computation.lift_eq_iff_equiv, Computation.liftRel_map, Eq
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b

Tactic:
rfl

Premises used: Computation.LiftRelAux, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ (b : β), b ∈ cb ∧ R a b

Tactic:
rfl

Premises used: Computation.LiftRelAux, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
⊢ LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ (a : α), a ∈ ca ∧ R a b

Tactic:
rfl

Premises used: Computation.LiftRelAux, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb

Tactic:
rfl

Premises used: Computation.LiftRelAux, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
h_1 : ∃ (b_1 : β), b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
rw : LiftRelAux R C (Sum.inl a) (pure b').destruct
⊢ LiftRelAux R C (Sum.inl a) (pure b).destruct

Tactic:
rw [mem_unique (ret_mem _) mb]

Premises used: Computation.mem_unique, Computation.ret_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
h_1 : ∃ (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:
h

Premises used: Computation.LiftRelAux
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
h_1 : ∃ (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
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
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⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
think : LiftRelAux R C (Sum.inl a) (Sum.inr cb) ↔ ∃ (b : β), b ∈ cb.think ∧ R a b
⊢ LiftRelAux R C (Sum.inl a) cb.think.destruct ↔ ∃ (b : β), b ∈ cb.think ∧ R a b

Tactic:
rw [destruct_think]

Premises used: Computation.destruct_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb) ↔ ∃ (b : β), b ∈ cb.think ∧ R a b

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

Premises used: Computation.think, _private.0.Computation.LiftRelAux.ret_left.match_3, Computation.LiftRelAux, Computation.think_mem, Membership.mem, Exists, Sum.inl, And, _private.0.Computation.LiftRelAux.ret_left.match_2, Sum.inr, And.intro, Iff.intro, Exists.intro, Computation.of_think_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
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⟩⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
pure :
  ∀ (b : β), LiftRelAux R C (Sum.inl a) (Computation.pure b).destruct ↔ ∃ (b_1 : β), b_1 ∈ Computation.pure b ∧ R a b_1
think : ∀ (cb : Computation β), LiftRelAux R C (Sum.inl a) cb.think.destruct ↔ ∃ (b : β), b ∈ cb.think ∧ R a b
⊢ LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ (b : β), b ∈ cb ∧ R a b

Tactic:
induction cb using recOn with
  | pure b =>
    exact
      ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩
  | think cb =>
    rw [destruct_think]
    exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩

Premises used: Computation.think, Computation.pure, Computation.destruct_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
a : α ⊕ Computation α
b : β ⊕ Computation β
inl :
  ∀ (a : α),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inl a) =
      LiftRelAux R C (Sum.inl a) b
inr :
  ∀ (ca : Computation α),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inr ca) =
      LiftRelAux R C (Sum.inr ca) b
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b a =
    LiftRelAux R C a b

Tactic:
rcases a with a | ca
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
b : β ⊕ Computation β
a : α
inl :
  ∀ (b : β),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) (Sum.inl a) =
      LiftRelAux R C (Sum.inl a) (Sum.inl b)
inl₁ :
  ∀ (cb : Computation β),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inr cb) (Sum.inl a) =
      LiftRelAux R C (Sum.inl a) (Sum.inr cb)
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inl a) =
    LiftRelAux R C (Sum.inl a) b

Tactic:
rcases b with b | cb
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
b : β ⊕ Computation β
ca : Computation α
inr :
  ∀ (b : β),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) (Sum.inr ca) =
      LiftRelAux R C (Sum.inr ca) (Sum.inl b)
inr₁ :
  ∀ (cb : Computation β),
    LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inr cb) (Sum.inr ca) =
      LiftRelAux R C (Sum.inr ca) (Sum.inr cb)
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) b (Sum.inr ca) =
    LiftRelAux R C (Sum.inr ca) b

Tactic:
rcases b with b | cb
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
a : α
b : β
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) (Sum.inl a) =
    LiftRelAux R C (Sum.inl a) (Sum.inl b)

Tactic:
simp only [LiftRelAux]

Premises used: Computation.LiftRelAux
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
a : α
cb : Computation β
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inr cb) (Sum.inl a) =
    LiftRelAux R C (Sum.inl a) (Sum.inr cb)

Tactic:
simp only [LiftRelAux]

Premises used: Computation.LiftRelAux
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
ca : Computation α
b : β
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) (Sum.inr ca) =
    LiftRelAux R C (Sum.inr ca) (Sum.inl b)

Tactic:
simp only [LiftRelAux]

Premises used: Computation.LiftRelAux
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : (x : Computation α) → (y : Computation β) → Prop
ca : Computation α
cb : Computation β
⊢ LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inr cb) (Sum.inr ca) =
    LiftRelAux R C (Sum.inr ca) (Sum.inr cb)

Tactic:
simp only [LiftRelAux]

Premises used: Computation.LiftRelAux
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
rw :
  LiftRelAux (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : Computation α) (a_1 : Computation β) ↦ Prop) C) (Sum.inl b) ca.destruct ↔
    ∃ (a : α), a ∈ ca ∧ R a b
rw₁ rw₂ :
  (∃ (b_1 : α), b_1 ∈ ca ∧ Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R b b_1) ↔ ∃ (a : α), a ∈ ca ∧ R a b
⊢ LiftRelAux R C ca.destruct (Sum.inl b) ↔ ∃ (a : α), a ∈ ca ∧ R a b

Tactic:
rw [← LiftRelAux.swap, LiftRelAux.ret_left]

Premises used: Computation.LiftRelAux.swap, Computation.LiftRelAux.ret_left
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
cb : Computation β
Hc : C ca cb
a : α
ha : a ∈ ca
revert : ∀ (cb : Computation β) (Hc : C ca cb), LiftRel R ca cb
⊢ LiftRel R ca cb

Tactic:
revert cb
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
⊢ ∀ (cb : Computation β) (Hc : C ca cb), LiftRel R ca cb

Tactic:
memRecOn (C := (fun ca ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb))
    ha ?_ (fun ca' IH => ?_)

Premises used: Computation.memRecOn
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
refine_1 : ∀ (cb : Computation β), C (pure a) cb → LiftRel R (pure a) cb
refine_2 :
  ∀ (ca' : Computation α) (IH : (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'),
    (fun (ca : Computation α) ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'.think
⊢ ∀ (cb : Computation β) (Hc : C ca cb), LiftRel R ca cb

Tactic:
refine memRecOn (C := (fun ca ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb))
    ha ?_ (fun ca' IH => ?_)

Premises used: Computation.memRecOn
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
⊢ LiftRelAux R C (pure a).destruct cb.destruct

Tactic:
have h := H Hc