-- Mathlib/CategoryTheory/Localization/Equivalence.lean
@[simp]
lemma equivalence_counitIso_app (X : C₂) :
    (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) =
      (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) =
    (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X

Tactic:
ext

Result:
case w
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X)).hom =
    ((Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X).hom

Proof state:
case w
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ (liftNatTrans L₂ W₂ (F ⋙ G') L₂ (F' ⋙ G') (𝟭 D₂) β.hom).app (L₂.obj X) =
    (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X

Tactic:
rw [liftNatTrans_app]

Result:
case w
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X ≫ (Lifting.iso L₂ W₂ L₂ (𝟭 D₂)).inv.app X =
    (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X

Proof state:
case w
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X ≫ (Lifting.iso L₂ W₂ L₂ (𝟭 D₂)).inv.app X =
    (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X

Tactic:
dsimp [Lifting.iso]

Result:
case w
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ G'.map ((Lifting.iso' W₂).hom.app X) ≫ β.hom.app X ≫ 𝟙 (L₂.obj X) = G'.map ((Lifting.iso' W₂).hom.app X) ≫ β.hom.app X

Proof state:
case w
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X)).hom =
    ((Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X).hom

Tactic:
dsimp [equivalence, Equivalence.mk]

Result:
case w
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ (liftNatTrans L₂ W₂ (F ⋙ G') L₂ (F' ⋙ G') (𝟭 D₂) β.hom).app (L₂.obj X) =
    (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom.app X ≫ β.hom.app X

Proof state:
case w
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_9, u_2} C₂
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ G'.map ((Lifting.iso' W₂).hom.app X) ≫ β.hom.app X ≫ 𝟙 (L₂.obj X) = G'.map ((Lifting.iso' W₂).hom.app X) ≫ β.hom.app X

Tactic:
rw [comp_id]

Result:
no goals