[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₁ hF).counitIso = equivalence₁CounitIso hF
[PROOFSTEP]
ext Y
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y : B'
⊢ NatTrans.app (equivalence₁ hF).counitIso.hom Y = NatTrans.app (equivalence₁CounitIso hF).hom Y
[PROOFSTEP]
dsimp [equivalence₁]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y : B'
⊢ NatTrans.app (Functor.asEquivalence F).counitIso.hom Y = NatTrans.app (equivalence₁CounitIso hF).hom Y
[PROOFSTEP]
unfold Functor.asEquivalence
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y : B'
⊢ NatTrans.app (Equivalence.mk' F (IsEquivalence.inverse F) IsEquivalence.unitIso IsEquivalence.counitIso).counitIso.hom
      Y =
    NatTrans.app (equivalence₁CounitIso hF).hom Y
[PROOFSTEP]
dsimp [equivalence₀, IsEquivalence.inverse, IsEquivalence.ofEquivalence]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y : B'
⊢ NatTrans.app IsEquivalence.counitIso.hom Y = NatTrans.app (equivalence₁CounitIso hF).hom Y
[PROOFSTEP]
simp
[GOAL]
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.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₁ hF).unitIso = equivalence₁UnitIso hF
[PROOFSTEP]
ext X
[GOAL]
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.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (equivalence₁ hF).unitIso.hom X = NatTrans.app (equivalence₁UnitIso hF).hom X
[PROOFSTEP]
dsimp [equivalence₁]
[GOAL]
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.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (Functor.asEquivalence F).unitIso.hom X = NatTrans.app (equivalence₁UnitIso hF).hom X
[PROOFSTEP]
unfold Functor.asEquivalence
[GOAL]
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.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (Equivalence.mk' F (IsEquivalence.inverse F) IsEquivalence.unitIso IsEquivalence.counitIso).unitIso.hom
      X =
    NatTrans.app (equivalence₁UnitIso hF).hom X
[PROOFSTEP]
dsimp [NatIso.hcomp, IsEquivalence.ofEquivalence]
[GOAL]
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.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app IsEquivalence.unitIso.hom X = NatTrans.app (equivalence₁UnitIso hF).hom X
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF
[PROOFSTEP]
ext Y'
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y' : B
⊢ NatTrans.app (equivalence₂ eB hF).counitIso.hom Y' = NatTrans.app (equivalence₂CounitIso eB hF).hom Y'
[PROOFSTEP]
dsimp [equivalence₂, Iso.refl]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y' : B
⊢ eB.inverse.map (NatTrans.app (equivalence₁ hF).counitIso.hom (eB.functor.obj Y')) ≫ NatTrans.app eB.unitIso.inv Y' =
    NatTrans.app (equivalence₂CounitIso eB hF).hom Y'
[PROOFSTEP]
simp only [equivalence₁CounitIso_eq, equivalence₂CounitIso_hom_app, equivalence₁CounitIso_hom_app, Functor.map_comp,
  assoc]
[GOAL]
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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF
[PROOFSTEP]
ext X
[GOAL]
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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (equivalence₂ eB hF).unitIso.hom X = NatTrans.app (equivalence₂UnitIso eB hF).hom X
[PROOFSTEP]
dsimp [equivalence₂]
[GOAL]
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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (equivalence₁ hF).unitIso.hom X ≫
      (equivalence₁ hF).inverse.map (NatTrans.app eB.counitIso.inv (F.obj X)) =
    NatTrans.app (equivalence₂UnitIso eB hF).hom X
[PROOFSTEP]
simp only [equivalence₂UnitIso_hom_app, equivalence₁UnitIso_eq, equivalence₁UnitIso_hom_app, assoc,
  NatIso.cancel_natIso_hom_left]
[GOAL]
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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app eA.unitIso.hom X ≫
      eA.inverse.map (NatTrans.app e'.unitIso.hom (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (NatTrans.app hF.hom X)) ≫
          (equivalence₁ hF).inverse.map (NatTrans.app eB.counitIso.inv (F.obj X)) =
    NatTrans.app eA.unitIso.hom X ≫
      eA.inverse.map (NatTrans.app e'.unitIso.hom (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (NatTrans.app hF.hom X)) ≫
          eA.inverse.map (e'.inverse.map (NatTrans.app eB.counitIso.inv (F.obj X)))
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{?u.46977, u_1} A
inst✝² : Category.{?u.46981, u_2} A'
inst✝¹ : Category.{?u.46985, u_3} B
inst✝ : Category.{?u.46989, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ IsEquivalence G
[PROOFSTEP]
refine' IsEquivalence.ofIso _ (IsEquivalence.ofEquivalence (equivalence₂ eB hF).symm)
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{?u.46977, u_1} A
inst✝² : Category.{?u.46981, u_2} A'
inst✝¹ : Category.{?u.46985, u_3} B
inst✝ : Category.{?u.46989, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (CategoryTheory.Equivalence.symm (equivalence₂ eB hF)).functor ≅ G
[PROOFSTEP]
calc
  eB.functor ⋙ e'.inverse ⋙ eA.inverse ≅ (eB.functor ⋙ e'.inverse) ⋙ eA.inverse := Iso.refl _
  _ ≅ (G ⋙ eA.functor) ⋙ eA.inverse := (isoWhiskerRight hG _)
  _ ≅ G ⋙ 𝟭 A := (isoWhiskerLeft _ eA.unitIso.symm)
  _ ≅ G := Functor.rightUnitor G
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{?u.52568, u_1} A
inst✝² : Category.{?u.52572, u_2} A'
inst✝¹ : Category.{?u.52576, u_3} B
inst✝ : Category.{?u.52580, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
⊢ (G ⋙ eA.functor) ⋙ e'.functor ≅ G ⋙ eA.functor ⋙ e'.functor
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso = equivalenceCounitIso η
[PROOFSTEP]
ext1
[GOAL]
case w
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso.hom = (equivalenceCounitIso η).hom
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case w.app
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso.hom.app = (equivalenceCounitIso η).hom.app
[PROOFSTEP]
ext Y
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app (equivalence hF hG).counitIso.hom Y = NatTrans.app (equivalenceCounitIso η).hom Y
[PROOFSTEP]
dsimp [equivalence, Functor.asEquivalence, IsEquivalence.ofEquivalence]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app IsEquivalence.unitIso.inv Y = NatTrans.app (equivalenceCounitIso η).hom Y
[PROOFSTEP]
rw [equivalenceCounitIso_hom_app, IsEquivalence.ofIso_unitIso_inv_app]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ (IsEquivalence.inverse (equivalence₂ eB hF).inverse).map
        (NatTrans.app
          (((Iso.refl (eB.functor ⋙ e'.inverse ⋙ eA.inverse) ≪≫ isoWhiskerRight hG eA.inverse) ≪≫
                isoWhiskerLeft G eA.unitIso.symm) ≪≫
              Functor.rightUnitor G).inv
          Y) ≫
      NatTrans.app IsEquivalence.unitIso.inv Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
dsimp
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (F.map
          (𝟙 (G.obj Y) ≫
            NatTrans.app eA.unitIso.hom (G.obj Y) ≫
              eA.inverse.map (NatTrans.app hG.inv Y) ≫ 𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))))) ≫
      NatTrans.app (equivalence₂ eB hF).counitIso.hom Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
simp only [comp_id, id_comp, F.map_comp, assoc, equivalence₂CounitIso_eq, equivalence₂CounitIso_hom_app, ←
  eB.inverse.map_comp_assoc, ← τ₀_hom_app, hη, τ₁_hom_app]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (F.map (NatTrans.app eA.unitIso.hom (G.obj Y)) ≫
          F.map (eA.inverse.map (NatTrans.app hG.inv Y)) ≫
            NatTrans.app hF.inv (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (NatTrans.app eA.counitIso.hom (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (NatTrans.app hG.hom Y) ≫ NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y) ≫
      NatTrans.app eB.unitIso.inv Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
erw [hF.inv.naturality_assoc, hF.inv.naturality_assoc]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (NatTrans.app hF.inv (G.obj Y) ≫
          (eA.functor ⋙ e'.functor).map (NatTrans.app eA.unitIso.hom (G.obj Y)) ≫
            (eA.functor ⋙ e'.functor).map (eA.inverse.map (NatTrans.app hG.inv Y)) ≫
              e'.functor.map (NatTrans.app eA.counitIso.hom (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (NatTrans.app hG.hom Y) ≫ NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y) ≫
      NatTrans.app eB.unitIso.inv Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
dsimp
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (NatTrans.app hF.inv (G.obj Y) ≫
          e'.functor.map (eA.functor.map (NatTrans.app eA.unitIso.hom (G.obj Y))) ≫
            e'.functor.map (eA.functor.map (eA.inverse.map (NatTrans.app hG.inv Y))) ≫
              e'.functor.map (NatTrans.app eA.counitIso.hom (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (NatTrans.app hG.hom Y) ≫ NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y) ≫
      NatTrans.app eB.unitIso.inv Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
congr 2
[GOAL]
case w.app.h.e_a.e_a
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app hF.inv (G.obj Y) ≫
      e'.functor.map (eA.functor.map (NatTrans.app eA.unitIso.hom (G.obj Y))) ≫
        e'.functor.map (eA.functor.map (eA.inverse.map (NatTrans.app hG.inv Y))) ≫
          e'.functor.map (NatTrans.app eA.counitIso.hom (e'.inverse.obj (eB.functor.obj Y))) ≫
            e'.functor.map (NatTrans.app hG.hom Y) ≫ NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y =
    NatTrans.app η.hom Y
[PROOFSTEP]
simp only [assoc, ← e'.functor.map_comp_assoc, Equivalence.fun_inv_map, Iso.inv_hom_id_app_assoc, hG.inv_hom_id_app]
[GOAL]
case w.app.h.e_a.e_a
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app hF.inv (G.obj Y) ≫
      e'.functor.map
          (eA.functor.map (NatTrans.app eA.unitIso.hom (G.obj Y)) ≫
            NatTrans.app (Equivalence.counit eA) (eA.functor.obj (G.obj Y)) ≫ 𝟙 ((G ⋙ eA.functor).obj Y)) ≫
        NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y =
    NatTrans.app η.hom Y
[PROOFSTEP]
dsimp
[GOAL]
case w.app.h.e_a.e_a
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, 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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app hF.inv (G.obj Y) ≫
      e'.functor.map
          (eA.functor.map (NatTrans.app eA.unitIso.hom (G.obj Y)) ≫
            NatTrans.app (Equivalence.counit eA) (eA.functor.obj (G.obj Y)) ≫ 𝟙 (eA.functor.obj (G.obj Y))) ≫
        NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y =
    NatTrans.app η.hom Y
[PROOFSTEP]
rw [comp_id, eA.functor_unitIso_comp, e'.functor.map_id, id_comp, hF.inv_hom_id_app_assoc]
[GOAL]
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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso = equivalenceUnitIso hG ε
[PROOFSTEP]
ext1
[GOAL]
case w
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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso.hom = (equivalenceUnitIso hG ε).hom
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case w.app
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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso.hom.app = (equivalenceUnitIso hG ε).hom.app
[PROOFSTEP]
ext X
[GOAL]
case w.app.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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app (equivalence hF hG).unitIso.hom X = NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
dsimp [equivalence, Functor.asEquivalence, IsEquivalence.ofEquivalence, IsEquivalence.inverse]
[GOAL]
case w.app.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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app IsEquivalence.counitIso.inv X = NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
rw [IsEquivalence.ofIso_counitIso_inv_app]
[GOAL]
case w.app.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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app IsEquivalence.counitIso.inv X ≫
      NatTrans.app
        (((Iso.refl (eB.functor ⋙ e'.inverse ⋙ eA.inverse) ≪≫ isoWhiskerRight hG eA.inverse) ≪≫
              isoWhiskerLeft G eA.unitIso.symm) ≪≫
            Functor.rightUnitor G).hom
        ((IsEquivalence.inverse (equivalence₂ eB hF).inverse).obj X) =
    NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
dsimp
[GOAL]
case w.app.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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app (equivalence₂ eB hF).unitIso.hom X ≫
      ((𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫
            eA.inverse.map (NatTrans.app hG.hom (eB.inverse.obj (F.obj X)))) ≫
          NatTrans.app eA.unitIso.inv (G.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 (G.obj (eB.inverse.obj (F.obj X))) =
    NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
erw [id_comp, comp_id]
[GOAL]
case w.app.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
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app (equivalence₂ eB hF).unitIso.hom X ≫
      eA.inverse.map (NatTrans.app hG.hom (eB.inverse.obj (F.obj X))) ≫
        NatTrans.app eA.unitIso.inv (G.obj (eB.inverse.obj (F.obj X))) =
    NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
simp only [equivalence₂UnitIso_eq eB hF, equivalence₂UnitIso_hom_app, assoc, equivalenceUnitIso_hom_app, ←
  eA.inverse.map_comp_assoc, ← hε, υ_hom_app]
