α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ Option.map
      (fun a' =>
        (a',
          tail
            { val := corec' (Corec.f f) (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) =>
      some
        (a,
          { val := corec' (Corec.f f) (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ destruct (corec f b) = omap (corec f) (f b)
dsimp [corec, destruct, nth]
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ Option.map
      (fun a' =>
        (a',
          tail
            { val := corec' (Corec.f f) (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) =>
      some
        (a,
          { val := corec' (Corec.f f) (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ Option.map
      (fun a' =>
        (a',
          tail
            { val := corec' (Corec.f f) (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) =>
      some
        (a,
          { val := corec' (Corec.f f) (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
dsimp
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map
      (fun a' =>
        (a',
          tail
            { val := corec' (Corec.f f) (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) =>
      some
        (a,
          { val := corec' (Corec.f f) (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ Option.map
      (fun a' =>
        (a',
          tail
            { val := corec' (Corec.f f) (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) =>
      some
        (a,
          { val := corec' (Corec.f f) (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
have h: Stream'.corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1 := rfl
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map
      (fun a' =>
        (a',
          tail
            { val := corec' (Corec.f f) (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (Corec.f f (some b)).fst =
    match f b with
    | none => none
    | some (a, b) =>
      some
        (a,
          { val := corec' (Corec.f f) (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map
      (fun a' =>
        (a',
          tail
            { val := corec' (Corec.f f) (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (corec' (Corec.f f) (some b) 0) =
    match f b with
    | none => none
    | some (a, b) =>
      some
        (a,
          { val := corec' (Corec.f f) (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
rw [h]
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map
      (fun a' =>
        (a',
          tail
            {
              val :=
                corec'
                  (fun x =>
                    match x with
                    | none => (none, none)
                    | some b =>
                      match f b with
                      | none => (none, none)
                      | some (a, b') => (some a, some b'))
                  (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (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,
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map
      (fun a' =>
        (a',
          tail
            { val := corec' (Corec.f f) (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (Corec.f f (some b)).fst =
    match f b with
    | none => none
    | some (a, b) =>
      some
        (a,
          { val := corec' (Corec.f f) (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
dsimp [Corec.f]
case none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
h : f b = none
⊢ Option.map
      (fun a' =>
        (a',
          tail
            {
              val :=
                corec'
                  (fun x =>
                    match x with
                    | none => (none, none)
                    | some b =>
                      match f b with
                      | none => (none, none)
                      | some (a, b') => (some a, some b'))
                  (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match none with
    | none => none
    | some (a, b) =>
      some
        (a,
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })

case some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
s : α × β
h : f b = some s
⊢ Option.map
      (fun a' =>
        (a',
          tail
            {
              val :=
                corec'
                  (fun x =>
                    match x with
                    | none => (none, none)
                    | some b =>
                      match f b with
                      | none => (none, none)
                      | some (a, b') => (some a, some b'))
                  (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (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,
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
⊢ Option.map
      (fun a' =>
        (a',
          tail
            {
              val :=
                corec'
                  (fun x =>
                    match x with
                    | none => (none, none)
                    | some b =>
                      match f b with
                      | none => (none, none)
                      | some (a, b') => (some a, some b'))
                  (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (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,
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
induction' h : f b with s
case some.mk
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ Option.map
      (fun a' =>
        (a',
          tail
            {
              val :=
                corec'
                  (fun x =>
                    match x with
                    | none => (none, none)
                    | some b =>
                      match f b with
                      | none => (none, none)
                      | some (a, b') => (some a, some b'))
                  (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (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,
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
case some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
s : α × β
h : f b = some s
⊢ Option.map
      (fun a' =>
        (a',
          tail
            {
              val :=
                corec'
                  (fun x =>
                    match x with
                    | none => (none, none)
                    | some b =>
                      match f b with
                      | none => (none, none)
                      | some (a, b') => (some a, some b'))
                  (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (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,
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
cases' s with a b'
case some.mk
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ some
      (a,
        tail
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }) =
    some
      (a,
        {
          val :=
            corec'
              (fun x =>
                match x with
                | none => (none, none)
                | some b =>
                  match f b with
                  | none => (none, none)
                  | some (a, b') => (some a, some b'))
              (some b'),
          property :=
            (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b') n = none → corec' (Corec.f f) (some b') (n + 1) = none) })
case some.mk
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ Option.map
      (fun a' =>
        (a',
          tail
            {
              val :=
                corec'
                  (fun x =>
                    match x with
                    | none => (none, none)
                    | some b =>
                      match f b with
                      | none => (none, none)
                      | some (a, b') => (some a, some b'))
                  (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (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,
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
dsimp [Corec.f]
case some.mk
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ tail
      {
        val :=
          corec'
            (fun x =>
              match x with
              | none => (none, none)
              | some b =>
                match f b with
                | none => (none, none)
                | some (a, b') => (some a, some b'))
            (some b),
        property :=
          (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) } =
    {
      val :=
        corec'
          (fun x =>
            match x with
            | none => (none, none)
            | some b =>
              match f b with
              | none => (none, none)
              | some (a, b') => (some a, some b'))
          (some b'),
      property := (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b') n = none → corec' (Corec.f f) (some b') (n + 1) = none) }
case some.mk
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ some
      (a,
        tail
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }) =
    some
      (a,
        {
          val :=
            corec'
              (fun x =>
                match x with
                | none => (none, none)
                | some b =>
                  match f b with
                  | none => (none, none)
                  | some (a, b') => (some a, some b'))
              (some b'),
          property :=
            (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b') n = none → corec' (Corec.f f) (some b') (n + 1) = none) })
apply congr_arg fun b' => some (a, b')
case some.mk.a
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ ↑(tail
        {
          val :=
            corec'
              (fun x =>
                match x with
                | none => (none, none)
                | some b =>
                  match f b with
                  | none => (none, none)
                  | some (a, b') => (some a, some b'))
              (some b),
          property :=
            (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }) =
    ↑{
        val :=
          corec'
            (fun x =>
              match x with
              | none => (none, none)
              | some b =>
                match f b with
                | none => (none, none)
                | some (a, b') => (some a, some b'))
            (some b'),
        property :=
          (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b') n = none → corec' (Corec.f f) (some b') (n + 1) = none) }
case some.mk
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ tail
      {
        val :=
          corec'
            (fun x =>
              match x with
              | none => (none, none)
              | some b =>
                match f b with
                | none => (none, none)
                | some (a, b') => (some a, some b'))
            (some b),
        property :=
          (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) } =
    {
      val :=
        corec'
          (fun x =>
            match x with
            | none => (none, none)
            | some b =>
              match f b with
              | none => (none, none)
              | some (a, b') => (some a, some b'))
          (some b'),
      property := (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b') n = none → corec' (Corec.f f) (some b') (n + 1) = none) }
apply Subtype.eq
case some.mk.a
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ Stream'.tail
      (corec'
        (fun x =>
          match x with
          | none => (none, none)
          | some b =>
            match f b with
            | none => (none, none)
            | some (a, b') => (some a, some b'))
        (some b)) =
    corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (some b')
case some.mk.a
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ ↑(tail
        {
          val :=
            corec'
              (fun x =>
                match x with
                | none => (none, none)
                | some b =>
                  match f b with
                  | none => (none, none)
                  | some (a, b') => (some a, some b'))
              (some b),
          property :=
            (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }) =
    ↑{
        val :=
          corec'
            (fun x =>
              match x with
              | none => (none, none)
              | some b =>
                match f b with
                | none => (none, none)
                | some (a, b') => (some a, some b'))
            (some b'),
        property :=
          (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b') n = none → corec' (Corec.f f) (some b') (n + 1) = none) }
dsimp [corec, tail]
case some.mk.a
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (match some b with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd =
    corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (some b')
case some.mk.a
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ Stream'.tail
      (corec'
        (fun x =>
          match x with
          | none => (none, none)
          | some b =>
            match f b with
            | none => (none, none)
            | some (a, b') => (some a, some b'))
        (some b)) =
    corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (some b')
rw [Stream'.corec'_eq, Stream'.tail_cons]
case some.mk.a
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).snd =
    corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (some b')
case some.mk.a
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (match some b with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd =
    corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (some b')
dsimp [Corec.f]
no goals
case some.mk.a
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
a : α
b' : β
h : f b = some (a, b')
⊢ corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).snd =
    corec'
      (fun x =>
        match x with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b'))
      (some b')
rw [h]
no goals
case none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h✝¹ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).fst
x✝ : Option (α × β)
h✝ : f b = x✝
h : f b = none
⊢ Option.map
      (fun a' =>
        (a',
          tail
            {
              val :=
                corec'
                  (fun x =>
                    match x with
                    | none => (none, none)
                    | some b =>
                      match f b with
                      | none => (none, none)
                      | some (a, b') => (some a, some b'))
                  (some b),
              property :=
                (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) }))
      (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match none with
    | none => none
    | some (a, b) =>
      some
        (a,
          {
            val :=
              corec'
                (fun x =>
                  match x with
                  | none => (none, none)
                  | some b =>
                    match f b with
                    | none => (none, none)
                    | some (a, b') => (some a, some b'))
                (some b),
            property :=
              (_ : ∀ {n : ℕ}, corec' (Corec.f f) (some b) n = none → corec' (Corec.f f) (some b) (n + 1) = none) })
rfl