goal2.lean

 Freeze display
Tactic State
4 goals
α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_functor : α ⥤ β,
e_inverse : β ⥤ α,
e_unit_iso : 𝟭 α ≅ e_functor ⋙ e_inverse,
e_counit_iso : e_inverse ⋙ e_functor ≅ 𝟭 β,
e_functor_unit_iso_comp' :
  auto_param
    (∀ (X : α),
       e_functor.map (e_unit_iso.hom.app X) ≫ e_counit_iso.hom.app (e_functor.obj X) = 𝟙 (e_functor.obj X))
    (name.mk_string "obviously" name.anonymous)
⊢ 𝟭 α ⋙ e_functor = e_functor

α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_functor : α ⥤ β,
e_inverse : β ⥤ α,
e_unit_iso : 𝟭 α ≅ e_functor ⋙ e_inverse,
e_counit_iso : e_inverse ⋙ e_functor ≅ 𝟭 β,
e_functor_unit_iso_comp' :
  auto_param
    (∀ (X : α),
       e_functor.map (e_unit_iso.hom.app X) ≫ e_counit_iso.hom.app (e_functor.obj X) = 𝟙 (e_functor.obj X))
    (name.mk_string "obviously" name.anonymous)
⊢ {functor := e_functor,
       inverse := e_inverse,
       unit_iso := e_unit_iso,
       counit_iso := e_counit_iso,
       functor_unit_iso_comp' := e_functor_unit_iso_comp'}.inverse ⋙
      equivalence.refl.inverse =
    e_inverse

α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_functor : α ⥤ β,
e_inverse : β ⥤ α,
e_unit_iso : 𝟭 α ≅ e_functor ⋙ e_inverse,
e_counit_iso : e_inverse ⋙ e_functor ≅ 𝟭 β,
e_functor_unit_iso_comp' :
  auto_param
    (∀ (X : α),
       e_functor.map (e_unit_iso.hom.app X) ≫ e_counit_iso.hom.app (e_functor.obj X) = 𝟙 (e_functor.obj X))
    (name.mk_string "obviously" name.anonymous)
⊢ equivalence.adjointify_η
      (equivalence.refl.unit_iso ≪≫
         iso_whisker_left equivalence.refl.functor
           (iso_whisker_right
              {functor := e_functor,
               inverse := e_inverse,
               unit_iso := e_unit_iso,
               counit_iso := e_counit_iso,
               functor_unit_iso_comp' := e_functor_unit_iso_comp'}.unit_iso
              equivalence.refl.inverse))
      (iso_whisker_left
           {functor := e_functor,
            inverse := e_inverse,
            unit_iso := e_unit_iso,
            counit_iso := e_counit_iso,
            functor_unit_iso_comp' := e_functor_unit_iso_comp'}.inverse
           (iso_whisker_right equivalence.refl.counit_iso
              {functor := e_functor,
               inverse := e_inverse,
               unit_iso := e_unit_iso,
               counit_iso := e_counit_iso,
               functor_unit_iso_comp' := e_functor_unit_iso_comp'}.functor) ≪≫
         {functor := e_functor,
          inverse := e_inverse,
          unit_iso := e_unit_iso,
          counit_iso := e_counit_iso,
          functor_unit_iso_comp' := e_functor_unit_iso_comp'}.counit_iso) =
    e_unit_iso

α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_functor : α ⥤ β,
e_inverse : β ⥤ α,
e_unit_iso : 𝟭 α ≅ e_functor ⋙ e_inverse,
e_counit_iso : e_inverse ⋙ e_functor ≅ 𝟭 β,
e_functor_unit_iso_comp' :
  auto_param
    (∀ (X : α),
       e_functor.map (e_unit_iso.hom.app X) ≫ e_counit_iso.hom.app (e_functor.obj X) = 𝟙 (e_functor.obj X))
    (name.mk_string "obviously" name.anonymous)
⊢ iso_whisker_left
        {functor := e_functor,
         inverse := e_inverse,
         unit_iso := e_unit_iso,
         counit_iso := e_counit_iso,
         functor_unit_iso_comp' := e_functor_unit_iso_comp'}.inverse
        (iso_whisker_right equivalence.refl.counit_iso
           {functor := e_functor,
            inverse := e_inverse,
            unit_iso := e_unit_iso,
            counit_iso := e_counit_iso,
            functor_unit_iso_comp' := e_functor_unit_iso_comp'}.functor) ≪≫
      {functor := e_functor,
       inverse := e_inverse,
       unit_iso := e_unit_iso,
       counit_iso := e_counit_iso,
       functor_unit_iso_comp' := e_functor_unit_iso_comp'}.counit_iso =
    e_counit_iso