-- Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
theorem equivalence₂UnitIso_eq : (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF

Proof state:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ (equivalence₁ hF).unitIso.hom.app X ≫
      (equivalence₁ hF).inverse.map
          (𝟙 (F.obj X) ≫ eB.counitIso.inv.app (F.obj X) ≫ 𝟙 (eB.functor.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 ((equivalence₁ hF).inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X)))) =
    (equivalence₂UnitIso eB hF).hom.app X

Tactic:
simp only [equivalence₁UnitIso_eq, equivalence₁UnitIso_hom_app, comp_id, id_comp, assoc,
  equivalence₂UnitIso_hom_app]

Result:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ eA.unitIso.hom.app X ≫
      eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫
          (equivalence₁ hF).inverse.map (eB.counitIso.inv.app (F.obj X)) =
    eA.unitIso.hom.app X ≫
      eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫
          eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X)))

Proof state:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X = (equivalence₂UnitIso eB hF).hom.app X

Tactic:
dsimp [equivalence₂]

Result:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ (equivalence₁ hF).unitIso.hom.app X ≫
      (equivalence₁ hF).inverse.map
          (𝟙 (F.obj X) ≫ eB.counitIso.inv.app (F.obj X) ≫ 𝟙 (eB.functor.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 ((equivalence₁ hF).inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X)))) =
    (equivalence₂UnitIso eB hF).hom.app X

Proof state:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF

Tactic:
ext X

Result:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ (equivalence₂ eB hF).unitIso.hom.app X = (equivalence₂UnitIso eB hF).hom.app X

Proof state:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
X : A
⊢ eA.unitIso.hom.app X ≫
      eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫
          (equivalence₁ hF).inverse.map (eB.counitIso.inv.app (F.obj X)) =
    eA.unitIso.hom.app X ≫
      eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫
          eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X)))

Tactic:
rfl

Result:
no goals