[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.1655, u_3} D₁
inst✝⁴ : Category.{?u.1659, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ 𝟭 D₁ ⟶ G' ⋙ F'
[PROOFSTEP]
letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso'.symm
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.1655, u_3} D₁
inst✝⁴ : Category.{?u.1659, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso' := CatCommSq.iso'.symm }
⊢ 𝟭 D₁ ⟶ G' ⋙ F'
[PROOFSTEP]
exact Localization.liftNatTrans L₁ W₁ L₁ ((G ⋙ F) ⋙ L₁) (𝟭 D₁) (G' ⋙ F') (whiskerRight adj.unit L₁)
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_5, u_3} D₁
inst✝⁴ : Category.{u_6, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ NatTrans.app (ε adj L₁ W₁ L₂ G' F') (L₁.obj X₁) =
    L₁.map (NatTrans.app adj.unit X₁) ≫
      NatTrans.app (CatCommSq.iso F L₂ L₁ F').hom (G.obj X₁) ≫ F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').hom X₁)
[PROOFSTEP]
letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso'.symm
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_5, u_3} D₁
inst✝⁴ : Category.{u_6, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso' := CatCommSq.iso'.symm }
⊢ NatTrans.app (ε adj L₁ W₁ L₂ G' F') (L₁.obj X₁) =
    L₁.map (NatTrans.app adj.unit X₁) ≫
      NatTrans.app (CatCommSq.iso F L₂ L₁ F').hom (G.obj X₁) ≫ F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').hom X₁)
