awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
b : β
k : ℕ
zero :
  ∀ {s : Computation α},
    (s.bind f).Results b 0 → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ 0 = n + m
⊢ (s.bind f).Results b k → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ k = n + m
have succ : ∀ (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 α},
  (s.bind f).Results b (n + 1) →
    ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
Tactic: induction k generalizing s with | zero | succ n IH
Cleared hypotheses: s, k
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
⊢ (s.bind f).Results b 0 → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ 0 = n + m
have zero : ∀ (a : α) (h : ((pure a).bind f).Results b 0),
  ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m
Tactic: induction s using recOn with intro h | pure a | think s'
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
zero :
  ∀ (a : α) (h : ((pure a).bind f).Results b 0),
    ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m
⊢ (s.bind f).Results b 0 → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ 0 = n + m
have zero₁ : ∀ (s' : Computation α) (h : (s'.think.bind f).Results b 0),
  ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m
Tactic: induction s using recOn with intro h | pure a | think s'
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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 α
⊢ (s.bind f).Results b (n + 1) →
    ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
have succ : ∀ (a : α) (h : ((pure a).bind f).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: induction s using recOn with intro h | pure a | think s'
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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 α
succ :
  ∀ (a : α) (h : ((pure a).bind f).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
⊢ (s.bind f).Results b (n + 1) →
    ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
have succ₁ : ∀ (s' : Computation α) (h : (s'.think.bind f).Results b (n + 1)),
  ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
Tactic: induction s using recOn with intro h | pure a | think s'
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : ((pure a).bind f).Results b 0
⊢ ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m
have h₁ : (f a).Results b 0
Tactic: simp only [ret_bind] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
⊢ ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m
have this : (s'.think.bind f).head = ((pure b).thinkN 0).head
Tactic: have := congr_arg head (eq_thinkN h)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
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)
⊢ ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m
have h₁ : (f a).Results b (n + 1)
Tactic: simp only [ret_bind] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
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)
⊢ ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
have h₁ : (s'.bind f).Results b n
Tactic: simp only [think_bind, results_think_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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_1 : ℕ), s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
have 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
Tactic: let ⟨a, m, n', h1, h2, e'⟩ := IH h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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 : ℕ), ∃ (n_1 : ℕ), s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
have succ : ∃ (a : α), ∃ (m_1 : ℕ), ∃ (n : ℕ), s'.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1
Tactic: rw [e']
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
⊢ b = b'
have rcases : ∀ (a' : α) (a's : a' ∈ s) (ba' : b' ∈ f a'), b = b'
Tactic: rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
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'
have ba'₁ : b' ∈ f a
Tactic: rw [← h1 a's] at ba'
Cleared hypotheses: ba'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ map f s
have rw : f a ∈ s.bind (pure ∘ f)
Tactic: rw [← bind_pure]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)
have apply : f a ∈ (pure ∘ f) a
Tactic: apply mem_bind m
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ map f s
⊢ ∃ (a : α), a ∈ s ∧ f a = b
have h₁ : b ∈ s.bind (pure ∘ f)
Tactic: rw [← bind_pure] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
⊢ ∃ (a : α), a ∈ s ∧ f a = b
have let : ∀ (a : α) (as : a ∈ s) (fb : b ∈ (pure ∘ f) a), ∃ (a : α), a ∈ s ∧ f a = b
Tactic: let ⟨a, as, fb⟩ := exists_of_mem_bind h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst : s.Terminates
⊢ (map f s).Terminates
have rw : (s.bind (pure ∘ f)).Terminates
Tactic: rw [← bind_pure]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c : Computation α
⊢ (empty α <|> c) = c
have apply : IsBisimulation.{u} (α := α) fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁
Tactic: apply eq_of_bisim (fun c₁ c₂ => (empty α <|> c₂) = c₁) _ rfl
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct
have rw : BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s.think).destruct s.think.destruct
have think : BisimO (fun (c₁ c₂ : Computation α) ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> s.think).destruct
  s.think.destruct
Tactic: rw [think_empty]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> s.think).destruct
    s.think.destruct
