awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
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
h₁ :
  ∀ (val a : α),
    Option.rec (motive := fun (x : Option α) ↦ Option α) none some (some val) = some a ↔ id (some val) = some a
⊢ Eq.{u + 1} (α := (t : Option α) → Option α) (Option.rec (motive := fun (x : Option α) ↦ Option α) none some) id

Tactic:
ext ⟨⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
a : α
⊢ Option.rec (motive := fun (x : Option α) ↦ Option α) none some none = some a ↔ id none = some a

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
val a : α
⊢ Option.rec (motive := fun (x : Option α) ↦ Option α) none some (some val) = some a ↔ id (some val) = some a

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
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

Tactic:
have e : @Option.rec α (fun _ => Option α) none some = id := by ext ⟨⟩ <;> rfl
-- Module: Mathlib.Data.Seq.Computation
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
⊢ Eq.{u + 1} (α := (x : Option α) → Option α) (fun (x : Option α) ↦ x) id

Tactic:
have h : ((fun x : Option α => x) = id) := rfl
-- Module: Mathlib.Data.Seq.Computation
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
h : Eq.{u + 1} (α := (x : Option α) → Option α) (fun (x : Option α) ↦ x) id
⊢ Stream'.map
      (fun (o : Option α) ↦ Option.rec (motive := fun (x : Option α) ↦ Option α) none (fun (val : α) ↦ some val) o) f =
    f

Tactic:
simp [e, h, Stream'.map_id]

Premises used: Stream'.map_id
-- Module: Mathlib.Data.Seq.Computation
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 :
  (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)
⊢ 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))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Computation
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 :
  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)
⊢ (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:
dsimp [map]

Premises used: Computation.map
-- Module: Mathlib.Data.Seq.Computation
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 :
  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)
⊢ 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:
apply congr_arg fun f : _ → Option γ => Stream'.map f s

Premises used: congr_arg, Stream'.map
-- Module: Mathlib.Data.Seq.Computation
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
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
⊢ 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:
ext ⟨⟩
-- Module: Mathlib.Data.Seq.Computation
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 : γ
⊢ 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:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some 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:
rfl
-- Module: Mathlib.Data.Seq.Computation
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₂)
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))
⊢ (pure a).bind f = 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₂)

Premises used: Computation.corec, Computation.Bind.f, And, Sum.inr, Computation.pure, Or, Computation.eq_of_bisim, Computation.bind, Eq
-- Module: Mathlib.Data.Seq.Computation
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₂)
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
⊢ 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

Tactic:
simp only [BisimO, bind, Bind.f, corec_eq, rmap, destruct_pure]

Premises used: Computation.destruct_pure, Computation.rmap, Computation.Bind.f, Computation.corec_eq, Computation.BisimO, Computation.bind
-- Module: Mathlib.Data.Seq.Computation
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
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
⊢ 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:
rcases destruct (f a) with b | cb

Premises used: Computation.destruct
-- Module: Mathlib.Data.Seq.Computation
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₂)
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:
simp [Bind.g]

Premises used: Computation.Bind.g
-- Module: Mathlib.Data.Seq.Computation
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₂)
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:
simp [Bind.g]

Premises used: Computation.Bind.g
-- Module: Mathlib.Data.Seq.Computation
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 β
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
⊢ 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

Tactic:
simp only [BisimO, Bind.f, corec_eq, rmap]

Premises used: Computation.rmap, Computation.Bind.f, Computation.corec_eq, Computation.BisimO
-- Module: Mathlib.Data.Seq.Computation
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 β
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
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 = (pure a).bind f ∧ 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 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:
rcases destruct c with b | cb

Premises used: Computation.destruct
-- Module: Mathlib.Data.Seq.Computation
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 β
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:
simp [Bind.g]

Premises used: Computation.Bind.g
-- Module: Mathlib.Data.Seq.Computation
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 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 = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
simp [Bind.g]