[PROOFSTEP]
simp only [ε, liftNatTrans_app, Lifting.iso, Iso.symm, Functor.id_obj, Functor.comp_obj, Lifting.id_iso',
  Functor.rightUnitor_hom_app, whiskerRight_app, CatCommSq.hComp_iso'_hom_app, id_comp]
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.13571, u_3} D₁
inst✝⁴ : Category.{?u.13575, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ F' ⋙ G' ⟶ 𝟭 D₂
[PROOFSTEP]
letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso'.symm
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.13571, u_3} D₁
inst✝⁴ : Category.{?u.13575, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso' := CatCommSq.iso'.symm }
⊢ F' ⋙ G' ⟶ 𝟭 D₂
[PROOFSTEP]
exact liftNatTrans L₂ W₂ ((F ⋙ G) ⋙ L₂) L₂ (F' ⋙ G') (𝟭 D₂) (whiskerRight adj.counit L₂)
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_6, u_3} D₁
inst✝⁴ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ NatTrans.app (η adj L₁ L₂ W₂ G' F') (L₂.obj X₂) =
    G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').inv X₂) ≫
      NatTrans.app (CatCommSq.iso G L₁ L₂ G').inv (F.obj X₂) ≫ L₂.map (NatTrans.app adj.counit X₂)
[PROOFSTEP]
letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso'.symm
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_6, u_3} D₁
inst✝⁴ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso' := CatCommSq.iso'.symm }
⊢ NatTrans.app (η adj L₁ L₂ W₂ G' F') (L₂.obj X₂) =
    G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').inv X₂) ≫
      NatTrans.app (CatCommSq.iso G L₁ L₂ G').inv (F.obj X₂) ≫ L₂.map (NatTrans.app adj.counit X₂)
[PROOFSTEP]
simp only [η, liftNatTrans_app, Lifting.iso, Iso.symm, CatCommSq.hComp_iso'_inv_app, whiskerRight_app, Lifting.id_iso',
  Functor.rightUnitor_inv_app, comp_id, assoc]
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
      (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F') =
    NatTrans.id (𝟭 D₁ ⋙ G')
[PROOFSTEP]
apply natTrans_ext L₁ W₁
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ ∀ (X : C₁),
    NatTrans.app
        (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
          (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F'))
        (L₁.obj X) =
      NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X)
[PROOFSTEP]
intro X₁
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ NatTrans.app
      (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
        (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F'))
      (L₁.obj X₁) =
    NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
have eq := congr_app adj.left_triangle X₁
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : NatTrans.app (whiskerRight adj.unit G ≫ whiskerLeft G adj.counit) X₁ = NatTrans.app (𝟙 (𝟭 C₁ ⋙ G)) X₁
⊢ NatTrans.app
      (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
        (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F'))
      (L₁.obj X₁) =
    NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
dsimp at eq 
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (NatTrans.app adj.unit X₁) ≫ NatTrans.app adj.counit (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ NatTrans.app
      (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
        (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F'))
      (L₁.obj X₁) =
    NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
rw [NatTrans.comp_app, NatTrans.comp_app, whiskerRight_app, Localization.ε_app, Functor.associator_hom_app, id_comp,
  whiskerLeft_app, G'.map_comp, G'.map_comp, assoc, assoc]
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (NatTrans.app adj.unit X₁) ≫ NatTrans.app adj.counit (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map (L₁.map (NatTrans.app adj.unit X₁)) ≫
      G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').hom (G.obj X₁)) ≫
        G'.map (F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').hom X₁)) ≫
          NatTrans.app (Localization.η adj L₁ L₂ W₂ G' F') (G'.obj (L₁.obj X₁)) =
    NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
erw [(Localization.η adj L₁ L₂ W₂ G' F').naturality, Localization.η_app, assoc, assoc, ← G'.map_comp_assoc, ←
  G'.map_comp_assoc, assoc, Iso.hom_inv_id_app, comp_id, (CatCommSq.iso G L₁ L₂ G').inv.naturality_assoc, ←
  L₂.map_comp_assoc, eq, L₂.map_id, id_comp, Iso.inv_hom_id_app]
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (NatTrans.app adj.unit X₁) ≫ NatTrans.app adj.counit (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ 𝟙 ((L₁ ⋙ G').obj ((𝟭 C₁).obj X₁)) = NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
rfl
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
      (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F' =
    NatTrans.id (F' ⋙ 𝟭 D₁)
[PROOFSTEP]
apply natTrans_ext L₂ W₂
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ ∀ (X : C₂),
    NatTrans.app
        (whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
          (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F')
        (L₂.obj X) =
      NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X)
[PROOFSTEP]
intro X₂
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ NatTrans.app
      (whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
        (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F')
      (L₂.obj X₂) =
    NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
have eq := congr_app adj.right_triangle X₂
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : NatTrans.app (whiskerLeft F adj.unit ≫ whiskerRight adj.counit F) X₂ = NatTrans.app (𝟙 (F ⋙ 𝟭 C₁)) X₂
⊢ NatTrans.app
      (whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
        (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F')
      (L₂.obj X₂) =
    NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
dsimp at eq 
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : NatTrans.app adj.unit (F.obj X₂) ≫ F.map (NatTrans.app adj.counit X₂) = 𝟙 (F.obj X₂)
⊢ NatTrans.app
      (whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
        (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F')
      (L₂.obj X₂) =
    NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
rw [NatTrans.comp_app, NatTrans.comp_app, whiskerLeft_app, whiskerRight_app, Localization.η_app,
  Functor.associator_inv_app, id_comp, F'.map_comp, F'.map_comp]
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : NatTrans.app adj.unit (F.obj X₂) ≫ F.map (NatTrans.app adj.counit X₂) = 𝟙 (F.obj X₂)
⊢ NatTrans.app (Localization.ε adj L₁ W₁ L₂ G' F') (F'.obj (L₂.obj X₂)) ≫
      F'.map (G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').inv X₂)) ≫
        F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').inv (F.obj X₂)) ≫ F'.map (L₂.map (NatTrans.app adj.counit X₂)) =
    NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
erw [← (Localization.ε _ _ _ _ _ _).naturality_assoc, Localization.ε_app, assoc, assoc, ← F'.map_comp_assoc,
  Iso.hom_inv_id_app, F'.map_id, id_comp, ← NatTrans.naturality, ← L₁.map_comp_assoc, eq, L₁.map_id, id_comp,
  Iso.inv_hom_id_app]
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : NatTrans.app adj.unit (F.obj X₂) ≫ F.map (NatTrans.app adj.counit X₂) = 𝟙 (F.obj X₂)
⊢ 𝟙 ((L₂ ⋙ F').obj X₂) = NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
rfl
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_5, u_3} D₁
inst✝⁴ : Category.{u_6, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ NatTrans.app (localization adj L₁ W₁ L₂ W₂ G' F').unit (L₁.obj X₁) =
    L₁.map (NatTrans.app adj.unit X₁) ≫
      NatTrans.app (CatCommSq.iso F L₂ L₁ F').hom (G.obj X₁) ≫ F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').hom X₁)
[PROOFSTEP]
apply Localization.ε_app
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_6, u_3} D₁
inst✝⁴ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ NatTrans.app (localization adj L₁ W₁ L₂ W₂ G' F').counit (L₂.obj X₂) =
    G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').inv X₂) ≫
      NatTrans.app (CatCommSq.iso G L₁ L₂ G').inv (F.obj X₂) ≫ L₂.map (NatTrans.app adj.counit X₂)
[PROOFSTEP]
apply Localization.η_app
