awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : (f a).Results b 0
⊢ ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m

Tactic:
exact ⟨_, _, _, results_pure _, h, rfl⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
⊢ (s'.think.bind f).head = ((pure b).thinkN 0).head

Tactic:
have := congr_arg head (eq_thinkN h)
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
this : (s'.think.bind f).head = ((pure b).thinkN 0).head
⊢ ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : ((pure a).bind f).Results b (n + 1)
⊢ (f a).Results b (n + 1)

Tactic:
simp only [ret_bind] at h

Premises used: Computation.ret_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : (f a).Results b (n + 1)
⊢ ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
⟨_, _, n + 1, results_pure _, h, rfl⟩

Premises used: HAdd.hAdd, Computation.results_pure, And.intro, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : (f a).Results b (n + 1)
⊢ ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
exact ⟨_, _, n + 1, results_pure _, h, rfl⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.think.bind f).Results b (n + 1)
⊢ (s'.bind f).Results b n

Tactic:
simp only [think_bind, results_think_iff] at h

Premises used: Computation.results_think_iff, Computation.think_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
succ :
  ∀ (a : α) (m n' : ℕ) (h1 : s'.Results a m) (h2 : (f a).Results b n') (e' : n = n' + m),
    ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
⊢ ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
let ⟨a, m, n', h1, h2, e'⟩ := IH h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
a : α
m n' : ℕ
h1 : s'.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
succ : ∃ (a : α), ∃ (m_1 : ℕ), ∃ (n : ℕ), s'.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1
⊢ ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
rw [e']
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
a : α
m n' : ℕ
h1 : s'.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ (a : α), ∃ (m_1 : ℕ), ∃ (n : ℕ), s'.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1

Tactic:
⟨a, m.succ, n', results_think h1, h2, rfl⟩

Premises used: Computation.results_think, And.intro, Exists.intro, Nat.succ, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
a : α
m n' : ℕ
h1 : s'.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ (a : α), ∃ (m_1 : ℕ), ∃ (n : ℕ), s'.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1

Tactic:
exact ⟨a, m.succ, n', results_think h1, h2, rfl⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
b : β
h : b ∈ s.bind f
⊢ ∃ (a : α), a ∈ s ∧ b ∈ f a

Tactic:
let ⟨_, h⟩ := exists_results_of_mem h
  let ⟨a, _, _, h1, h2, _⟩ := of_results_bind h
  ⟨a, h1.mem, h2.mem⟩

Premises used: Computation.exists_results_of_mem, Membership.mem, Exists, _private.0.Computation.exists_of_mem_bind.match_1, _private.0.Computation.exists_of_mem_bind.match_2, And, And.intro, Exists.intro, Computation.Results.mem, Computation.of_results_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
rcases : ∀ (a' : α) (a's : a' ∈ s) (ba' : b' ∈ f a'), b = b'
⊢ b = b'

Tactic:
rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩

Premises used: Computation.exists_of_mem_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a'
⊢ b' ∈ f a

Tactic:
rw [← h1 a's] at ba'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'

Tactic:
h2 ba'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'

Tactic:
exact h2 ba'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
⊢ LawfulMonad Computation

Tactic:
LawfulMonad.mk'
  (id_map := @map_id)
  (bind_pure_comp := @bind_pure)
  (pure_bind := @ret_bind)
  (bind_assoc := @bind_assoc)

Premises used: Computation.bind_assoc, Computation.map_id, Computation.bind_pure, LawfulMonad.mk', Computation.ret_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α β : Type u
f : α → β
c : Computation α
⊢ f <$> c = map f c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ Pure.pure a = pure a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α β : Type u_1
⊢ ∀ (f : α → β) (a : α), f <$> pure a = pure (f a)

Tactic:
map_pure

Premises used: Computation.map_pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α β : Type u_1
⊢ ∀ (f : α → β) (s : Computation α), f <$> s.think = (f <$> s).think

Tactic:
map_think

Premises used: Computation.map_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
rw : f a ∈ s.bind (pure ∘ f)
⊢ f a ∈ map f s

Tactic:
rw [← bind_pure]

Premises used: Computation.bind_pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
apply : f a ∈ (pure ∘ f) a
⊢ f a ∈ s.bind (pure ∘ f)

Tactic:
apply mem_bind m

Premises used: Computation.mem_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ (pure ∘ f) a

Tactic:
apply ret_mem

Premises used: Computation.ret_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ map f s
⊢ b ∈ s.bind (pure ∘ f)

Tactic:
rw [← bind_pure] at h

Premises used: Computation.bind_pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
let : ∀ (a : α) (as : a ∈ s) (fb : b ∈ (pure ∘ f) a), ∃ (a : α), a ∈ s ∧ f a = b
⊢ ∃ (a : α), a ∈ s ∧ f a = b

Tactic:
let ⟨a, as, fb⟩ := exists_of_mem_bind h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
a : α
as : a ∈ s
fb : b ∈ (pure ∘ f) a
⊢ ∃ (a : α), a ∈ s ∧ f a = b

Tactic:
⟨a, as, mem_unique (ret_mem _) fb⟩

Premises used: Computation.mem_unique, And.intro, Exists.intro, Computation.ret_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
a : α
as : a ∈ s
fb : b ∈ (pure ∘ f) a
⊢ ∃ (a : α), a ∈ s ∧ f a = b

Tactic:
exact ⟨a, as, mem_unique (ret_mem _) fb⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst : s.Terminates
rw : (s.bind (pure ∘ f)).Terminates
⊢ (map f s).Terminates

Tactic:
rw [← bind_pure]

Premises used: Computation.bind_pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst : s.Terminates
⊢ (s.bind (pure ∘ f)).Terminates

Tactic:
terminates_of_mem (mem_bind (get_mem s) (get_mem (α := β) (f (get s))))

Premises used: Computation.get_mem, Computation.pure, Computation.terminates_of_mem, Computation.get, Computation.mem_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst : s.Terminates
⊢ (s.bind (pure ∘ f)).Terminates

Tactic:
exact terminates_of_mem (mem_bind (get_mem s) (get_mem (α := β) (f (get s))))

Premises used: Computation.get_mem, Computation.terminates_of_mem, Computation.mem_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ (map f s).Terminates ↔ s.Terminates

Tactic:
⟨fun ⟨⟨_, h⟩⟩ =>
    let ⟨_, h1, _⟩ := exists_of_mem_map h
    ⟨⟨_, h1⟩⟩,
    @Computation.terminates_map _ _ _ _⟩

Premises used: Computation.Terminates.mk, Computation.exists_of_mem_map, Computation.Terminates, Computation.terminates_map, _private.0.Computation.terminates_map_iff.match_1, _private.0.Computation.terminates_map_iff.match_2, Iff.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
c₂ : Computation α
⊢ ((pure a).orElse fun (x : Unit) ↦ c₂).destruct = Sum.inl a

Tactic:
simp [orElse]

Premises used: Computation.orElse
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ : Computation α
a : α
⊢ (c₁.think.orElse fun (x : Unit) ↦ pure a).destruct = Sum.inl a

Tactic:
simp [orElse]

Premises used: Computation.orElse
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ c₂ : Computation α
⊢ (c₁.think.orElse fun (x : Unit) ↦ c₂.think).destruct = Sum.inr (c₁.orElse fun (x : Unit) ↦ c₂)

Tactic:
simp [orElse]

Premises used: Computation.orElse
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c : Computation α
apply : IsBisimulation.{u} (α := α) fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁
⊢ (empty α <|> c) = c

Tactic:
apply eq_of_bisim (fun c₁ c₂ => (empty α <|> c₂) = c₁) _ rfl

Premises used: Computation.empty, HOrElse.hOrElse, Computation.eq_of_bisim, Eq
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
rw : BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct

Tactic:
rw [← h]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' : Computation α
s : α
h : (empty α <|> pure s) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> pure s).destruct
    (pure s).destruct

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
think :
  BisimO (fun (c₁ c₂ : Computation α) ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> s.think).destruct
    s.think.destruct
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s.think).destruct s.think.destruct

Tactic:
rw [think_empty]

Premises used: Computation.think_empty
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
think : ((empty α).think <|> s) = (empty α <|> s)
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> s.think).destruct
    s.think.destruct

Tactic:
simp only [BisimO, orElse_think, destruct_think]

Premises used: Computation.destruct_think, Computation.BisimO, Computation.orElse_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
think think₁ : (empty α <|> s) = (empty α <|> s)
⊢ ((empty α).think <|> s) = (empty α <|> s)

Tactic:
rw [← think_empty]

Premises used: Computation.think_empty
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
pure :
  ∀ (s : α) (h : (empty α <|> Computation.pure s) = s'),
    BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> Computation.pure s).destruct
      (Computation.pure s).destruct
pure₁ :
  ∀ (s : α) (h : (empty α <|> Computation.pure s) = s'),
    BisimO (fun (c₁ c₂ : Computation α) ↦ ((empty α).think <|> c₂) = c₁)
      ((empty α).think <|> Computation.pure s).destruct (Computation.pure s).destruct
think :
  ∀ (s : Computation α) (h : (empty α <|> s.think) = s'),
    BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s.think).destruct s.think.destruct
think₁ :
  ∀ (s : Computation α) (h : (empty α <|> s.think) = s'),
    BisimO (fun (c₁ c₂ : Computation α) ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> s.think).destruct
      s.think.destruct
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct

Tactic:
induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]

Premises used: Computation.think, Computation.think_empty, Computation.pure, Computation.destruct_think, Computation.BisimO, Computation.orElse_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c : Computation α
apply : IsBisimulation.{u} (α := α) fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁
⊢ (c <|> empty α) = c

Tactic:
apply eq_of_bisim (fun c₁ c₂ => (c₂ <|> empty α) = c₁) _ rfl

Premises used: Computation.empty, HOrElse.hOrElse, Computation.eq_of_bisim, Eq
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
rw : BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct

Tactic:
rw [← h]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' : Computation α
s : α
h : (pure s <|> empty α) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> (empty α).think) = c₁) (pure s <|> (empty α).think).destruct
    (pure s).destruct

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
think :
  BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct
    s.think.destruct
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s.think <|> empty α).destruct s.think.destruct

