F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : α → F α
x : α
⊢ Quot.lift (fun x => Quot.mk Mcongr <$> abs (PFunctor.M.dest x))
      (_ :
        ∀ (x y : PFunctor.M (P F)),
          Mcongr x y →
            (fun x => Quot.mk Mcongr <$> abs (PFunctor.M.dest x)) x =
              (fun x => Quot.mk Mcongr <$> abs (PFunctor.M.dest x)) y)
      (Quot.mk Mcongr (corecF g x)) =
    corec g <$> g x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : α → F α
x : α
⊢ dest (corec g x) = corec g <$> g x
conv =>
  lhs
  rw [Cofix.dest, Cofix.corec];
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> abs (PFunctor.M.dest (corecF g x)) = corec g <$> g x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : α → F α
x : α
⊢ Quot.lift (fun x => Quot.mk Mcongr <$> abs (PFunctor.M.dest x))
      (_ :
        ∀ (x y : PFunctor.M (P F)),
          Mcongr x y →
            (fun x => Quot.mk Mcongr <$> abs (PFunctor.M.dest x)) x =
              (fun x => Quot.mk Mcongr <$> abs (PFunctor.M.dest x)) y)
      (Quot.mk Mcongr (corecF g x)) =
    corec g <$> g x
dsimp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : α → F α
x : α
⊢ (Quot.mk Mcongr ∘ corecF g) <$> g x = corec g <$> g x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> abs (PFunctor.M.dest (corecF g x)) = corec g <$> g x
rw [corecF_eq, abs_map, abs_repr, ← comp_map]
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : α → F α
x : α
⊢ (Quot.mk Mcongr ∘ corecF g) <$> g x = corec g <$> g x
rfl