have think : ((empty α).think <|> s) = (empty α <|> s)
Tactic: simp only [BisimO, orElse_think, destruct_think]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ ((empty α).think <|> s) = (empty α <|> s)
have think : (empty α <|> s) = (empty α <|> s)
Tactic: rw [← think_empty]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct
have pure : ∀ (s : α) (h : (empty α <|> pure s) = s'),
  BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> pure s).destruct (pure 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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct
have 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
Tactic: induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct
have think : ∀ (s : Computation α) (h : (empty α <|> s.think) = s'),
  BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s.think).destruct s.think.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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct
have 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
Tactic: induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c : Computation α
⊢ (c <|> empty α) = c
have apply : IsBisimulation.{u} (α := α) fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁
Tactic: apply eq_of_bisim (fun c₁ c₂ => (c₂ <|> empty α) = c₁) _ rfl
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct
have rw : BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s.think <|> empty α).destruct s.think.destruct
have think : BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct
  s.think.destruct
Tactic: rw [think_empty]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct
    s.think.destruct
have think : (s <|> (empty α).think) = (s <|> empty α)
Tactic: simp only [BisimO, orElse_think, destruct_think]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ (s <|> (empty α).think) = (s <|> empty α)
have think : (s <|> empty α) = (s <|> empty α)
Tactic: rw [← think_empty]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct
have pure : ∀ (s : α) (h : (pure s <|> empty α) = s'),
  BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (pure s <|> empty α).destruct (pure 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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct
have 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
Tactic: induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct
have think : ∀ (s : Computation α) (h : (s.think <|> empty α) = s'),
  BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s.think <|> empty α).destruct s.think.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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
⊢ BisimO (fun (c₁ c₂ : Computation α) ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct
have 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
Tactic: induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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₁
⊢ a ∈ c₂
have let : ∀ (b : α) (b2 : b ∈ c₂) (ab : a = b), a ∈ c₂
Tactic: let ⟨b, b2, ab⟩ := h1 a1
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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₂
⊢ a ∈ c₁
have let : ∀ (b : α) (b1 : b ∈ c₁) (ab : b = a), a ∈ c₁
Tactic: let ⟨b, b1, ab⟩ := h2 a2
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
⊢ R a b
have let : ∀ (b' : β) (mb' : b' ∈ cb) (ab' : R a b'), R a b
Tactic: let ⟨b', mb', ab'⟩ := l ma
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
have rw : ∃ (b : β), b ∈ cb ∧ R a b
Tactic: rw [mem_unique ma' ma]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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'
have rw : ∃ (a : α), a ∈ ca ∧ R a b
Tactic: rw [mem_unique mb' mb]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b
have let : ∀ (b' : β) (mb' : b' ∈ cb) (ab : R a b'), R a b
Tactic: let ⟨b', mb', ab⟩ := h.left ma
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
b : β
⊢ LiftRel R ca (pure b) ↔ ∃ (a : α), a ∈ ca ∧ R a b
have rw : LiftRel (fun (x : β) (y : α) ↦ R y x) (pure b) ca ↔ ∃ (a : α), a ∈ ca ∧ R a b
Tactic: rw [LiftRel.swap, liftRel_pure_left]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
⊢ LiftRel R ca (pure b) ↔ ∃ (a : α), a ∈ ca ∧ R a b
have rw₁ : (∃ (b_1 : α), b_1 ∈ ca ∧ R b_1 b) ↔ ∃ (a : α), a ∈ ca ∧ R a b
Tactic: rw [LiftRel.swap, liftRel_pure_left]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel R ca cb.think ↔ LiftRel R ca cb
have rw : LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) cb.think ca ↔
  LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) cb ca
Tactic: rw [← LiftRel.swap R, ← LiftRel.swap R]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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)
⊢ LiftRel S (map f1 s1) (map f2 s2)
have rw : LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))
Tactic: rw [← bind_pure, ← bind_pure]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))
have apply : ∀ {a : α} {b : β}, R a b → LiftRel S ((pure ∘ f1) a) ((pure ∘ f2) b)
Tactic: apply liftRel_bind _ _ h1
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ map f s1 ~ map f s2
have rw : LiftRel (fun (x1 x2 : β) ↦ x1 = x2) (map f s1) (map f s2)
Tactic: rw [← lift_eq_iff_equiv]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
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
have rw : LiftRelAux R C (Sum.inl a) (pure b').destruct
Tactic: rw [mem_unique (ret_mem _) mb]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb.think.destruct ↔ ∃ (b : β), b ∈ cb.think ∧ R a b
have think : LiftRelAux R C (Sum.inl a) (Sum.inr cb) ↔ ∃ (b : β), b ∈ cb.think ∧ R a b
Tactic: rw [destruct_think]