[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
⊢ (yoneda.map (NatTrans.app h.unit X) ≫
      NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f)) =
    𝟙 (yoneda.obj ((𝟭 C).obj X))
[PROOFSTEP]
ext x
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((𝟭 C).obj X)).obj x
⊢ NatTrans.app
      (yoneda.map (NatTrans.app h.unit X) ≫
        NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f))
      x a✝ =
    NatTrans.app (𝟙 (yoneda.obj ((𝟭 C).obj X))) x a✝
[PROOFSTEP]
apply L.map_injective
[GOAL]
case w.h.h.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((𝟭 C).obj X)).obj x
⊢ L.map
      (NatTrans.app
        (yoneda.map (NatTrans.app h.unit X) ≫
          NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f))
        x a✝) =
    L.map (NatTrans.app (𝟙 (yoneda.obj ((𝟭 C).obj X))) x a✝)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
⊢ (NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f)) ≫
      yoneda.map (NatTrans.app h.unit X) =
    𝟙 (yoneda.obj ((L ⋙ R).obj X))
[PROOFSTEP]
ext x
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((L ⋙ R).obj X)).obj x
⊢ NatTrans.app
      ((NatTrans.mk fun Y f => L.preimage (↑(Adjunction.homEquiv h Y.unop (L.obj X)).symm f)) ≫
        yoneda.map (NatTrans.app h.unit X))
      x a✝ =
    NatTrans.app (𝟙 (yoneda.obj ((L ⋙ R).obj X))) x a✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((L ⋙ R).obj X)).obj x
⊢ L.preimage (↑(Adjunction.homEquiv h x.unop (L.obj X)).symm a✝) ≫ NatTrans.app h.unit X = a✝
[PROOFSTEP]
simp only [Adjunction.homEquiv_counit, preimage_comp, preimage_map, Category.assoc]
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((L ⋙ R).obj X)).obj x
⊢ a✝ ≫ L.preimage (NatTrans.app h.counit (L.obj X)) ≫ NatTrans.app h.unit X = a✝
[PROOFSTEP]
rw [← h.unit_naturality]
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
X : C
x : Cᵒᵖ
a✝ : (yoneda.obj ((L ⋙ R).obj X)).obj x
⊢ a✝ ≫ NatTrans.app h.unit (R.obj (L.obj X)) ≫ R.map (L.map (L.preimage (NatTrans.app h.counit (L.obj X)))) = a✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X : D
⊢ (coyoneda.map (NatTrans.app h.counit X).op ≫
      NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f)) =
    𝟙 (coyoneda.obj (op ((𝟭 D).obj X)))
[PROOFSTEP]
ext x
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((𝟭 D).obj X))).obj x
⊢ NatTrans.app
      (coyoneda.map (NatTrans.app h.counit X).op ≫
        NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f))
      x a✝ =
    NatTrans.app (𝟙 (coyoneda.obj (op ((𝟭 D).obj X)))) x a✝
[PROOFSTEP]
apply R.map_injective
[GOAL]
case w.h.h.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((𝟭 D).obj X))).obj x
⊢ R.map
      (NatTrans.app
        (coyoneda.map (NatTrans.app h.counit X).op ≫
          NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f))
        x a✝) =
    R.map (NatTrans.app (𝟙 (coyoneda.obj (op ((𝟭 D).obj X)))) x a✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X : D
⊢ (NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f)) ≫
      coyoneda.map (NatTrans.app h.counit X).op =
    𝟙 (coyoneda.obj (op ((R ⋙ L).obj X)))
[PROOFSTEP]
ext x
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((R ⋙ L).obj X))).obj x
⊢ NatTrans.app
      ((NatTrans.mk fun Y f => R.preimage (↑(Adjunction.homEquiv h (R.obj X) Y) f)) ≫
        coyoneda.map (NatTrans.app h.counit X).op)
      x a✝ =
    NatTrans.app (𝟙 (coyoneda.obj (op ((R ⋙ L).obj X)))) x a✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((R ⋙ L).obj X))).obj x
