-- Mathlib/Data/Seq/Computation.lean
theorem corec_eq (f : β → α ⊕ β) (b : β) : destruct (corec f b) = rmap (corec f) (f b)

Proof state:
case inr.h.a
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ ↑(tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩) = ↑⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩

Tactic:
dsimp [corec, tail]

Result:
case inr.h.a
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (Stream'.corec' (Corec.f f) (Sum.inr b)).tail = Stream'.corec' (Corec.f f) (Sum.inr b')

Proof state:
case inr.h
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩ = ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩

Tactic:
apply Subtype.eq

Result:
case inr.h.a
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ ↑(tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩) = ↑⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩

Proof state:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match f b with
    | Sum.inl a => some a
    | Sum.inr val => none) =
    Sum.rec some (fun x => none) (f b)

Tactic:
match (f b) with
| Sum.inl x => rfl
| Sum.inr x => rfl

Result:
no goals

Proof state:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (match Sum.rec some (fun x => none) (Sum.inr b') with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inr b' with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Tactic:
dsimp [Corec.f, destruct]

Result:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩) = Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩

Proof state:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

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
  ]

Result:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match Sum.rec some (fun x => none) (f b) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Proof state:
case inr.h.a
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (f b) = Stream'.corec' (Corec.f f) (Sum.inr b')

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → α ⊕ β
b x : β
⊢ (match Sum.inr x with
    | Sum.inl a => some a
    | Sum.inr val => none) =
    Sum.rec some (fun x => none) (Sum.inr x)

Tactic:
rfl

Result:
no goals

Proof state:
case inr.h.a
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = 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]

Result:
case inr.h.a
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd = Stream'.corec' (Corec.f f) (Sum.inr b')

Proof state:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ Stream'.corec' (Corec.f f) (Sum.inr b) 0 = Sum.rec some (fun x => none) (f b)

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

Result:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match f b with
    | Sum.inl a => some a
    | Sum.inr val => none) =
    Sum.rec some (fun x => none) (f b)

Proof state:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩) = Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩

Tactic:
apply congr_arg

Result:
case inr.h
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩ = ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩

Proof state:
case inr.h.a
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = 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]

Result:
case inr.h.a
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (f b) = Stream'.corec' (Corec.f f) (Sum.inr b')

Proof state:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (corec f b).destruct = rmap (corec f) (f b)

Tactic:
dsimp [corec, destruct]

Result:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Proof state:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
x : α
⊢ (match Sum.inl x with
    | Sum.inl a => some a
    | Sum.inr val => none) =
    Sum.rec some (fun x => none) (Sum.inl x)

Tactic:
rfl

Result:
no goals

Proof state:
case inl
α : Type u
β : Type v
f : β → α ⊕ β
b : β
a : α
h : f b = Sum.inl a
⊢ (match Sum.rec some (fun x => none) (Sum.inl a) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inl a with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match Sum.rec some (fun x => none) (f b) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Tactic:
induction' h : f b with a b'

Result:
case inl
α : Type u
β : Type v
f : β → α ⊕ β
b : β
a : α
h : f b = Sum.inl a
⊢ (match Sum.rec some (fun x => none) (Sum.inl a) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inl a with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (match Sum.rec some (fun x => none) (Sum.inr b') with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inr b' with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