awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
n : ℕ
⊢ C ((pure a).thinkN n)
have zero : C ((pure a).thinkN 0)
Tactic: induction n with | zero => exact h1 | succ n IH => exact h2 _ IH
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
n : ℕ
zero : C ((pure a).thinkN 0)
⊢ C ((pure a).thinkN n)
have succ : (n : ℕ) → (IH : C ((pure a).thinkN n)) → C ((pure a).thinkN (n + 1))
Tactic: induction n with | zero => exact h1 | succ n IH => exact h2 _ IH
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
⊢ Stream'.map (fun (o : Option α) ↦ Option.casesOn (motive := fun (x : Option α) ↦ Option β) o none (some ∘ f)) s n =
      some b →
    Stream'.map (fun (o : Option α) ↦ Option.casesOn (motive := fun (x : Option α) ↦ Option β) o none (some ∘ f)) s
        (n + 1) =
      some b
have dsimp : Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (s n) = some b →
  Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (s (n + 1)) = some b
Tactic: dsimp [Stream'.map, Stream'.get]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
⊢ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (s n) = some b →
    Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (s (n + 1)) = some b
have none : ∀ (e : s n = none),
  Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) none = some b →
    Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) (s (n + 1)) = some b
Tactic: rcases e : s n with - | a
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
none :
  ∀ (e : s n = Option.none),
    Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ some (f val)) Option.none =
        some b →
      Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ some (f val)) (s (n + 1)) =
        some b
⊢ Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ some (f val)) (s n) = some b →
    Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ some (f val)) (s (n + 1)) = some b
have some : ∀ (a : α) (e : s n = some a),
  Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ some (f val)) (some a) = some b →
    Option.rec (motive := fun (x : Option α) ↦ Option β) Option.none (fun (val : α) ↦ some (f val)) (s (n + 1)) = some b
Tactic: rcases e : s n with - | a
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ map f
      (think
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s al)) =
    (map f
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
          al)).think
