awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : Computation α
a : Stream' (Option α)
s' : ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1
H :
  s.destruct =
    Sum.inr (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) a s')
rw :
  motive
    (Computation.think
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) a s'))
⊢ motive s

Tactic:
rw [destruct_eq_think H]

Premises used: Computation.destruct_eq_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : Computation α
a : Stream' (Option α)
s' : ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1
H :
  s.destruct =
    Sum.inr (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) a s')
⊢ motive
    (Computation.think
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) a s'))

Tactic:
apply think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
refine :
  ∀ (n : ℕ) (a' : α) (h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'),
    Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a'
⊢ Computation α

Tactic:
refine ⟨Stream'.corec' (Corec.f f) (Sum.inr b), fun n a' h => ?_⟩
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'
rw : Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd) (n + 1) = some a'
⊢ Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a'

Tactic:
rw [Stream'.corec'_eq]

Premises used: Stream'.corec'_eq
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'
revert :
  ∀ (h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'),
    Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'

Tactic:
revert h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
generalize :
  ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
⊢ ∀ (h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'),
    Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'

Tactic:
generalize Sum.inr b = o

Premises used: Sum.inr
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
o : α ⊕ β
zero : (Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'
⊢ ∀ (h : Stream'.corec' (Corec.f f) o 0 = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd 0 = some a'

Tactic:
change (Corec.f f o).1 = some a' → (Corec.f f (Corec.f f o).2).1 = some a'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
o : α ⊕ β
zero : ∀ (val : α), (Corec.f f (Sum.inl val)).fst = some a' → (Corec.f f (Corec.f f (Sum.inl val)).snd).fst = some a'
zero₁ : ∀ (b : β), (Corec.f f (Sum.inr b)).fst = some a' → (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'
⊢ (Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'

Tactic:
rcases o with _ | b
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' val : α
h : (Corec.f f (Sum.inl val)).fst = some a'
⊢ (Corec.f f (Corec.f f (Sum.inl val)).snd).fst = some a'

Tactic:
h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' val : α
h : (Corec.f f (Sum.inl val)).fst = some a'
⊢ (Corec.f f (Corec.f f (Sum.inl val)).snd).fst = some a'

Tactic:
exact h
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b_1 : β
a' : α
b : β
h : (Corec.f f (Sum.inr b)).fst = some a'
zero :
  Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β))
        Prod.snd (α := Option α)
          (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match (motive := α ⊕ β → Option α) f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)) with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'
⊢ (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'

Tactic:
unfold Corec.f at *

Premises used: Computation.Corec.f
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b_1 : β
a' : α
b : β
h :
  Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'
h_1 :
  ∀ (x : α ⊕ β) (a : α),
    Eq (α := α ⊕ β)
        (Prod.snd (α := Option α)
          (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match (motive := α ⊕ β → Option α) f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)))
        (Sum.inl a) →
      Prod.fst (β := α ⊕ β) (some a, Sum.inl a) = some a'
h_2 :
  ∀ (x : α ⊕ β) (val : β),
    Eq (α := α ⊕ β)
        (Prod.snd (α := Option α)
          (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match (motive := α ⊕ β → Option α) f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)))
        (Sum.inr val) →
      Prod.fst (β := α ⊕ β)
          (match (motive := α ⊕ β → Option α) f val with
            | Sum.inl a => some a
            | Sum.inr val => none,
            f val) =
        some a'
⊢ Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β))
        Prod.snd (α := Option α)
          (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match (motive := α ⊕ β → Option α) f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)) with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'

Tactic:
split
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b_1 : β
a' : α
b : β
h :
  Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'
x : α ⊕ β
a : α
heq :
  Eq (α := α ⊕ β)
    (Prod.snd (α := Option α)
      (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)))
    (Sum.inl a)
⊢ Prod.fst (β := α ⊕ β) (some a, Sum.inl a) = some a'

Tactic:
simp_all
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b_1 : β
a' : α
b : β
h :
  Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'
x : α ⊕ β
val : β
heq :
  Eq (α := α ⊕ β)
    (Prod.snd (α := Option α)
      (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)))
    (Sum.inr val)
⊢ Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α) f val with
        | Sum.inl a => some a
        | Sum.inr val => none,
        f val) =
    some a'

Tactic:
simp_all
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH :
  ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
