goal.lean

 Freeze display
Tactic State
1 goal
α : Type u₁,
β : Type u₂,
_inst_1 : category α,
_inst_2 : category β,
e_inverse_obj : β → α,
e_inverse_map : Π {X Y : β}, (X ⟶ Y) → (e_inverse_obj X ⟶ e_inverse_obj Y),
e_inverse_map_id' :
  auto_param (∀ (X : β), e_inverse_map (𝟙 X) = 𝟙 (e_inverse_obj X))
    (name.mk_string "obviously" name.anonymous),
e_inverse_map_comp' :
  auto_param
    (∀ {X Y Z : β} (f : X ⟶ Y) (g : Y ⟶ Z), e_inverse_map (f ≫ g) = e_inverse_map f ≫ e_inverse_map g)
    (name.mk_string "obviously" name.anonymous),
e_functor_obj : α → β,
e_functor_map : Π {X Y : α}, (X ⟶ Y) → (e_functor_obj X ⟶ e_functor_obj Y),
e_functor_map_id' :
  auto_param (∀ (X : α), e_functor_map (𝟙 X) = 𝟙 (e_functor_obj X))
    (name.mk_string "obviously" name.anonymous),
e_functor_map_comp' :
  auto_param
    (∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z), e_functor_map (f ≫ g) = e_functor_map f ≫ e_functor_map g)
    (name.mk_string "obviously" name.anonymous),
e_counit_iso_hom :
  {obj := e_inverse_obj, map := e_inverse_map, map_id' := e_inverse_map_id', map_comp' := e_inverse_map_comp'} ⋙
      {obj := e_functor_obj, map := e_functor_map, map_id' := e_functor_map_id', map_comp' := e_functor_map_comp'} ⟶
    𝟭 β,
e_counit_iso_inv :
  𝟭 β ⟶
    {obj := e_inverse_obj, map := e_inverse_map, map_id' := e_inverse_map_id', map_comp' := e_inverse_map_comp'} ⋙
      {obj := e_functor_obj, map := e_functor_map, map_id' := e_functor_map_id', map_comp' := e_functor_map_comp'},
e_counit_iso_hom_inv_id' :
  auto_param
    (e_counit_iso_hom ≫ e_counit_iso_inv =
       𝟙
         ({obj := e_inverse_obj,
             map := e_inverse_map,
             map_id' := e_inverse_map_id',
             map_comp' := e_inverse_map_comp'} ⋙
            {obj := e_functor_obj,
             map := e_functor_map,
             map_id' := e_functor_map_id',
             map_comp' := e_functor_map_comp'}))
    (name.mk_string "obviously" name.anonymous),
e_counit_iso_inv_hom_id' :
  auto_param (e_counit_iso_inv ≫ e_counit_iso_hom = 𝟙 (𝟭 β)) (name.mk_string "obviously" name.anonymous),
e_unit_iso_hom :
  𝟭 α ⟶
    {obj := e_functor_obj, map := e_functor_map, map_id' := e_functor_map_id', map_comp' := e_functor_map_comp'} ⋙
      {obj := e_inverse_obj, map := e_inverse_map, map_id' := e_inverse_map_id', map_comp' := e_inverse_map_comp'},
e_unit_iso_inv :
  {obj := e_functor_obj, map := e_functor_map, map_id' := e_functor_map_id', map_comp' := e_functor_map_comp'} ⋙
      {obj := e_inverse_obj, map := e_inverse_map, map_id' := e_inverse_map_id', map_comp' := e_inverse_map_comp'} ⟶
    𝟭 α,
e_unit_iso_hom_inv_id' :
  auto_param (e_unit_iso_hom ≫ e_unit_iso_inv = 𝟙 (𝟭 α)) (name.mk_string "obviously" name.anonymous),
e_unit_iso_inv_hom_id' :
  auto_param
    (e_unit_iso_inv ≫ e_unit_iso_hom =
       𝟙
         ({obj := e_functor_obj,
             map := e_functor_map,
             map_id' := e_functor_map_id',
             map_comp' := e_functor_map_comp'} ⋙
            {obj := e_inverse_obj,
             map := e_inverse_map,
             map_id' := e_inverse_map_id',
             map_comp' := e_inverse_map_comp'}))
    (name.mk_string "obviously" name.anonymous),