Premises used: Computation.Bind.g
-- Module: Mathlib.Data.Seq.Computation
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₂))
    c₁.destruct c₂.destruct

Tactic:
match c₁, c₂, h with
    | _, _, Or.inl ⟨rfl, rfl⟩ =>
      simp only [BisimO, bind, Bind.f, corec_eq, rmap, destruct_pure]
      rcases destruct (f a) with b | cb <;> simp [Bind.g]
    | _, c, Or.inr rfl =>
      simp only [BisimO, Bind.f, corec_eq, rmap]
      rcases destruct c with b | cb <;> simp [Bind.g]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ (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:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
c : Computation α
f : α → Computation β
⊢ (c.think.bind f).destruct = Sum.inr (c.bind f)

Tactic:
simp [bind, Bind.f]

Premises used: Computation.Bind.f, Computation.bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
bisim :
  IsBisimulation.{v} (α := β) fun (c₁ c₂ : Computation β) ↦
    c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
r : s.bind (pure ∘ f) = map f s ∨ ∃ (s_1 : Computation α), s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1
⊢ s.bind (pure ∘ f) = map f s

Tactic:
apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s

Premises used: Function.comp, Exists, And, Computation.map, Computation.pure, Or, Computation.eq_of_bisim, Computation.bind, Eq
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂_1 : Computation β
h : c₁ = c₂_1 ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂_1 = map f s
c₂ : Computation β
inl :
  ∀ (b : β),
    BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
      (Sum.inl b) (Sum.inl b)
inr :
  ∀ (cb : Computation β),
    BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
      (Sum.inr cb) (Sum.inr cb)
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    c₂.destruct c₂.destruct

Tactic:
rcases destruct c₂ with b | cb

Premises used: Computation.destruct
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂_1 : Computation β
h : c₁ = c₂_1 ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂_1 = map f s
c₂ : Computation β
b : β
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    (Sum.inl b) (Sum.inl b)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂_1 : Computation β
h : c₁ = c₂_1 ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂_1 = map f s
c₂ cb : Computation β
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    (Sum.inr cb) (Sum.inr cb)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s_1 : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s : α
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    ((pure s).bind (pure ∘ f)).destruct (map f (pure s)).destruct

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s_1 : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s : Computation α
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    (s.think.bind (pure ∘ f)).destruct (map f s.think).destruct

Tactic:
simpa using Or.inr ⟨s, rfl, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s_1 : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (Computation.pure ∘ f) ∧ c₂ = map f s
s : Computation α
pure :
  ∀ (s : α),
    BisimO
      (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (Computation.pure ∘ f) ∧ c₂ = map f s)
      ((Computation.pure s).bind (Computation.pure ∘ f)).destruct (map f (Computation.pure s)).destruct
think :
  ∀ (s : Computation α),
    BisimO
      (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (Computation.pure ∘ f) ∧ c₂ = map f s)
      (s.think.bind (Computation.pure ∘ f)).destruct (map f s.think).destruct
⊢ BisimO
    (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (Computation.pure ∘ f) ∧ c₂ = map f s)
    (s.bind (Computation.pure ∘ f)).destruct (map f s).destruct

Tactic:
induction s using recOn with
      | pure s => simp
      | think s => simpa using Or.inr ⟨s, rfl, rfl⟩

Premises used: Computation.think, Computation.pure, Or.inr
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    c₁.destruct c₂.destruct

Tactic:
match c₁, c₂, h with
    | _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
    | _, _, Or.inr ⟨s, rfl, rfl⟩ =>
      induction s using recOn with
      | pure s => simp
      | think s => simpa using Or.inr ⟨s, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ (s_1 : Computation α), s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1

Tactic:
Or.inr ⟨s, rfl, rfl⟩

Premises used: And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ (s_1 : Computation α), s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1

Tactic:
exact Or.inr ⟨s, rfl, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
⊢ s.bind pure = s

Tactic:
simpa using bind_pure id s

Premises used: id, Computation.bind_pure