Tactic:
rw [think_empty]

Premises used: Computation.think_empty
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
think : (s <|> (empty α).think) = (s <|> empty α)
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct
    s.think.destruct

Tactic:
simp only [BisimO, orElse_think, destruct_think]

Premises used: Computation.destruct_think, Computation.BisimO, Computation.orElse_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
think think₁ : (s <|> empty α) = (s <|> empty α)
⊢ (s <|> (empty α).think) = (s <|> empty α)

Tactic:
rw [← think_empty]

Premises used: Computation.think_empty
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
pure :
  ∀ (s : α) (h : (Computation.pure s <|> empty α) = s'),
    BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (Computation.pure s <|> empty α).destruct
      (Computation.pure s).destruct
pure₁ :
  ∀ (s : α) (h : (Computation.pure s <|> empty α) = s'),
    BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> (empty α).think) = c₁)
      (Computation.pure s <|> (empty α).think).destruct (Computation.pure s).destruct
think :
  ∀ (s : Computation α) (h : (s.think <|> empty α) = s'),
    BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s.think <|> empty α).destruct s.think.destruct
think₁ :
  ∀ (s : Computation α) (h : (s.think <|> empty α) = s'),
    BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct
      s.think.destruct
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct

Tactic:
induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]

Premises used: Computation.think, Computation.think_empty, Computation.pure, Computation.destruct_think, Computation.BisimO, Computation.orElse_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
⊢ s ~ s