have a : (map f
        (think
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
            al))).val
    (p := fun (x : Stream' (Option β)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : β⦄, x n = some a → x (n + 1) = some a) =
  (map f
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
            al)).think.val
    (p := fun (x : Stream' (Option β)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : β⦄, x n = some a → x (n + 1) = some a)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (map f
          (think
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
              al))).val
      (p := fun (x : Stream' (Option β)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : β⦄, x n = some a → x (n + 1) = some a) =
    (map f
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
              al)).think.val
      (p := fun (x : Stream' (Option β)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : β⦄, x n = some a → x (n + 1) = some a)
have a : Eq.{v + 1} (α := Stream' (Option β))
  (Stream'.map
    (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
    (Stream'.cons none s))
  (Stream'.cons none
    (Stream'.map
      (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
      s))
Tactic: dsimp [think, map]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Eq.{v + 1} (α := Stream' (Option β))
    (Stream'.map
      (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
      (Stream'.cons none s))
    (Stream'.cons none
      (Stream'.map
        (fun (o : Option α) ↦
          Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
        s))
have a : Eq.{v + 1} (α := Stream' (Option β))
  (Stream'.cons (Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) none)
      (Stream'.map
        (fun (o : Option α) ↦
          Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
        s) :
    Stream' (Option β))
  (Stream'.cons none
      (Stream'.map
        (fun (o : Option α) ↦
          Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
        s) :
    Stream' (Option β))
Tactic: rw [Stream'.map_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ (map f s).destruct = lmap f (rmap (map f) s.destruct)
have pure : ∀ (a : α), (map f (pure a)).destruct = lmap f (rmap (map f) (pure a).destruct)
Tactic: induction s using recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
pure : ∀ (a : α), (map f (Computation.pure a)).destruct = lmap f (rmap (map f) (Computation.pure a).destruct)
⊢ (map f s).destruct = lmap f (rmap (map f) s.destruct)
have think : ∀ (s : Computation α), (map f s.think).destruct = lmap f (rmap (map f) s.think.destruct)
Tactic: induction s using recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ map id (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al
have a : (map id
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f
          al)).val
    (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
  Subtype.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
    (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ (map id
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f
            al)).val
      (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    Subtype.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al)
have a : Stream'.map
    (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option α) none (fun (val : α) ↦ some val) o) f =
  f
Tactic: simp only [map, comp_apply, id_eq]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ Eq.{u + 1} (α := (t : Option α) → Option α) (Option.rec (motive := fun (x : Option α) ↦ Option α) none some) id
have h : ∀ (a : α), Option.rec (motive := fun (x : Option α) ↦ Option α) none some none = some a ↔ id none = some a
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
h : ∀ (a : α), Option.rec (motive := fun (x : Option α) ↦ Option α) none some none = some a ↔ id none = some a
⊢ Eq.{u + 1} (α := (t : Option α) → Option α) (Option.rec (motive := fun (x : Option α) ↦ Option α) none some) id
have h₁ : ∀ (val a : α),
  Option.rec (motive := fun (x : Option α) ↦ Option α) none some (some val) = some a ↔ id (some val) = some a
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ Stream'.map
      (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option α) none (fun (val : α) ↦ some val) o) f =
    f
have e : Eq.{u + 1} (α := (t : Option α) → Option α) (Option.rec (motive := fun (x : Option α) ↦ Option α) none some) id
Tactic: have e : @Option.rec α (fun _ => Option α) none some = id := by ext ⟨⟩ <;> rfl
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
e : Eq.{u + 1} (α := (t : Option α) → Option α) (Option.rec (motive := fun (x : Option α) ↦ Option α) none some) id
⊢ Stream'.map
      (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option α) none (fun (val : α) ↦ some val) o) f =
    f
have h : Eq.{u + 1} (α := (x : Option α) → Option α) (fun (x : Option α) ↦ x) id
Tactic: have h : ((fun x : Option α => x) = id) := rfl
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ map (g ∘ f)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s al) =
    map g
      (map f
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s al))
have a : (map (g ∘ f)
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
          al)).val
    (p := fun (x : Stream' (Option γ)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : γ⦄, x n = some a → x (n + 1) = some a) =
  (map g
        (map f
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
            al))).val
    (p := fun (x : Stream' (Option γ)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : γ⦄, x n = some a → x (n + 1) = some a)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (map (g ∘ f)
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
            al)).val
      (p := fun (x : Stream' (Option γ)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : γ⦄, x n = some a → x (n + 1) = some a) =
    (map g
          (map f
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) s
              al))).val
      (p := fun (x : Stream' (Option γ)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : γ⦄, x n = some a → x (n + 1) = some a)
have a : Eq.{w + 1} (α := Stream' (Option γ))
  (Stream'.map
    (fun (o : Option α) ↦
      Option.rec (motive := fun (x : Option α) ↦ Option γ) none (fun (val : α) ↦ some (g (f val))) o)
    s)
  (Stream'.map
    ((fun (o : Option β) ↦ Option.rec (motive := fun (x : Option β) ↦ Option γ) none (fun (val : β) ↦ some (g val)) o) ∘
      fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
    s)
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Eq.{w + 1} (α := Stream' (Option γ))
    (Stream'.map
      (fun (o : Option α) ↦
        Option.rec (motive := fun (x : Option α) ↦ Option γ) none (fun (val : α) ↦ some (g (f val))) o)
      s)
    (Stream'.map
      ((fun (o : Option β) ↦
          Option.rec (motive := fun (x : Option β) ↦ Option γ) none (fun (val : β) ↦ some (g val)) o) ∘
        fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
      s)
have a : Eq (α := Option α → Option γ)
  (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option γ) none (fun (val : α) ↦ some (g (f val))) o)
  ((fun (o : Option β) ↦ Option.rec (motive := fun (x : Option β) ↦ Option γ) none (fun (val : β) ↦ some (g val)) o) ∘
    fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
Tactic: apply congr_arg fun f : _ → Option γ => Stream'.map f s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Eq (α := Option α → Option γ)
    (fun (o : Option α) ↦
      Option.rec (motive := fun (x : Option α) ↦ Option γ) none (fun (val : α) ↦ some (g (f val))) o)
    ((fun (o : Option β) ↦ Option.rec (motive := fun (x : Option β) ↦ Option γ) none (fun (val : β) ↦ some (g val)) o) ∘
      fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
have a : ∀ (a : γ),
  Option.rec (motive := fun (x : Option α) ↦ Option γ) none (fun (val : α) ↦ some (g (f val))) none = some a ↔
    ((fun (o : Option β) ↦ Option.rec (motive := fun (x : Option β) ↦ Option γ) none (fun (val : β) ↦ some (g val)) o) ∘
          fun (o : Option α) ↦
          Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
        none =
      some a
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
a :
  ∀ (a : γ),
    Option.rec (motive := fun (x : Option α) ↦ Option γ) none (fun (val : α) ↦ some (g (f val))) none = some a ↔
      ((fun (o : Option β) ↦
              Option.rec (motive := fun (x : Option β) ↦ Option γ) none (fun (val : β) ↦ some (g val)) o) ∘
            fun (o : Option α) ↦
            Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
          none =
        some a
⊢ Eq (α := Option α → Option γ)
    (fun (o : Option α) ↦
      Option.rec (motive := fun (x : Option α) ↦ Option γ) none (fun (val : α) ↦ some (g (f val))) o)
    ((fun (o : Option β) ↦ Option.rec (motive := fun (x : Option β) ↦ Option γ) none (fun (val : β) ↦ some (g val)) o) ∘
      fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
have a₁ : ∀ (val : α) (a : γ),
  Option.rec (motive := fun (x : Option α) ↦ Option γ) none (fun (val : α) ↦ some (g (f val))) (some val) = some a ↔
    ((fun (o : Option β) ↦ Option.rec (motive := fun (x : Option β) ↦ Option γ) none (fun (val : β) ↦ some (g val)) o) ∘
          fun (o : Option α) ↦
          Option.rec (motive := fun (x : Option α) ↦ Option β) none (fun (val : α) ↦ some (f val)) o)
        (some val) =
      some a
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ (pure a).bind f = f a
have bisim : IsBisimulation.{v} (α := β) fun (c₁ c₂ : Computation β) ↦
  c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
Tactic: apply
    eq_of_bisim fun c₁ c₂ => c₁ = bind (pure a) f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
bisim :
  IsBisimulation.{v} (α := β) fun (c₁ c₂ : Computation β) ↦
    c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
⊢ (pure a).bind f = f a
have r : (pure a).bind f = (pure a).bind f ∧ f a = f a ∨ (pure a).bind f = corec (Bind.f f) (Sum.inr (f a))
Tactic: apply
    eq_of_bisim fun c₁ c₂ => c₁ = bind (pure a) f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂))
    ((pure a).bind f).destruct (f a).destruct
have simp : match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
  match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (f a).destruct with
  | Sum.inl a => Sum.inl a
  | Sum.inr b => Sum.inr (corec (Bind.f f) b),
  (f a).destruct with
| Sum.inl a, Sum.inl a' => a = a'
| Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
| x, x_1 => False
Tactic: simp only [BisimO, bind, Bind.f, corec_eq, rmap, destruct_pure]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
⊢ match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (f a).destruct with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    (f a).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
have inl : ∀ (b : β),
  match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (Sum.inl b) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
Tactic: rcases destruct (f a) with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
inl :
  ∀ (b : β),
    match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
      match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (Sum.inl b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (corec (Bind.f f) b),
      Sum.inl b with
    | Sum.inl a, Sum.inl a' => a = a'
    | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
    | x, x_1 => False
⊢ match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (f a).destruct with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    (f a).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
have inr : ∀ (cb : Computation β),
  match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
Tactic: rcases destruct (f a) with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c : Computation β
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂))
    (corec (Bind.f f) (Sum.inr c)).destruct c.destruct
have simp : match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
  match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g c.destruct with
  | Sum.inl a => Sum.inl a
  | Sum.inr b => Sum.inr (corec (Bind.f f) b),
  c.destruct with
| Sum.inl a, Sum.inl a' => a = a'
| Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
| x, x_1 => False
Tactic: simp only [BisimO, Bind.f, corec_eq, rmap]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c : Computation β
⊢ match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g c.destruct with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    c.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
have inl : ∀ (b : β),
  match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (Sum.inl b) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
Tactic: rcases destruct c with b | cb