Theorem: Container.M.destruct_corec (CoInd/M.lean)

State before:
C : Container
α : Type u₃
f : α → Obj C α
x₀ : α
⊢ destruct (corec f x₀) = Map (corec f) (f x₀)
Tactic:
simp only [corec, destruct]
State after:
C : Container
α : Type u₃
f : α → Obj C α
x₀ : α
⊢ {
      fst :=
        node
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) },
      snd :=
        children
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) } } =
    Map
      (fun x₀ =>
        { approx := Approx.corec f x₀,
          agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) })
      (f x₀)

State before:
C : Container
α : Type u₃
f : α → Obj C α
x₀ : α
⊢ {
      fst :=
        node
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) },
      snd :=
        children
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) } } =
    Map
      (fun x₀ =>
        { approx := Approx.corec f x₀,
          agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) })
      (f x₀)
Tactic:
rfl
State after:
no goals