⊢ NatTrans.app h.counit X ≫ R.preimage (↑(Adjunction.homEquiv h (R.obj X) x) a✝) = a✝
[PROOFSTEP]
simp only [Adjunction.homEquiv_unit, preimage_comp, preimage_map]
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((R ⋙ L).obj X))).obj x
⊢ NatTrans.app h.counit X ≫ R.preimage (NatTrans.app h.unit (R.obj X)) ≫ a✝ = a✝
[PROOFSTEP]
rw [← h.counit_naturality]
[GOAL]
case w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
X x : D
a✝ : (coyoneda.obj (op ((R ⋙ L).obj X))).obj x
⊢ L.map (R.map (R.preimage (NatTrans.app h.unit (R.obj X)) ≫ a✝)) ≫ NatTrans.app h.counit x = a✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.unit
X Y : C
f g : X ⟶ Y
H : L.map f = L.map g
⊢ f = g
[PROOFSTEP]
rw [← (h.homEquiv X (L.obj Y)).apply_eq_iff_eq] at H 
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.unit
X Y : C
f g : X ⟶ Y
H : ↑(Adjunction.homEquiv h X (L.obj Y)) (L.map f) = ↑(Adjunction.homEquiv h X (L.obj Y)) (L.map g)
⊢ f = g
[PROOFSTEP]
simpa using H =≫ inv (h.unit.app Y)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.counit
X Y : D
f g : X ⟶ Y
H : R.map f = R.map g
⊢ f = g
[PROOFSTEP]
rw [← (h.homEquiv (R.obj X) Y).symm.apply_eq_iff_eq] at H 
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : IsIso h.counit
X Y : D
f g : X ⟶ Y
H : ↑(Adjunction.homEquiv h (R.obj X) Y).symm (R.map f) = ↑(Adjunction.homEquiv h (R.obj X) Y).symm (R.map g)
⊢ f = g
[PROOFSTEP]
simpa using inv (h.counit.app X) ≫= H
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
⊢ IsIso (whiskerLeft L h.counit)
[PROOFSTEP]
have := h.left_triangle
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerRight h.unit L ≫ whiskerLeft L h.counit = 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (whiskerLeft L h.counit)
[PROOFSTEP]
rw [← IsIso.eq_inv_comp] at this 
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerLeft L h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (whiskerLeft L h.counit)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerLeft L h.counit = inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (inv (whiskerRight h.unit L) ≫ 𝟙 (𝟭 C ⋙ L))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
⊢ IsIso (whiskerRight h.counit R)
[PROOFSTEP]
have := h.right_triangle
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerLeft R h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (whiskerRight h.counit R)
[PROOFSTEP]
rw [← IsIso.eq_inv_comp] at this 
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerRight h.counit R = inv (whiskerLeft R h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (whiskerRight h.counit R)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full L
inst✝ : Faithful L
this : whiskerRight h.counit R = inv (whiskerLeft R h.unit) ≫ 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (inv (whiskerLeft R h.unit) ≫ 𝟙 (R ⋙ 𝟭 C))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
⊢ IsIso (whiskerLeft R h.unit)
[PROOFSTEP]
have := h.right_triangle
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerLeft R h.unit ≫ whiskerRight h.counit R = 𝟙 (R ⋙ 𝟭 C)
⊢ IsIso (whiskerLeft R h.unit)
[PROOFSTEP]
rw [← IsIso.eq_comp_inv] at this 
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerLeft R h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)
⊢ IsIso (whiskerLeft R h.unit)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerLeft R h.unit = 𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R)
⊢ IsIso (𝟙 (R ⋙ 𝟭 C) ≫ inv (whiskerRight h.counit R))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
⊢ IsIso (whiskerRight h.unit L)
[PROOFSTEP]
have := h.left_triangle
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerRight h.unit L ≫ whiskerLeft L h.counit = 𝟙 (𝟭 C ⋙ L)
⊢ IsIso (whiskerRight h.unit L)
[PROOFSTEP]
rw [← IsIso.eq_comp_inv] at this 
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (whiskerLeft L h.counit)
⊢ IsIso (whiskerRight h.unit L)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : Full R
inst✝ : Faithful R
this : whiskerRight h.unit L = 𝟙 (𝟭 C ⋙ L) ≫ inv (whiskerLeft L h.counit)
⊢ IsIso (𝟙 (𝟭 C ⋙ L) ≫ inv (whiskerLeft L h.counit))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ R.obj Y
⊢ ↑((fun X Y =>
              Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                    (homEquiv adj (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (equivOfFullyFaithful iC).symm)
            X' Y).symm
      (f ≫ g) =
    L.map f ≫
      ↑((fun X Y =>
                Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                      (homEquiv adj (iC.obj X) (iD.obj Y)))
                    (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                  (equivOfFullyFaithful iC).symm)
              X Y).symm
        g
[PROOFSTEP]
apply iD.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ R.obj Y
⊢ iD.map
      (↑((fun X Y =>
                Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                      (homEquiv adj (iC.obj X) (iD.obj Y)))
                    (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                  (equivOfFullyFaithful iC).symm)
              X' Y).symm
        (f ≫ g)) =
    iD.map
      (L.map f ≫
        ↑((fun X Y =>
                  Trans.trans
                    (Trans.trans
                      (Trans.trans
                        (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                        (homEquiv adj (iC.obj X) (iD.obj Y)))
                      (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                    (equivOfFullyFaithful iC).symm)
                X Y).symm
          g)
[PROOFSTEP]
simpa [Trans.trans] using (comm1.inv.naturality_assoc f _).symm
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ ↑((fun X Y =>
            Trans.trans
              (Trans.trans
                (Trans.trans
                  (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                  (homEquiv adj (iC.obj X) (iD.obj Y)))
                (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
              (equivOfFullyFaithful iC).symm)
          X Y)
      (f ≫ g) =
    ↑((fun X Y =>
              Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                    (homEquiv adj (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (equivOfFullyFaithful iC).symm)
            X Y')
        f ≫
      R.map g
[PROOFSTEP]
apply iC.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ iC.map
      (↑((fun X Y =>
              Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                    (homEquiv adj (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (equivOfFullyFaithful iC).symm)
            X Y)
        (f ≫ g)) =
    iC.map
      (↑((fun X Y =>
                Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                      (homEquiv adj (iC.obj X) (iD.obj Y)))
                    (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                  (equivOfFullyFaithful iC).symm)
              X Y')
          f ≫
        R.map g)
[PROOFSTEP]
suffices : R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)
[GOAL]
case a
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
this : R'.map (iD.map g) ≫ NatTrans.app comm2.hom Y = NatTrans.app comm2.hom Y' ≫ iC.map (R.map g)
⊢ iC.map
      (↑((fun X Y =>
              Trans.trans
                (Trans.trans
                  (Trans.trans
                    (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                    (homEquiv adj (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (equivOfFullyFaithful iC).symm)
            X Y)
        (f ≫ g)) =
    iC.map
      (↑((fun X Y =>
                Trans.trans
                  (Trans.trans
                    (Trans.trans
                      (Trans.trans (equivOfFullyFaithful iD) (Iso.homCongr (comm1.symm.app X) (Iso.refl (iD.obj Y))))
                      (homEquiv adj (iC.obj X) (iD.obj Y)))
                    (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                  (equivOfFullyFaithful iC).symm)
              X Y')
          f ≫
        R.map g)
[PROOFSTEP]
simp [Trans.trans, this]
[GOAL]
case this
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
L✝ : C ⥤ D
R✝ : D ⥤ C
h : L✝ ⊣ R✝
C' : Type u₃
inst✝⁵ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
inst✝³ : Full iC
inst✝² : Faithful iC
inst✝¹ : Full iD
inst✝ : Faithful iD
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ R'.map (iD.map g) ≫ NatTrans.app comm2.hom Y = NatTrans.app comm2.hom Y' ≫ iC.map (R.map g)
[PROOFSTEP]
apply comm2.hom.naturality g