e_functor_unit_iso_comp' :
  auto_param
    (∀ (X : α),
       {obj := e_functor_obj, map := e_functor_map, map_id' := e_functor_map_id', map_comp' := e_functor_map_comp'}.map
             ({hom := e_unit_iso_hom,
               inv := e_unit_iso_inv,
               hom_inv_id' := e_unit_iso_hom_inv_id',
               inv_hom_id' := e_unit_iso_inv_hom_id'}.hom.app
                X) ≫
           {hom := e_counit_iso_hom,
            inv := e_counit_iso_inv,
            hom_inv_id' := e_counit_iso_hom_inv_id',
            inv_hom_id' := e_counit_iso_inv_hom_id'}.hom.app
             ({obj := e_functor_obj,
               map := e_functor_map,
               map_id' := e_functor_map_id',
               map_comp' := e_functor_map_comp'}.obj
                X) =
         𝟙
           ({obj := e_functor_obj,
             map := e_functor_map,
             map_id' := e_functor_map_id',
             map_comp' := e_functor_map_comp'}.obj
              X))
    (name.mk_string "obviously" name.anonymous)
⊢ {functor := 𝟭 α ⋙
                  {obj := e_functor_obj,
                   map := e_functor_map,
                   map_id' := e_functor_map_id',
                   map_comp' := e_functor_map_comp'},
     inverse := {obj := e_inverse_obj,
                   map := e_inverse_map,
                   map_id' := e_inverse_map_id',
                   map_comp' := e_inverse_map_comp'} ⋙
                  𝟭 α,
     unit_iso := equivalence.adjointify_η
                   (iso.refl (𝟭 α) ≪≫
                      {hom := whisker_left (𝟭 α) {app := e_unit_iso_hom.app, naturality' := _},
                       inv := whisker_left (𝟭 α) {app := e_unit_iso_inv.app, naturality' := _},
                       hom_inv_id' := _,
                       inv_hom_id' := _})
                   ({hom := whisker_left
                                {obj := e_inverse_obj,
                                 map := e_inverse_map,
                                 map_id' := e_inverse_map_id',
                                 map_comp' := e_inverse_map_comp'}
                                {app := λ (c : α), e_functor_map (𝟙 c), naturality' := _},
                       inv := whisker_left
                                {obj := e_inverse_obj,
                                 map := e_inverse_map,
                                 map_id' := e_inverse_map_id',
                                 map_comp' := e_inverse_map_comp'}
                                {app := λ (c : α), e_functor_map ((𝟙 (𝟭 α ⋙ 𝟭 α)).app c),
                                 naturality' := _},
                       hom_inv_id' := _,
                       inv_hom_id' := _} ≪≫
                      {hom := e_counit_iso_hom,
                       inv := e_counit_iso_inv,
                       hom_inv_id' := e_counit_iso_hom_inv_id',
                       inv_hom_id' := e_counit_iso_inv_hom_id'}),
     counit_iso := {hom := whisker_left
                               {obj := e_inverse_obj,
                                map := e_inverse_map,
                                map_id' := e_inverse_map_id',
                                map_comp' := e_inverse_map_comp'}
                               {app := λ (c : α), e_functor_map (𝟙 c), naturality' := _},
                      inv := whisker_left
                               {obj := e_inverse_obj,
                                map := e_inverse_map,
                                map_id' := e_inverse_map_id',
                                map_comp' := e_inverse_map_comp'}
                               {app := λ (c : α), e_functor_map ((𝟙 (𝟭 α ⋙ 𝟭 α)).app c),
                                naturality' := _},
                      hom_inv_id' := _,
                      inv_hom_id' := _} ≪≫
                     {hom := e_counit_iso_hom,
                      inv := e_counit_iso_inv,
                      hom_inv_id' := e_counit_iso_hom_inv_id',
                      inv_hom_id' := e_counit_iso_inv_hom_id'},
     functor_unit_iso_comp' := _} =
    {functor := {obj := e_functor_obj,
                 map := e_functor_map,
                 map_id' := e_functor_map_id',
                 map_comp' := e_functor_map_comp'},
     inverse := {obj := e_inverse_obj,
                 map := e_inverse_map,
                 map_id' := e_inverse_map_id',
                 map_comp' := e_inverse_map_comp'},
     unit_iso := {hom := e_unit_iso_hom,
                  inv := e_unit_iso_inv,
                  hom_inv_id' := e_unit_iso_hom_inv_id',
                  inv_hom_id' := e_unit_iso_inv_hom_id'},
     counit_iso := {hom := e_counit_iso_hom,
                    inv := e_counit_iso_inv,
                    hom_inv_id' := e_counit_iso_hom_inv_id',
                    inv_hom_id' := e_counit_iso_inv_hom_id'},
     functor_unit_iso_comp' := e_functor_unit_iso_comp'}