[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : autoParam (F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom) _auto✝
⊢ F.map h.inv ≫ A₀.str = A₁.str ≫ h.inv
[PROOFSTEP]
rw [h.eq_comp_inv, Category.assoc, ← w, ← Functor.map_comp_assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : autoParam (F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom) _auto✝
⊢ F.map (h.inv ≫ h.hom) ≫ A₁.str = A₁.str
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f✝ : A₀ ⟶ A₁
g : A₁ ⟶ A₂
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ F.map (inv f.f) ≫ A₀.str = A₁.str ≫ inv f.f
[PROOFSTEP]
rw [IsIso.eq_comp_inv f.1, Category.assoc, ← f.h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f✝ : A₀ ⟶ A₁
g : A₁ ⟶ A₂
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ F.map (inv f.f) ≫ F.map f.f ≫ A₁.str = A₁.str
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f✝ : A₀ ⟶ A₁
g : A₁ ⟶ A₂
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ f ≫ Hom.mk (inv f.f) = 𝟙 A₀
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f✝ : A₀ ⟶ A₁
g : A₁ ⟶ A₂
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ Hom.mk (inv f.f) ≫ f = 𝟙 A₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
A A₀ A₁ A₂ : Algebra F✝
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
F G : C ⥤ C
α : F ≅ G
⊢ 𝟙 F = α.hom ≫ α.inv
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
A A₀ A₁ A₂ : Algebra F✝
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
F G : C ⥤ C
α : F ≅ G
⊢ α.inv ≫ α.hom = 𝟙 G
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str
[PROOFSTEP]
rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)
[PROOFSTEP]
rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ F.map ((Limits.IsInitial.to h { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ (Limits.IsInitial.to h { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a
[PROOFSTEP]
exact left_inv h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : autoParam (V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str) _auto✝
⊢ V₁.str ≫ F.map h.inv = h.inv ≫ V₀.str
[PROOFSTEP]
rw [h.eq_inv_comp, ← Category.assoc, ← w, Category.assoc, ← F.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : autoParam (V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str) _auto✝
⊢ V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str
[PROOFSTEP]
simp only [Iso.hom_inv_id, Functor.map_id, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₁.str ≫ F.map (inv f.f) = inv f.f ≫ V₀.str
[PROOFSTEP]
rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ f ≫ Hom.mk (inv f.f) = 𝟙 V₀
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ Hom.mk (inv f.f) ≫ f = 𝟙 V₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ⟶ G
X✝ Y✝ : Coalgebra F
f : X✝ ⟶ Y✝
⊢ ((fun V => { V := V.V, str := V.str ≫ NatTrans.app α V.V }) X✝).str ≫ G.map f.f =
    f.f ≫ ((fun V => { V := V.V, str := V.str ≫ NatTrans.app α V.V }) Y✝).str
[PROOFSTEP]
rw [Category.assoc, ← α.naturality, ← Category.assoc, f.h, Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ≅ G
⊢ 𝟙 F = α.hom ≫ α.inv
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ≅ G
⊢ α.inv ≫ α.hom = 𝟙 G
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ ↑(Adjunction.homEquiv adj A₁.a A₁.a) A₁.str ≫ G.map f.f = f.f ≫ ↑(Adjunction.homEquiv adj A₂.a A₂.a) A₂.str
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ F.map f.f ≫ ↑(Adjunction.homEquiv adj V₂.V V₂.V).symm V₂.str = ↑(Adjunction.homEquiv adj V₁.V V₁.V).symm V₁.str ≫ f.f
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm, f.h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ F.map (𝟙 A.a) ≫ ((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).obj A).str =
    ((𝟭 (Algebra F)).obj A).str ≫ 𝟙 A.a
[PROOFSTEP]
erw [F.map_id, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ ((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).obj A).str = ((𝟭 (Algebra F)).obj A).str
[PROOFSTEP]
apply (adj.homEquiv _ _).left_inv A.str
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ F.map (𝟙 A.a) ≫ ((𝟭 (Algebra F)).obj A).str =
    ((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).obj A).str ≫ 𝟙 A.a
[PROOFSTEP]
erw [F.map_id, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ ((𝟭 (Algebra F)).obj A).str = ((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).obj A).str
[PROOFSTEP]
apply ((adj.homEquiv _ _).left_inv A.str).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ (Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).map f ≫ (fun A => Algebra.Hom.mk (𝟙 A.a)) A₂ =
    (fun A => Algebra.Hom.mk (𝟙 A.a)) A₁ ≫ (𝟭 (Algebra F)).map f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ autoParam
    (((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).map f ≫ (fun A => Algebra.Hom.mk (𝟙 A.a)) A₂).f =
      ((fun A => Algebra.Hom.mk (𝟙 A.a)) A₁ ≫ (𝟭 (Algebra F)).map f).f)
    _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ autoParam (((Coalgebra.toAlgebraOf adj).map ((Algebra.toCoalgebraOf adj).map f)).f ≫ 𝟙 A₂.a = 𝟙 A₁.a ≫ f.f) _auto✝
[PROOFSTEP]
erw [Category.comp_id, Category.id_comp]
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ autoParam (((Coalgebra.toAlgebraOf adj).map ((Algebra.toCoalgebraOf adj).map f)).f = f.f) _auto✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ ((Coalgebra.toAlgebraOf adj ⋙ Algebra.toCoalgebraOf adj).obj V).str ≫ G.map (𝟙 V.V) =
    𝟙 V.V ≫ ((𝟭 (Coalgebra G)).obj V).str
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ ((Algebra.toCoalgebraOf adj).obj ((Coalgebra.toAlgebraOf adj).obj V)).str ≫ G.map (𝟙 V.V) = 𝟙 V.V ≫ V.str
[PROOFSTEP]
erw [G.map_id, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ ((Algebra.toCoalgebraOf adj).obj ((Coalgebra.toAlgebraOf adj).obj V)).str = V.str
[PROOFSTEP]
apply (adj.homEquiv _ _).right_inv V.str
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ (Coalgebra.toAlgebraOf adj ⋙ Algebra.toCoalgebraOf adj).map f ≫ (fun V => Coalgebra.Hom.mk (𝟙 V.V)) V₂ =
    (fun V => Coalgebra.Hom.mk (𝟙 V.V)) V₁ ≫ (𝟭 (Coalgebra G)).map f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ autoParam
    (((Coalgebra.toAlgebraOf adj ⋙ Algebra.toCoalgebraOf adj).map f ≫ (fun V => Coalgebra.Hom.mk (𝟙 V.V)) V₂).f =
      ((fun V => Coalgebra.Hom.mk (𝟙 V.V)) V₁ ≫ (𝟭 (Coalgebra G)).map f).f)
    _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ autoParam (((Algebra.toCoalgebraOf adj).map ((Coalgebra.toAlgebraOf adj).map f)).f ≫ 𝟙 V₂.V = 𝟙 V₁.V ≫ f.f) _auto✝
[PROOFSTEP]
erw [Category.comp_id, Category.id_comp]
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ autoParam (((Algebra.toCoalgebraOf adj).map ((Coalgebra.toAlgebraOf adj).map f)).f = f.f) _auto✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ ((𝟭 (Coalgebra G)).obj V).str ≫ G.map (𝟙 V.V) =
    𝟙 V.V ≫ ((Coalgebra.toAlgebraOf adj ⋙ Algebra.toCoalgebraOf adj).obj V).str
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ V.str ≫ G.map (𝟙 V.V) = 𝟙 V.V ≫ ((Algebra.toCoalgebraOf adj).obj ((Coalgebra.toAlgebraOf adj).obj V)).str
[PROOFSTEP]
rw [G.map_id, Category.comp_id, Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ V.str = ((Algebra.toCoalgebraOf adj).obj ((Coalgebra.toAlgebraOf adj).obj V)).str
[PROOFSTEP]
apply ((adj.homEquiv _ _).right_inv V.str).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ (Algebra.toCoalgebraOf adj).map (NatTrans.app (AlgCoalgEquiv.unitIso adj).hom A) ≫
      NatTrans.app (AlgCoalgEquiv.counitIso adj).hom ((Algebra.toCoalgebraOf adj).obj A) =
    𝟙 ((Algebra.toCoalgebraOf adj).obj A)
[PROOFSTEP]
ext
  -- Porting note: why doesn't `simp` work here?
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ autoParam
    (((Algebra.toCoalgebraOf adj).map (NatTrans.app (AlgCoalgEquiv.unitIso adj).hom A) ≫
          NatTrans.app (AlgCoalgEquiv.counitIso adj).hom ((Algebra.toCoalgebraOf adj).obj A)).f =
      (𝟙 ((Algebra.toCoalgebraOf adj).obj A)).f)
    _auto✝
[PROOFSTEP]
exact Category.comp_id _