Tactic:
fun _ => Iff.rfl

Premises used: Iff.rfl, Computation.Equiv
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s t : Computation α
⊢ s ~ t → t ~ s

Tactic:
fun h a => (h a).symm

Premises used: Computation.Equiv, Iff.symm
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s t u : Computation α
⊢ s ~ t → t ~ u → s ~ u

Tactic:
fun h1 h2 a =>
  (h1 a).trans (h2 a)

Premises used: Computation.Equiv, Iff.trans
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
⊢ Equivalence.{u + 1} (α := Computation α) Equiv

Tactic:
⟨@Equiv.refl _, @Equiv.symm _, @Equiv.trans _⟩

Premises used: Computation.Equiv.symm, Computation.Equiv.refl, Equivalence.mk, Computation.Equiv.trans
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
rw : a ∈ t
⊢ a' ∈ t

Tactic:
rw [mem_unique ma h1]

Premises used: Computation.mem_unique
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t

Tactic:
h2
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t

Tactic:
exact h2
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
rw : a ∈ s
⊢ a' ∈ s

Tactic:
rw [mem_unique ma h2]

Premises used: Computation.mem_unique
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s

Tactic:
h1
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s

Tactic:
exact h1
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ c₂ : Computation α
h : c₁ ~ c₂
⊢ c₁.Terminates ↔ c₂.Terminates

Tactic:
simp only [terminates_iff, exists_congr h]

Premises used: exists_congr, Computation.terminates_iff
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ c₂ : Computation α
h : c₁ ~ c₂
a : α
⊢ c₁ ~> a ↔ c₂ ~> a

