[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X✝ : C
Y Y' : D
X : C
⊢ ↑(homEquiv adj X (F.obj X)) (𝟙 (F.obj X)) = NatTrans.app adj.unit X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X✝ : C
Y Y' X : D
⊢ ↑(homEquiv adj (G.obj X) X).symm (𝟙 (G.obj X)) = NatTrans.app adj.counit X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ ↑(homEquiv adj X' Y).symm (f ≫ g) = F.map f ≫ ↑(homEquiv adj X Y).symm g
[PROOFSTEP]
rw [homEquiv_counit, F.map_comp, assoc, adj.homEquiv_counit.symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ ↑(homEquiv adj X' Y) (F.map f ≫ g) = f ≫ ↑(homEquiv adj X Y) g
[PROOFSTEP]
rw [← Equiv.eq_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = ↑(homEquiv adj X' Y).symm (f ≫ ↑(homEquiv adj X Y) g)
[PROOFSTEP]
simp only [Equiv.symm_apply_apply, eq_self_iff_true, homEquiv_naturality_left_symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ ↑(homEquiv adj X Y') (f ≫ g) = ↑(homEquiv adj X Y) f ≫ G.map g
[PROOFSTEP]
rw [homEquiv_unit, G.map_comp, ← assoc, ← homEquiv_unit]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ ↑(homEquiv adj X Y').symm (f ≫ G.map g) = ↑(homEquiv adj X Y).symm f ≫ g
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = ↑(homEquiv adj X Y') (↑(homEquiv adj X Y).symm f ≫ g)
[PROOFSTEP]
simp only [homEquiv_naturality_right, eq_self_iff_true, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
⊢ whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 (𝟭 C ⋙ F)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
x✝ : C
⊢ NatTrans.app (whiskerRight adj.unit F ≫ whiskerLeft F adj.counit) x✝ = NatTrans.app (𝟙 (𝟭 C ⋙ F)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
x✝ : C
⊢ F.map (NatTrans.app adj.unit x✝) ≫ NatTrans.app adj.counit (F.obj x✝) = 𝟙 (F.obj x✝)
[PROOFSTEP]
erw [← adj.homEquiv_counit, Equiv.symm_apply_eq, adj.homEquiv_unit]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
x✝ : C
⊢ NatTrans.app adj.unit x✝ = NatTrans.app adj.unit x✝ ≫ G.map (𝟙 (F.obj x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
⊢ whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 (G ⋙ 𝟭 C)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ NatTrans.app (whiskerLeft G adj.unit ≫ whiskerRight adj.counit G) x✝ = NatTrans.app (𝟙 (G ⋙ 𝟭 C)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ NatTrans.app adj.unit (G.obj x✝) ≫ G.map (NatTrans.app adj.counit x✝) = 𝟙 (G.obj x✝)
[PROOFSTEP]
erw [← adj.homEquiv_unit, ← Equiv.eq_symm_apply, adj.homEquiv_counit]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ NatTrans.app adj.counit x✝ = F.map (𝟙 (G.obj x✝)) ≫ NatTrans.app adj.counit x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : ↑(homEquiv adj A B) f = g
⊢ f = ↑(homEquiv adj A B).symm g
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
⊢ f = ↑(homEquiv adj A B).symm (↑(homEquiv adj A B) f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : f = ↑(homEquiv adj A B).symm g
⊢ ↑(homEquiv adj A B) f = g
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
g : A ⟶ G.obj B
⊢ ↑(homEquiv adj A B) (↑(homEquiv adj A B).symm g) = g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : g = ↑(homEquiv adj A B) f
⊢ ↑(homEquiv adj A B).symm g = f
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
⊢ ↑(homEquiv adj A B).symm (↑(homEquiv adj A B) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : ↑(homEquiv adj A B).symm g = f
⊢ g = ↑(homEquiv adj A B) f
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
g : A ⟶ G.obj B
⊢ g = ↑(homEquiv adj A B) (↑(homEquiv adj A B).symm g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ ↑(homEquiv adj X' (F.obj X)) (F.map f) ≫ G.map g = f ≫ ↑(homEquiv adj X Y) g
[PROOFSTEP]
rw [← homEquiv_naturality_right, ← Equiv.eq_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = ↑(homEquiv adj X' Y).symm (f ≫ ↑(homEquiv adj X Y) g)
[PROOFSTEP]
simp
  -- @[simp] -- Porting note: LHS simplifies, added aux lemma above
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ ↑(homEquiv adj X' Y) (F.map f ≫ g) = f ≫ ↑(homEquiv adj X Y) g
[PROOFSTEP]
rw [← Equiv.eq_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = ↑(homEquiv adj X' Y).symm (f ≫ ↑(homEquiv adj X Y) g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ F.map f ≫ ↑(homEquiv adj (G.obj Y) Y').symm (G.map g) = ↑(homEquiv adj X Y).symm f ≫ g
[PROOFSTEP]
rw [← homEquiv_naturality_left_symm, Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = ↑(homEquiv adj X Y') (↑(homEquiv adj X Y).symm f ≫ g)
[PROOFSTEP]
simp
  -- @[simp] -- Porting note: LHS simplifies, added aux lemma above
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ ↑(homEquiv adj X Y').symm (f ≫ G.map g) = ↑(homEquiv adj X Y).symm f ≫ g
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = ↑(homEquiv adj X Y') (↑(homEquiv adj X Y).symm f ≫ g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    (𝟭 C).map f ≫ (fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) Y =
      (fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) X ≫ (F ⋙ G).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 C).map f✝ ≫ (fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) Y✝ =
    (fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) X✝ ≫ (F ⋙ G).map f✝
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left, ← adj.homEquiv_naturality_right]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ↑(CoreHomEquiv.homEquiv adj ((𝟭 C).obj X✝) (F.obj Y✝)) (F.map ((𝟭 C).map f✝) ≫ 𝟙 (F.obj Y✝)) =
    ↑(CoreHomEquiv.homEquiv adj ((𝟭 C).obj X✝) (F.obj Y✝)) (𝟙 (F.obj X✝) ≫ F.map f✝)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ↑(CoreHomEquiv.homEquiv adj X✝ (F.obj Y✝)) (F.map f✝ ≫ 𝟙 (F.obj Y✝)) =
    ↑(CoreHomEquiv.homEquiv adj X✝ (F.obj Y✝)) (𝟙 (F.obj X✝) ≫ F.map f✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    (G ⋙ F).map f ≫ (fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y))) Y =
      (fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y))) X ≫ (𝟭 D).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ (G ⋙ F).map f✝ ≫ (fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y))) Y✝ =
    (fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y))) X✝ ≫ (𝟭 D).map f✝
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ ↑(CoreHomEquiv.homEquiv adj (G.obj X✝) ((𝟭 D).obj Y✝)).symm (G.map f✝ ≫ 𝟙 (G.obj Y✝)) =
    ↑(CoreHomEquiv.homEquiv adj (G.obj X✝) ((𝟭 D).obj Y✝)).symm (𝟙 (G.obj X✝) ≫ G.map ((𝟭 D).map f✝))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ ↑(CoreHomEquiv.homEquiv adj (G.obj X✝) Y✝).symm (G.map f✝ ≫ 𝟙 (G.obj Y✝)) =
    ↑(CoreHomEquiv.homEquiv adj (G.obj X✝) Y✝).symm (𝟙 (G.obj X✝) ≫ G.map f✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ↑(CoreHomEquiv.homEquiv adj X Y) f =
    NatTrans.app (NatTrans.mk fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) X ≫ G.map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_right]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ↑(CoreHomEquiv.homEquiv adj X Y) f = ↑(CoreHomEquiv.homEquiv adj ((𝟭 C).obj X) Y) (𝟙 (F.obj X) ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : X ⟶ G.obj Y
⊢ ↑(CoreHomEquiv.homEquiv adj X Y).symm f =
    F.map f ≫
      NatTrans.app (NatTrans.mk fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y)))
        Y
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left_symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : X ⟶ G.obj Y
⊢ ↑(CoreHomEquiv.homEquiv adj X Y).symm f = ↑(CoreHomEquiv.homEquiv adj X ((𝟭 D).obj Y)).symm (f ≫ 𝟙 (G.obj Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (fun g => F.map g ≫ NatTrans.app adj.counit Y) ((fun f => NatTrans.app adj.unit X ≫ G.map f) f) = f
[PROOFSTEP]
change F.map (_ ≫ _) ≫ _ = _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ F.map (NatTrans.app adj.unit X ≫ G.map f) ≫ NatTrans.app adj.counit Y = f
[PROOFSTEP]
rw [F.map_comp, assoc, ← Functor.comp_map, adj.counit.naturality, ← assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X)) ≫ (𝟭 D).map f = f
[PROOFSTEP]
convert id_comp f
[GOAL]
case h.e'_2.h.e'_6.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X
⊢ F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
have t := congrArg (fun (s : NatTrans (𝟭 C ⋙ F) (F ⋙ 𝟭 D)) => s.app X) adj.left_triangle
[GOAL]
case h.e'_2.h.e'_6.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X
t :
  (fun s => NatTrans.app s X) (whiskerRight adj.unit F ≫ (Functor.associator F G F).hom ≫ whiskerLeft F adj.counit) =
    (fun s => NatTrans.app s X) (NatTrans.id (𝟭 C ⋙ F))
⊢ F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
dsimp at t 
[GOAL]
case h.e'_2.h.e'_6.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X
t : F.map (NatTrans.app adj.unit X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
⊢ F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
simp only [id_comp] at t 
[GOAL]
case h.e'_2.h.e'_6.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X
t : F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
⊢ F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
exact t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ (fun f => NatTrans.app adj.unit X ≫ G.map f) ((fun g => F.map g ≫ NatTrans.app adj.counit Y) g) = g
[PROOFSTEP]
change _ ≫ G.map (_ ≫ _) = _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ NatTrans.app adj.unit X ≫ G.map (F.map g ≫ NatTrans.app adj.counit Y) = g
[PROOFSTEP]
rw [G.map_comp, ← assoc, ← Functor.comp_map, ← adj.unit.naturality, assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ (𝟭 C).map g ≫ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = g
[PROOFSTEP]
convert comp_id g
[GOAL]
case h.e'_2.h.e'_7.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y
⊢ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
[PROOFSTEP]
have t := congrArg (fun t : NatTrans (G ⋙ 𝟭 C) (𝟭 D ⋙ G) => t.app Y) adj.right_triangle
[GOAL]
case h.e'_2.h.e'_7.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y
t :
  (fun t => NatTrans.app t Y) (whiskerLeft G adj.unit ≫ (Functor.associator G F G).inv ≫ whiskerRight adj.counit G) =
    (fun t => NatTrans.app t Y) (NatTrans.id (G ⋙ 𝟭 C))
⊢ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
[PROOFSTEP]
dsimp at t 
[GOAL]
case h.e'_2.h.e'_7.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y
t : NatTrans.app adj.unit (G.obj Y) ≫ 𝟙 (G.obj (F.obj (G.obj Y))) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
⊢ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
[PROOFSTEP]
simp only [id_comp] at t 
[GOAL]
case h.e'_2.h.e'_7.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y
t : NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
⊢ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
[PROOFSTEP]
exact t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : C ⥤ D
G : D ⥤ C
F F' : C ⥤ D
iso : F ≅ F'
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (fun g => NatTrans.app iso.hom X ≫ g) ((fun f => NatTrans.app iso.inv X ≫ f) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : C ⥤ D
G : D ⥤ C
F F' : C ⥤ D
iso : F ≅ F'
X : C
Y : D
g : F'.obj X ⟶ Y
⊢ (fun f => NatTrans.app iso.inv X ≫ f) ((fun g => NatTrans.app iso.hom X ≫ g) g) = g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G✝ G G' : D ⥤ C
iso : G ≅ G'
X : C
Y : D
f : X ⟶ G.obj Y
⊢ (fun g => g ≫ NatTrans.app iso.inv Y) ((fun f => f ≫ NatTrans.app iso.hom Y) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G✝ G G' : D ⥤ C
iso : G ≅ G'
X : C
Y : D
g : X ⟶ G'.obj Y
⊢ (fun f => f ≫ NatTrans.app iso.hom Y) ((fun g => g ≫ NatTrans.app iso.inv Y) g) = g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
[PROOFSTEP]
rw [Equiv.symm_apply_eq, he]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = ↑(e X Y) (↑(e X Y).symm f) ≫ G.map g
[PROOFSTEP]
simp
  -- #align category_theory.adjunction.he' category_theory.adjunction.he'
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ { obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map (f ≫ f') =
    { obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f ≫
      { obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f'
[PROOFSTEP]
rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      G.map
        ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
conv =>
  rhs
  rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      G.map
        ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
  rhs
  rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      G.map
        ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
  rhs
  rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      G.map
        ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
rhs
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
    G.map
      ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) = f ≫ f' ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ ↑(e X' Y).symm (f ≫ g) = (leftAdjointOfEquiv e he).map f ≫ ↑(e X Y).symm g
[PROOFSTEP]
have := @he' C _ D _ G F_obj e he
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ ↑(e X' Y).symm (f ≫ g) = (leftAdjointOfEquiv e he).map f ≫ ↑(e X Y).symm g
[PROOFSTEP]
erw [← this, ← Equiv.apply_eq_iff_eq (e X' Y)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ ↑(e X' Y) (↑(e X' Y).symm (f ≫ g)) =
    ↑(e X' Y)
      (↑(e X' Y).symm ((f ≫ ↑(e X ((fun X => F_obj X) X)) (𝟙 ((fun X => F_obj X) X))) ≫ G.map (↑(e X Y).symm g)))
[PROOFSTEP]
simp [(he X' (F_obj X) Y (e X Y |>.symm g) (leftAdjointOfEquiv e he |>.map f)).symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ f ≫ g = f ≫ ↑(e X (F_obj X)) (𝟙 (F_obj X)) ≫ G.map (↑(e X Y).symm g)
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ g = ↑(e X (F_obj X)) (𝟙 (F_obj X)) ≫ G.map (↑(e X Y).symm g)
[PROOFSTEP]
rw [← he]
[GOAL]
case e_a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ g = ↑(e X Y) (𝟙 (F_obj X) ≫ ↑(e X Y).symm g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ F.map f ≫ ↑(e X Y).symm g = ↑(e X' Y).symm (f ≫ g)
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ F.map f ≫ ↑(e X Y).symm g = ↑(e X' Y).symm (f ≫ g)
[PROOFSTEP]
rw [Equiv.eq_symm_apply, he]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ f ≫ ↑(e X Y) (↑(e X Y).symm g) = f ≫ g
[PROOFSTEP]
simp
  -- #align category_theory.adjunction.he' category_theory.adjunction.he'
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ { obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map (g ≫ g') =
    { obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g ≫
      { obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g'
[PROOFSTEP]
rw [← Equiv.eq_symm_apply, ← he'' e he, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
      ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
conv =>
  rhs
  rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
      ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
  rhs
  rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
      ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
  rhs
  rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
      ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
rhs
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
    ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' = (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ g'
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
⊢ ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ (rightAdjointOfEquiv e he).obj Y),
    ↑(e X' Y).symm (f ≫ g) = F.map f ≫ ↑(e X Y).symm g
[PROOFSTEP]
intro X X' Y f g
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ ↑(e X Y).symm (f ≫ g) = F.map f ≫ ↑(e X' Y).symm g
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g = ↑(e X Y) (F.map f ≫ ↑(e X' Y).symm g)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g = ↑(e X Y) (F.map f ≫ ↑(e X' Y).symm g)
[PROOFSTEP]
rw [he]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g = f ≫ ↑(e X' Y) (↑(e X' Y).symm g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
⊢ ∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), ↑(e X Y') (f ≫ g) = ↑(e X Y) f ≫ (rightAdjointOfEquiv e he).map g
[PROOFSTEP]
intro X Y Y' g h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X : C
Y Y' : D
g : F.obj X ⟶ Y
h : Y ⟶ Y'
⊢ ↑(e X Y') (g ≫ h) = ↑(e X Y) g ≫ (rightAdjointOfEquiv e he).map h
[PROOFSTEP]
erw [← he, Equiv.apply_eq_iff_eq, ← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ whiskerRight (unit e) e.functor ≫
      (Functor.associator e.functor e.inverse e.functor).hom ≫ whiskerLeft e.functor (counit e) =
    NatTrans.id (𝟭 C ⋙ e.functor)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : C
⊢ NatTrans.app
      (whiskerRight (unit e) e.functor ≫
        (Functor.associator e.functor e.inverse e.functor).hom ≫ whiskerLeft e.functor (counit e))
      x✝ =
    NatTrans.app (NatTrans.id (𝟭 C ⋙ e.functor)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : C
⊢ e.functor.map (NatTrans.app (unit e) x✝) ≫
      𝟙 (e.functor.obj (e.inverse.obj (e.functor.obj x✝))) ≫ NatTrans.app (counit e) (e.functor.obj x✝) =
    𝟙 (e.functor.obj x✝)
[PROOFSTEP]
simp only [id_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : C
⊢ e.functor.map (NatTrans.app (unit e) x✝) ≫ NatTrans.app (counit e) (e.functor.obj x✝) = 𝟙 (e.functor.obj x✝)
[PROOFSTEP]
exact e.functor_unit_comp _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ whiskerLeft e.inverse (unit e) ≫
      (Functor.associator e.inverse e.functor e.inverse).inv ≫ whiskerRight (counit e) e.inverse =
    NatTrans.id (e.inverse ⋙ 𝟭 C)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : D
⊢ NatTrans.app
      (whiskerLeft e.inverse (unit e) ≫
        (Functor.associator e.inverse e.functor e.inverse).inv ≫ whiskerRight (counit e) e.inverse)
      x✝ =
    NatTrans.app (NatTrans.id (e.inverse ⋙ 𝟭 C)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : D
⊢ NatTrans.app (unit e) (e.inverse.obj x✝) ≫
      𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj x✝))) ≫ e.inverse.map (NatTrans.app (counit e) x✝) =
    𝟙 (e.inverse.obj x✝)
[PROOFSTEP]
simp only [id_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : D
⊢ NatTrans.app (unit e) (e.inverse.obj x✝) ≫ e.inverse.map (NatTrans.app (counit e) x✝) = 𝟙 (e.inverse.obj x✝)
[PROOFSTEP]
exact e.unit_inverse_comp _