succ :
  ∀ (h : Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a'),
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'
⊢ ∀ (h : Stream'.corec' (Corec.f f) o (n + 1) = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd (n + 1) = some a'

Tactic:
rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]

Premises used: Stream'.corec'_eq, Prod.snd, Computation.Corec.f
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH :
  ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ ∀ (h : Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a'),
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'

Tactic:
IH (Corec.f f o).2

Premises used: Stream'.corec', Stream'.get, Stream'.map, Stream'.corec, Stream'.cons, Prod.snd, Computation.Corec.f
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH :
  ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ ∀ (h : Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a'),
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'

Tactic:
exact IH (Corec.f f o).2

Premises used: Prod.snd, Computation.Corec.f
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
o : α ⊕ β
zero :
  ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o 0 = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd 0 = some a'
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o n = some a'),
        Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a')
    (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o (n + 1) = some a'),
    Stream'.corec' (Corec.f f) (Corec.f f o).snd (n + 1) = some a'
⊢ ∀ (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'

Tactic:
induction n generalizing o with
  | zero =>
    change (Corec.f f o).1 = some a' → (Corec.f f (Corec.f f o).2).1 = some a'
    rcases o with _ | b <;> intro h
    · exact h
    unfold Corec.f at *; split <;> simp_all
  | succ n IH =>
    rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
    exact IH (Corec.f f o).2

Premises used: Stream'.corec'_eq, Prod.snd, Computation.Corec.f
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
dsimp :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) f b with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
      α ⊕ Computation α)
⊢ (corec f b).destruct = rmap (corec f) (f b)

Tactic:
dsimp [corec, destruct]

Premises used: Computation.corec, Computation.destruct
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
dsimp :
  Eq (α := Option α)
    (match (motive := α ⊕ β → Option α) f b with
      | Sum.inl a => some a
      | Sum.inr val => none :
      Option α)
    (Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b) : Option α)
⊢ Stream'.corec' (Corec.f f) (Sum.inr b) 0 =
    Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b)

Tactic:
dsimp [Corec.f, Stream'.corec', Stream'.corec, Stream'.map, Stream'.get, Stream'.iterate]

Premises used: Stream'.corec', Stream'.iterate, Stream'.get, Stream'.map, Stream'.corec, Computation.Corec.f
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
x : α
⊢ Eq (α := Option α)
    (match (motive := α ⊕ β → Option α) Sum.inl x with
      | Sum.inl a => some a
      | Sum.inr val => none :
      Option α)
    (Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (Sum.inl x) : Option α)

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b x : β
⊢ Eq.{u + 1} (α := Option α)
    (match (motive := α ⊕ β → Option α) Sum.inr x with
      | Sum.inl a => some a
      | Sum.inr val => none :
      Option α)
    (Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (Sum.inr x) : Option α)

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ Eq (α := Option α)
    (match (motive := α ⊕ β → Option α) f b with
      | Sum.inl a => some a
      | Sum.inr val => none :
      Option α)
    (Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b) : Option α)

Tactic:
match (f b) with
    | Sum.inl x => rfl
    | Sum.inr x => rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
rw :
  Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b) with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) f b with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
      α ⊕ Computation α)
⊢ Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) f b with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
      α ⊕ Computation α)

Tactic:
rw [show Stream'.corec' (Corec.f f) (Sum.inr b) 0 =
    Sum.rec Option.some (fun _ ↦ none) (f b) by
    dsimp [Corec.f, Stream'.corec', Stream'.corec, Stream'.map, Stream'.get, Stream'.iterate]
    match (f b) with
    | Sum.inl x => rfl
    | Sum.inr x => rfl]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
inl :
  ∀ (a : α) (h : f b = Sum.inl a),
    Eq.{u + 1} (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α)
          Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (Sum.inl a) with
        | none =>
          Sum.inr
            (tail
              (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
                (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (match (motive := α ⊕ β → α ⊕ Computation α) Sum.inl a with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
        α ⊕ Computation α)
inr :
  ∀ (b' : β) (h : f b = Sum.inr b'),
    Eq.{u + 1} (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α)
          Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (Sum.inr b') with
        | none =>
          Sum.inr
            (tail
              (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
                (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (match (motive := α ⊕ β → α ⊕ Computation α) Sum.inr b' with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
        α ⊕ Computation α)
⊢ Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b) with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) f b with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
      α ⊕ Computation α)

Tactic:
rcases h : f b with a | b'
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
a : α
h : f b = Sum.inl a
⊢ Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (Sum.inl a) with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) Sum.inl a with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
      α ⊕ Computation α)

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
inr :
  tail
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Stream'.corec' (Corec.f f) (Sum.inr b')) ⋯
⊢ Eq (α := α ⊕ Computation α)
    (Sum.inr
      (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯)))
    (Sum.inr
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Stream'.corec' (Corec.f f) (Sum.inr b')) ⋯))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
inr :
  (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯)).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)
        (Stream'.corec' (Corec.f f) (Sum.inr b')) ⋯)
⊢ tail
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) =
    Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Stream'.corec' (Corec.f f) (Sum.inr b')) ⋯

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
inr : Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd = Stream'.corec' (Corec.f f) (Sum.inr b')
⊢ (Stream'.corec' (Corec.f f) (Sum.inr b)).tail = Stream'.corec' (Corec.f f) (Sum.inr b')

Tactic:
rw [Stream'.corec'_eq, Stream'.tail_cons]

Premises used: Stream'.corec'_eq, Stream'.tail_cons
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
inr : Stream'.corec' (Corec.f f) (f b) = Stream'.corec' (Corec.f f) (Sum.inr b')
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd = Stream'.corec' (Corec.f f) (Sum.inr b')

Tactic:
dsimp [Corec.f]

Premises used: Computation.Corec.f
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
inr inr₁ : Stream'.corec' (Corec.f f) (Sum.inr b') = Stream'.corec' (Corec.f f) (Sum.inr b')
⊢ Stream'.corec' (Corec.f f) (f b) = Stream'.corec' (Corec.f f) (Sum.inr b')

Tactic:
rw [h]
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
a :
  s₁.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) =
    s₂.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
⊢ s₁ = s₂

Tactic:
apply Subtype.ext

Premises used: Subtype.ext