Tactic:
forall_congr' fun a' => imp_congr (h a') Iff.rfl

Premises used: Iff.rfl, Computation.Promises, imp_congr, forall_congr'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ c₂ : Computation α
h : c₁ ~ c₂
inst : c₁.Terminates
inst_1 : c₂.Terminates
⊢ c₁.get = c₂.get

Tactic:
get_eq_of_mem _ <| (h _).2 <| get_mem _

Premises used: Iff.mpr, Computation.get_mem, Computation.get_eq_of_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
⊢ s.think ~ s

Tactic:
fun _ => ⟨of_think_mem, think_mem⟩

Premises used: Computation.think_mem, Iff.intro, Computation.Equiv, Computation.of_think_mem
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
n : ℕ
⊢ s.thinkN n ~ s

Tactic:
fun _ => thinkN_mem n

Premises used: Computation.thinkN_mem, Computation.Equiv
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s1 s2 : Computation α
f1 f2 : α → Computation β
h1 : s1 ~ s2
h2 : ∀ (a : α), f1 a ~ f2 a
⊢ s1.bind f1 ~ s2.bind f2

Tactic:
fun b =>
  ⟨fun h =>
    let ⟨a, ha, hb⟩ := exists_of_mem_bind h
    mem_bind ((h1 a).1 ha) ((h2 a b).1 hb),
    fun h =>
    let ⟨a, ha, hb⟩ := exists_of_mem_bind h
    mem_bind ((h1 a).2 ha) ((h2 a b).2 hb)⟩

Premises used: Iff.mpr, Membership.mem, Computation.exists_of_mem_bind, Iff.intro, Computation.Equiv, Iff.mp, Computation.bind, _private.0.Computation.bind_congr.match_1, Computation.mem_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
h : a ∈ s
⊢ s ~ pure a

Tactic:
equiv_of_mem h (ret_mem _)

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

Tactic:
@and_comm _ _

Premises used: and_comm, Computation.LiftRel
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ c₂ : Computation α
h : LiftRel (fun (x1 x2 : α) ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ (b : α), b ∈ c₂ ∧ (fun (x1 x2 : α) ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ (a : α), a ∈ c₁ ∧ (fun (x1 x2 : α) ↦ x1 = x2) a b
a1 : a ∈ c₁
let : ∀ (b : α) (b2 : b ∈ c₂) (ab : a = b), a ∈ c₂
⊢ a ∈ c₂

Tactic:
let ⟨b, b2, ab⟩ := h1 a1
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ c₂ : Computation α
h : LiftRel (fun (x1 x2 : α) ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ (b : α), b ∈ c₂ ∧ (fun (x1 x2 : α) ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ (a : α), a ∈ c₁ ∧ (fun (x1 x2 : α) ↦ x1 = x2) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun (x1 x2 : α) ↦ x1 = x2) a b
rwa rwa₁ rwa₂ rwa₃ : b ∈ c₂
⊢ a ∈ c₂

Tactic:
rwa [ab]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ c₂ : Computation α
h : LiftRel (fun (x1 x2 : α) ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ (b : α), b ∈ c₂ ∧ (fun (x1 x2 : α) ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ (a : α), a ∈ c₁ ∧ (fun (x1 x2 : α) ↦ x1 = x2) a b
a2 : a ∈ c₂
let : ∀ (b : α) (b1 : b ∈ c₁) (ab : b = a), a ∈ c₁
⊢ a ∈ c₁

Tactic:
let ⟨b, b1, ab⟩ := h2 a2
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
c₁ c₂ : Computation α
h : LiftRel (fun (x1 x2 : α) ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ (b : α), b ∈ c₂ ∧ (fun (x1 x2 : α) ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ (a : α), a ∈ c₁ ∧ (fun (x1 x2 : α) ↦ x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun (x1 x2 : α) ↦ x1 = x2) b a
rwa rwa₁ rwa₂ rwa₃ : b ∈ c₁
⊢ a ∈ c₁

Tactic:
rwa [← ab]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : α → α → Prop
H : Symmetric R
⊢ Symmetric (LiftRel R)

Tactic:
fun _ _ ⟨l, r⟩ =>
  ⟨fun {_} a2 =>
    let ⟨b, b1, ab⟩ := r a2
    ⟨b, b1, H ab⟩,
    fun {_} a1 =>
    let ⟨b, b2, ab⟩ := l a1
    ⟨b, b2, H ab⟩⟩

Premises used: _private.0.Computation.LiftRel.symm.match_2, _private.0.Computation.LiftRel.symm.match_1, Symmetric, Membership.mem, Exists, _private.0.Computation.LiftRel.symm.match_3, And, And.intro, Exists.intro, Computation.LiftRel