-- Mathlib/Data/Seq/Seq.lean
theorem corec_eq (f : β → Option (α × β)) (b : β) :
    destruct (corec f b) = omap (corec f) (f b)

Proof state:
case some.mk
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ some (a, tail ⟨corec' (Corec.f f) (some b), ⋯⟩) = some (a, ⟨corec' (Corec.f f) (some b'), ⋯⟩)

Tactic:
apply congr_arg fun b' => some (a, b')

Result:
case some.mk
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ tail ⟨corec' (Corec.f f) (some b), ⋯⟩ = ⟨corec' (Corec.f f) (some b'), ⋯⟩

Proof state:
case some.mk
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match some (a, b') with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match some (a, b') with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
dsimp [Corec.f]

Result:
case some.mk
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ some (a, tail ⟨corec' (Corec.f f) (some b), ⋯⟩) = some (a, ⟨corec' (Corec.f f) (some b'), ⋯⟩)

Proof state:
case some.mk
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ tail ⟨corec' (Corec.f f) (some b), ⋯⟩ = ⟨corec' (Corec.f f) (some b'), ⋯⟩

Tactic:
apply Subtype.eq

Result:
case some.mk.a
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ ↑(tail ⟨corec' (Corec.f f) (some b), ⋯⟩) = ↑⟨corec' (Corec.f f) (some b'), ⋯⟩

Proof state:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
induction' h : f b with s

Result:
case none
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
h : f b = none
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match none with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
s : α × β
h : f b = some s
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match some s with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match some s with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Proof state:
case some.mk.a
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ corec' (Corec.f f) (Corec.f f (some b)).snd = corec' (Corec.f f) (some b')

Tactic:
dsimp [Corec.f]

Result:
case some.mk.a
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ corec' (Corec.f f)
      (match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).snd =
    corec' (Corec.f f) (some b')

Proof state:
case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
s : α × β
h : f b = some s
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match some s with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match some s with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
obtain ⟨a, b'⟩ := s

Result:
case some.mk
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match some (a, b') with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match some (a, b') with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Proof state:
case some.mk.a
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ corec' (Corec.f f)
      (match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).snd =
    corec' (Corec.f f) (some b')

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩)) (Corec.f f (some b)).fst =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
dsimp [Corec.f]

Result:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Proof state:
case none
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
h : f b = none
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match none with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩)) (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
have h : Stream'.corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1 := rfl

Result:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map (fun a' => (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩)) (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Proof state:
case some.mk.a
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ (corec' (Corec.f f) (some b)).tail = corec' (Corec.f f) (some b')

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

Result:
case some.mk.a
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
a : α
b' : β
h : f b = some (a, b')
⊢ corec' (Corec.f f) (Corec.f f (some b)).snd = corec' (Corec.f f) (some b')