[GOAL]
I : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
x✝³ x✝² : C i
x✝¹ x✝ : x✝³ ⟶ x✝²
h : (incl i).map x✝¹ = (incl i).map x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
injection h
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : (i : I) → C i ⥤ D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ F ⟶ incl i ⋙ G
⊢ ∀ ⦃X Y : (i : I) × C i⦄ (f : X ⟶ Y),
    F.map f ≫
        (fun x =>
            match x with
            | { fst := j, snd := X } => NatTrans.app (h j) X)
          Y =
      (fun x =>
            match x with
            | { fst := j, snd := X } => NatTrans.app (h j) X)
          X ≫
        G.map f
[PROOFSTEP]
rintro ⟨j, X⟩ ⟨_, _⟩ ⟨f⟩
[GOAL]
case mk.mk.mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : (i : I) → C i ⥤ D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ F ⟶ incl i ⋙ G
j : I
X Y✝ : C j
f : X ⟶ Y✝
⊢ F.map (SigmaHom.mk f) ≫
      (fun x =>
          match x with
          | { fst := j, snd := X } => NatTrans.app (h j) X)
        { fst := j, snd := Y✝ } =
    (fun x =>
          match x with
          | { fst := j, snd := X } => NatTrans.app (h j) X)
        { fst := j, snd := X } ≫
      G.map (SigmaHom.mk f)
[PROOFSTEP]
apply (h j).naturality
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
⊢ ∀ (X : (i : I) × C i),
    { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (𝟙 X) =
      𝟙 ({ obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.obj X)
[PROOFSTEP]
rintro ⟨i, X⟩
[GOAL]
case mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
i : I
X : C i
⊢ { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (𝟙 { fst := i, snd := X }) =
    𝟙 ({ obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.obj { fst := i, snd := X })
[PROOFSTEP]
apply (F i).map_id
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
⊢ ∀ {X Y Z : (i : I) × C i} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (f ≫ g) =
      { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map f ≫
        { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map g
[PROOFSTEP]
rintro ⟨i, X⟩ ⟨_, Y⟩ ⟨_, Z⟩ ⟨f⟩ ⟨g⟩
[GOAL]
case mk.mk.mk.mk.mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
i : I
X Y✝¹ : C i
f : X ⟶ Y✝¹
Y✝ : C i
g : Y✝¹ ⟶ Y✝
⊢ { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk f ≫ SigmaHom.mk g) =
    { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk f) ≫
      { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk g)
[PROOFSTEP]
apply (F i).map_comp
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
q : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ q ≅ F i
⊢ ∀ {X Y : (i : I) × C i} (f : X ⟶ Y),
    q.map f ≫
        ((fun x =>
              match x with
              | { fst := i, snd := X } => (h i).app X)
            Y).hom =
      ((fun x =>
              match x with
              | { fst := i, snd := X } => (h i).app X)
            X).hom ≫
        (desc F).map f
[PROOFSTEP]
rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
[GOAL]
case mk.mk.mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
q : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ q ≅ F i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ q.map (SigmaHom.mk f) ≫
      ((fun x =>
            match x with
            | { fst := i, snd := X } => (h i).app X)
          { fst := i, snd := Y✝ }).hom =
    ((fun x =>
            match x with
            | { fst := i, snd := X } => (h i).app X)
          { fst := i, snd := X }).hom ≫
      (desc F).map (SigmaHom.mk f)
[PROOFSTEP]
apply (h i).hom.naturality f
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
⊢ ∀ ⦃X Y : (i : I) × C i⦄ (f : X ⟶ Y),
    (Functor.sigma F).map f ≫ (fun f => SigmaHom.mk (NatTrans.app (α f.fst) f.snd)) Y =
      (fun f => SigmaHom.mk (NatTrans.app (α f.fst) f.snd)) X ≫ (Functor.sigma G).map f
[PROOFSTEP]
rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
[GOAL]
case mk.mk.mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ (Functor.sigma F).map (SigmaHom.mk f) ≫
      (fun f => SigmaHom.mk (NatTrans.app (α f.fst) f.snd)) { fst := i, snd := Y✝ } =
    (fun f => SigmaHom.mk (NatTrans.app (α f.fst) f.snd)) { fst := i, snd := X } ≫ (Functor.sigma G).map (SigmaHom.mk f)
[PROOFSTEP]
change SigmaHom.mk _ = SigmaHom.mk _
[GOAL]
case mk.mk.mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ SigmaHom.mk
      ((F { fst := i, snd := X }.fst).map f ≫
        NatTrans.app (α { fst := i, snd := Y✝ }.fst) { fst := i, snd := Y✝ }.snd) =
    SigmaHom.mk
      (NatTrans.app (α { fst := i, snd := X }.fst) { fst := i, snd := X }.snd ≫ (G { fst := i, snd := X }.fst).map f)
[PROOFSTEP]
rw [(α i).naturality]


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ NatTrans.app (counitInv e) (e.functor.obj X) ≫ e.functor.map (NatTrans.app (unitInv e) X) = 𝟙 (e.functor.obj X)
[PROOFSTEP]
erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)) (Iso.refl _)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)).hom =
    (Iso.refl (e.functor.obj ((𝟭 C).obj X))).hom
[PROOFSTEP]
exact e.functor_unit_comp X
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ NatTrans.app (counitInv e) (e.functor.obj X) = e.functor.map (NatTrans.app (unit e) X)
[PROOFSTEP]
symm
[GOAL]
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 (counitInv e) (e.functor.obj X)
[PROOFSTEP]
erw [← Iso.comp_hom_eq_id (e.counitIso.app _), functor_unit_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 ((𝟭 D).obj (e.functor.toPrefunctor.1 ((𝟭 C).obj X)))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ NatTrans.app (counit e) (e.functor.obj X) = e.functor.map (NatTrans.app (unitInv e) X)
[PROOFSTEP]
erw [← Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)), functor_unit_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 (e.functor.obj ((𝟭 C).obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) (e.inverse.obj Y) ≫ e.inverse.map (NatTrans.app (counit e) Y) = 𝟙 (e.inverse.obj Y)
[PROOFSTEP]
rw [← id_comp (e.inverse.map _), ← map_id e.inverse, ← counitInv_functor_comp, map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) (e.inverse.obj Y) ≫
      (e.inverse.map (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))) ≫
          e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
        e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) (e.inverse.obj Y) ≫
      (e.inverse.map (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))) ≫
          e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
        e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
rw [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), app_hom, app_inv]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) (e.inverse.obj Y) ≫
      (e.inverse.map (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))) ≫
          NatTrans.app e.unitIso.hom
              (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
            NatTrans.app e.unitIso.inv
                (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
              e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
        e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 2 3 => erw [e.unit.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))) ≫
    NatTrans.app e.unitIso.hom
      (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) (e.inverse.obj Y)
[PROOFSTEP]
erw [e.unit.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))) ≫
    NatTrans.app e.unitIso.hom
      (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) (e.inverse.obj Y)
[PROOFSTEP]
erw [e.unit.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))) ≫
    NatTrans.app e.unitIso.hom
      (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) (e.inverse.obj Y)
[PROOFSTEP]
erw [e.unit.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) (e.inverse.obj Y) ≫
      (((NatTrans.app (unit e) (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y))) ≫
              (e.functor ⋙ e.inverse).map
                (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))) ≫
            NatTrans.app e.unitIso.inv
              (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
        e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 1 2 => erw [e.unit.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) (e.inverse.obj Y) ≫
    NatTrans.app (unit e) (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
[PROOFSTEP]
erw [e.unit.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) (e.inverse.obj Y) ≫
    NatTrans.app (unit e) (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
[PROOFSTEP]
erw [e.unit.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) (e.inverse.obj Y) ≫
    NatTrans.app (unit e) (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
[PROOFSTEP]
erw [e.unit.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ ((((NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
              (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y))) ≫
            (e.functor ⋙ e.inverse).map
              (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))) ≫
          NatTrans.app e.unitIso.inv
            (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
        e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
      e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 4 4 => rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
[GOAL]
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))
[PROOFSTEP]
rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
[GOAL]
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))
[PROOFSTEP]
rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
[GOAL]
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app e.unitIso.inv
    (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))
[PROOFSTEP]
rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y)) ≫
        (e.functor ⋙ e.inverse).map
            (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y)))) ≫
          (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom ≫
                (e.inverse.mapIso
                      (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
                  NatTrans.app (unitInv e)
                    (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
              e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
            e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 3 4 =>
  erw [← map_comp e.inverse, e.counit.naturality]
  erw [(e.counitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map
      (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y)))) ≫
    (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y))
[PROOFSTEP]
  erw [← map_comp e.inverse, e.counit.naturality]
  erw [(e.counitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map
      (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y)))) ≫
    (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y))
[PROOFSTEP]
  erw [← map_comp e.inverse, e.counit.naturality]
  erw [(e.counitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map
      (e.inverse.toPrefunctor.2 (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y)))) ≫
    (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y))
[PROOFSTEP]
erw [← map_comp e.inverse, e.counit.naturality]
[GOAL]
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map
    (NatTrans.app (counit e) (e.functor.obj (e.inverse.obj Y)) ≫
      (𝟭 D).map (NatTrans.app (counitInv e) (e.functor.obj (e.inverse.obj Y))))
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv
case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y))
[PROOFSTEP]
erw [(e.counitIso.app _).hom_inv_id, map_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y)) ≫
        (((𝟙 (e.inverse.obj (e.functor.obj (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y))))) ≫
                (e.inverse.mapIso
                    (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv) ≫
              NatTrans.app (unitInv e)
                (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
            e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
          e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
erw [id_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y)) ≫
        (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
              NatTrans.app (unitInv e)
                (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
            e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
          e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 2 3 => erw [← map_comp e.inverse, e.counitIso.inv.naturality, map_comp]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y)) ≫
    (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
[PROOFSTEP]
erw [← map_comp e.inverse, e.counitIso.inv.naturality, map_comp]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y)) ≫
    (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
[PROOFSTEP]
erw [← map_comp e.inverse, e.counitIso.inv.naturality, map_comp]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.functor ⋙ e.inverse).map ((unit e).1 (e.inverse.obj Y)) ≫
    (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
[PROOFSTEP]
erw [← map_comp e.inverse, e.counitIso.inv.naturality, map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      (((e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
              e.inverse.map ((e.inverse ⋙ e.functor).map (e.functor.toPrefunctor.2 ((unit e).1 (e.inverse.obj Y))))) ≫
            NatTrans.app (unitInv e)
              (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
        e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 3 4 => erw [e.unitInv.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map ((e.inverse ⋙ e.functor).map (e.functor.toPrefunctor.2 ((unit e).1 (e.inverse.obj Y)))) ≫
    NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [e.unitInv.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map ((e.inverse ⋙ e.functor).map (e.functor.toPrefunctor.2 ((unit e).1 (e.inverse.obj Y)))) ≫
    NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [e.unitInv.naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map ((e.inverse ⋙ e.functor).map (e.functor.toPrefunctor.2 ((unit e).1 (e.inverse.obj Y)))) ≫
    NatTrans.app (unitInv e) (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [e.unitInv.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        ((NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
              (𝟭 C).map (e.inverse.map (e.functor.toPrefunctor.2 ((unit e).1 (e.inverse.obj Y))))) ≫
            e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))) ≫
          e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 4 5 => erw [← map_comp (e.functor ⋙ e.inverse), (e.unitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (𝟭 C).map (e.inverse.map (e.functor.toPrefunctor.2 ((unit e).1 (e.inverse.obj Y)))) ≫
    e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [← map_comp (e.functor ⋙ e.inverse), (e.unitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (𝟭 C).map (e.inverse.map (e.functor.toPrefunctor.2 ((unit e).1 (e.inverse.obj Y)))) ≫
    e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [← map_comp (e.functor ⋙ e.inverse), (e.unitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (𝟭 C).map (e.inverse.map (e.functor.toPrefunctor.2 ((unit e).1 (e.inverse.obj Y)))) ≫
    e.inverse.map (e.functor.map (NatTrans.app (unitInv e) (e.inverse.obj Y)))
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [← map_comp (e.functor ⋙ e.inverse), (e.unitIso.app _).hom_inv_id, map_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
          𝟙 ((e.functor ⋙ e.inverse).obj ((𝟭 C).obj (e.inverse.obj Y))) ≫ e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
erw [id_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
          e.inverse.map (NatTrans.app (counit e) Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 3 4 => erw [← e.unitInv.naturality]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
    e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [← e.unitInv.naturality]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
    e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [← e.unitInv.naturality]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
    e.inverse.map (NatTrans.app (counit e) Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y))))
[PROOFSTEP]
erw [← e.unitInv.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counit e) Y)) ≫
          NatTrans.app (unitInv e) (e.inverse.toPrefunctor.1 Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
slice_lhs 2 3 => erw [← map_comp e.inverse, ← e.counitIso.inv.naturality, (e.counitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
    (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counit e) Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.toPrefunctor.1 Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
[PROOFSTEP]
erw [← map_comp e.inverse, ← e.counitIso.inv.naturality, (e.counitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
    (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counit e) Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.toPrefunctor.1 Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
[PROOFSTEP]
erw [← map_comp e.inverse, ← e.counitIso.inv.naturality, (e.counitIso.app _).hom_inv_id, map_id]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (NatTrans.app e.counitIso.inv (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫
    (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (NatTrans.app (counit e) Y))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unitInv e) (e.inverse.toPrefunctor.1 Y)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y))
[PROOFSTEP]
erw [← map_comp e.inverse, ← e.counitIso.inv.naturality, (e.counitIso.app _).hom_inv_id, map_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) ((𝟭 C).obj (e.inverse.obj Y)) ≫
      𝟙 (e.inverse.obj (e.functor.obj ((𝟭 C).obj (e.inverse.obj Y)))) ≫
        NatTrans.app (unitInv e) (e.inverse.toPrefunctor.1 Y) =
    𝟙 (e.inverse.obj Y)
[PROOFSTEP]
erw [id_comp, (e.unitIso.app _).hom_inv_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ 𝟙 ((𝟭 C).obj ((𝟭 C).obj (e.inverse.obj Y))) = 𝟙 (e.inverse.obj Y)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.inverse.map (NatTrans.app (counitInv e) Y) ≫ NatTrans.app (unitInv e) (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y)
[PROOFSTEP]
erw [Iso.inv_eq_inv (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y)) (Iso.refl _)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y)).hom =
    (Iso.refl ((𝟭 C).obj (e.inverse.obj Y))).hom
[PROOFSTEP]
exact e.unit_inverse_comp Y
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unit e) (e.inverse.obj Y) = e.inverse.map (NatTrans.app (counitInv e) Y)
[PROOFSTEP]
erw [← Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)), unit_inverse_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 (e.inverse.obj ((𝟭 D).obj Y))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ NatTrans.app (unitInv e) (e.inverse.obj Y) = e.inverse.map (NatTrans.app (counit e) Y)
[PROOFSTEP]
symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.inverse.map (NatTrans.app (counit e) Y) = NatTrans.app (unitInv e) (e.inverse.obj Y)
[PROOFSTEP]
erw [← Iso.hom_comp_eq_id (e.unitIso.app _), unit_inverse_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 ((𝟭 C).obj (e.inverse.obj Y))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
⊢ 𝟭 C ≅ F ⋙ G
[PROOFSTEP]
calc
  𝟭 C ≅ F ⋙ G := η
  _ ≅ F ⋙ 𝟭 D ⋙ G := (isoWhiskerLeft F (leftUnitor G).symm)
  _ ≅ F ⋙ (G ⋙ F) ⋙ G := (isoWhiskerLeft F (isoWhiskerRight ε.symm G))
  _ ≅ F ⋙ G ⋙ F ⋙ G := (isoWhiskerLeft F (associator G F G))
  _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm
  _ ≅ 𝟭 C ⋙ F ⋙ G := (isoWhiskerRight η.symm (F ⋙ G))
  _ ≅ F ⋙ G := leftUnitor (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
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (NatTrans.app (adjointifyη η ε).hom X) ≫ NatTrans.app ε.hom (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
dsimp [adjointifyη, Trans.trans]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map
        ((((((NatTrans.app η.hom X ≫ 𝟙 (G.obj (F.obj X))) ≫ G.map (NatTrans.app ε.inv (F.obj X))) ≫
                𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫
              𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫
            G.map (F.map (NatTrans.app η.inv X))) ≫
          𝟙 (G.obj (F.obj X))) ≫
      NatTrans.app ε.hom (F.obj X) =
    𝟙 (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
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (NatTrans.app η.hom X) ≫
      F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫
        F.map (G.map (F.map (NatTrans.app η.inv X))) ≫ NatTrans.app ε.hom (F.obj X) =
    𝟙 (F.obj X)
[PROOFSTEP]
have := ε.hom.naturality (F.map (η.inv.app X))
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  (G ⋙ F).map (F.map (NatTrans.app η.inv X)) ≫ NatTrans.app ε.hom (F.obj ((𝟭 C).obj X)) =
    NatTrans.app ε.hom (F.obj ((F ⋙ G).obj X)) ≫ (𝟭 D).map (F.map (NatTrans.app η.inv X))
⊢ F.map (NatTrans.app η.hom X) ≫
      F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫
        F.map (G.map (F.map (NatTrans.app η.inv X))) ≫ NatTrans.app ε.hom (F.obj X) =
    𝟙 (F.obj X)
[PROOFSTEP]
dsimp at this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (NatTrans.app η.inv X))) ≫ NatTrans.app ε.hom (F.obj X) =
    NatTrans.app ε.hom (F.obj (G.obj (F.obj X))) ≫ F.map (NatTrans.app η.inv X)
⊢ F.map (NatTrans.app η.hom X) ≫
      F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫
        F.map (G.map (F.map (NatTrans.app η.inv X))) ≫ NatTrans.app ε.hom (F.obj X) =
    𝟙 (F.obj X)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (NatTrans.app η.inv X))) ≫ NatTrans.app ε.hom (F.obj X) =
    NatTrans.app ε.hom (F.obj (G.obj (F.obj X))) ≫ F.map (NatTrans.app η.inv X)
⊢ F.map (NatTrans.app η.hom X) ≫
      F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫
        NatTrans.app ε.hom (F.obj (G.obj (F.obj X))) ≫ F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
clear this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (NatTrans.app η.hom X) ≫
      F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫
        NatTrans.app ε.hom (F.obj (G.obj (F.obj X))) ≫ F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
rw [← assoc _ _ (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
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (NatTrans.app η.hom X) ≫
      (F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫ NatTrans.app ε.hom (F.obj (G.obj (F.obj X)))) ≫
        F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
have := ε.hom.naturality (ε.inv.app <| F.obj X)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  (G ⋙ F).map (NatTrans.app ε.inv (F.obj X)) ≫ NatTrans.app ε.hom ((G ⋙ F).obj (F.obj X)) =
    NatTrans.app ε.hom ((𝟭 D).obj (F.obj X)) ≫ (𝟭 D).map (NatTrans.app ε.inv (F.obj X))
⊢ F.map (NatTrans.app η.hom X) ≫
      (F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫ NatTrans.app ε.hom (F.obj (G.obj (F.obj X)))) ≫
        F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
dsimp at this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫ NatTrans.app ε.hom (F.obj (G.obj (F.obj X))) =
    NatTrans.app ε.hom (F.obj X) ≫ NatTrans.app ε.inv (F.obj X)
⊢ F.map (NatTrans.app η.hom X) ≫
      (F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫ NatTrans.app ε.hom (F.obj (G.obj (F.obj X)))) ≫
        F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (NatTrans.app ε.inv (F.obj X))) ≫ NatTrans.app ε.hom (F.obj (G.obj (F.obj X))) =
    NatTrans.app ε.hom (F.obj X) ≫ NatTrans.app ε.inv (F.obj X)
⊢ F.map (NatTrans.app η.hom X) ≫
      (NatTrans.app ε.hom (F.obj X) ≫ NatTrans.app ε.inv (F.obj X)) ≫ F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
clear this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (NatTrans.app η.hom X) ≫
      (NatTrans.app ε.hom (F.obj X) ≫ NatTrans.app ε.inv (F.obj X)) ≫ F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
have := (ε.app <| F.obj X).hom_inv_id
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : (ε.app (F.obj X)).hom ≫ (ε.app (F.obj X)).inv = 𝟙 ((G ⋙ F).obj (F.obj X))
⊢ F.map (NatTrans.app η.hom X) ≫
      (NatTrans.app ε.hom (F.obj X) ≫ NatTrans.app ε.inv (F.obj X)) ≫ F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
dsimp at this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : NatTrans.app ε.hom (F.obj X) ≫ NatTrans.app ε.inv (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (NatTrans.app η.hom X) ≫
      (NatTrans.app ε.hom (F.obj X) ≫ NatTrans.app ε.inv (F.obj X)) ≫ F.map (NatTrans.app η.inv X) =
    𝟙 (F.obj X)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : NatTrans.app ε.hom (F.obj X) ≫ NatTrans.app ε.inv (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (NatTrans.app η.hom X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (NatTrans.app η.inv X) = 𝟙 (F.obj X)
[PROOFSTEP]
clear this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (NatTrans.app η.hom X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (NatTrans.app η.inv X) = 𝟙 (F.obj X)
[PROOFSTEP]
rw [id_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (NatTrans.app η.hom X) ≫ F.map (NatTrans.app η.inv X) = 𝟙 (F.obj X)
[PROOFSTEP]
have := (F.mapIso <| η.app X).hom_inv_id
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : (F.mapIso (η.app X)).hom ≫ (F.mapIso (η.app X)).inv = 𝟙 (F.obj ((𝟭 C).obj X))
⊢ F.map (NatTrans.app η.hom X) ≫ F.map (NatTrans.app η.inv X) = 𝟙 (F.obj X)
[PROOFSTEP]
dsimp at this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : F.map (NatTrans.app η.hom X) ≫ F.map (NatTrans.app η.inv X) = 𝟙 (F.obj X)
⊢ F.map (NatTrans.app η.hom X) ≫ F.map (NatTrans.app η.inv X) = 𝟙 (F.obj X)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
⊢ 𝟭 C ≅ (e.functor ⋙ f.functor) ⋙ f.inverse ⋙ e.inverse
[PROOFSTEP]
refine' Iso.trans e.unitIso _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
⊢ e.functor ⋙ e.inverse ≅ (e.functor ⋙ f.functor) ⋙ f.inverse ⋙ e.inverse
[PROOFSTEP]
exact isoWhiskerLeft e.functor (isoWhiskerRight f.unitIso e.inverse)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
⊢ (f.inverse ⋙ e.inverse) ⋙ e.functor ⋙ f.functor ≅ 𝟭 E
[PROOFSTEP]
refine' Iso.trans _ f.counitIso
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
⊢ (f.inverse ⋙ e.inverse) ⋙ e.functor ⋙ f.functor ≅ f.inverse ⋙ f.functor
[PROOFSTEP]
exact
  isoWhiskerLeft f.inverse
    (isoWhiskerRight e.counitIso f.functor)
      -- We wouldn't have needed to give this proof if we'd used `Equivalence.mk`,
        -- but we choose to avoid using that here, for the sake of good structure projection `simp`
        -- lemmas.
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
X : C
⊢ (e.functor ⋙ f.functor).map
        (NatTrans.app (e.unitIso ≪≫ isoWhiskerLeft e.functor (isoWhiskerRight f.unitIso e.inverse)).hom X) ≫
      NatTrans.app (isoWhiskerLeft f.inverse (isoWhiskerRight e.counitIso f.functor) ≪≫ f.counitIso).hom
        ((e.functor ⋙ f.functor).obj X) =
    𝟙 ((e.functor ⋙ f.functor).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
X : C
⊢ f.functor.map
        (e.functor.map (NatTrans.app e.unitIso.hom X ≫ e.inverse.map (NatTrans.app f.unitIso.hom (e.functor.obj X)))) ≫
      f.functor.map (NatTrans.app e.counitIso.hom (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
        NatTrans.app f.counitIso.hom (f.functor.obj (e.functor.obj X)) =
    𝟙 (f.functor.obj (e.functor.obj X))
[PROOFSTEP]
rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counitInv_app_functor, fun_inv_map, Iso.inv_hom_id_app_assoc,
  assoc, Iso.inv_hom_id_app, counit_app_functor, ← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
X : C
⊢ f.functor.map
      ((NatTrans.app f.unitIso.hom (e.functor.obj X) ≫
          𝟙 ((𝟭 D).obj (f.inverse.obj (f.functor.obj (e.functor.obj X))))) ≫
        NatTrans.app (unitInv f) (e.functor.obj X)) =
    𝟙 (f.functor.obj (e.functor.obj X))
[PROOFSTEP]
erw [comp_id, Iso.hom_inv_id_app, Functor.map_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ NatTrans.app (funInvIdAssoc e F).hom X = F.map (NatTrans.app (unitInv e) X)
[PROOFSTEP]
dsimp [funInvIdAssoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ 𝟙 (F.obj (e.inverse.obj (e.functor.obj X))) ≫ F.map (NatTrans.app e.unitIso.inv X) ≫ 𝟙 (F.obj X) =
    F.map (NatTrans.app (unitInv e) X)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ NatTrans.app (funInvIdAssoc e F).inv X = F.map (NatTrans.app (unit e) X)
[PROOFSTEP]
dsimp [funInvIdAssoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ (𝟙 (F.obj X) ≫ F.map (NatTrans.app e.unitIso.hom X)) ≫ 𝟙 (F.obj (e.inverse.obj (e.functor.obj X))) =
    F.map (NatTrans.app (unit e) X)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ NatTrans.app (invFunIdAssoc e F).hom X = F.map (NatTrans.app (counit e) X)
[PROOFSTEP]
dsimp [invFunIdAssoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ 𝟙 (F.obj (e.functor.obj (e.inverse.obj X))) ≫ F.map (NatTrans.app e.counitIso.hom X) ≫ 𝟙 (F.obj X) =
    F.map (NatTrans.app (counit e) X)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ NatTrans.app (invFunIdAssoc e F).inv X = F.map (NatTrans.app (counitInv e) X)
[PROOFSTEP]
dsimp [invFunIdAssoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ (𝟙 (F.obj X) ≫ F.map (NatTrans.app e.counitIso.inv X)) ≫ 𝟙 (F.obj (e.functor.obj (e.inverse.obj X))) =
    F.map (NatTrans.app (counitInv e) X)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
X Y : C
f f' : X ⟶ Y
⊢ f ≫ NatTrans.app (unit e) Y = f' ≫ NatTrans.app (unit e) Y ↔ f = f'
[PROOFSTEP]
simp only [cancel_mono]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
X Y : C
f f' : X ⟶ e.inverse.obj (e.functor.obj Y)
⊢ f ≫ NatTrans.app (unitInv e) Y = f' ≫ NatTrans.app (unitInv e) Y ↔ f = f'
[PROOFSTEP]
simp only [cancel_mono]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
X Y : D
f f' : X ⟶ e.functor.obj (e.inverse.obj Y)
⊢ f ≫ NatTrans.app (counit e) Y = f' ≫ NatTrans.app (counit e) Y ↔ f = f'
[PROOFSTEP]
simp only [cancel_mono]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
X Y : D
f f' : X ⟶ Y
⊢ f ≫ NatTrans.app (counitInv e) Y = f' ≫ NatTrans.app (counitInv e) Y ↔ f = f'
[PROOFSTEP]
simp only [cancel_mono]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
W X X' Y : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
⊢ f ≫ g ≫ NatTrans.app (unit e) Y = f' ≫ g' ≫ NatTrans.app (unit e) Y ↔ f ≫ g = f' ≫ g'
[PROOFSTEP]
simp only [← Category.assoc, cancel_mono]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
W X X' Y : D
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
⊢ f ≫ g ≫ NatTrans.app (counitInv e) Y = f' ≫ g' ≫ NatTrans.app (counitInv e) Y ↔ f ≫ g = f' ≫ g'
[PROOFSTEP]
simp only [← Category.assoc, cancel_mono]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
W X X' Y Y' Z : C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ NatTrans.app (unit e) Z = f' ≫ g' ≫ h' ≫ NatTrans.app (unit e) Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'
[PROOFSTEP]
simp only [← Category.assoc, cancel_mono]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
W X X' Y Y' Z : D
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ NatTrans.app (counitInv e) Z = f' ≫ g' ≫ h' ≫ NatTrans.app (counitInv e) Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'
[PROOFSTEP]
simp only [← Category.assoc, cancel_mono]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
E : C ≌ D
⊢ asEquivalence E.functor = E
[PROOFSTEP]
cases E
[GOAL]
case mk'
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
functor✝ : C ⥤ D
inverse✝ : D ⥤ C
unitIso✝ : 𝟭 C ≅ functor✝ ⋙ inverse✝
counitIso✝ : inverse✝ ⋙ functor✝ ≅ 𝟭 D
functor_unitIso_comp✝ :
  ∀ (X : C),
    functor✝.map (NatTrans.app unitIso✝.hom X) ≫ NatTrans.app counitIso✝.hom (functor✝.obj X) = 𝟙 (functor✝.obj X)
⊢ asEquivalence (mk' functor✝ inverse✝ unitIso✝ counitIso✝).functor = mk' functor✝ inverse✝ unitIso✝ counitIso✝
[PROOFSTEP]
congr
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
E : C ≌ D
⊢ asEquivalence E.inverse = symm E
[PROOFSTEP]
cases E
[GOAL]
case mk'
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
functor✝ : C ⥤ D
inverse✝ : D ⥤ C
unitIso✝ : 𝟭 C ≅ functor✝ ⋙ inverse✝
counitIso✝ : inverse✝ ⋙ functor✝ ≅ 𝟭 D
functor_unitIso_comp✝ :
  ∀ (X : C),
    functor✝.map (NatTrans.app unitIso✝.hom X) ≫ NatTrans.app counitIso✝.hom (functor✝.obj X) = 𝟙 (functor✝.obj X)
⊢ asEquivalence (mk' functor✝ inverse✝ unitIso✝ counitIso✝).inverse = symm (mk' functor✝ inverse✝ unitIso✝ counitIso✝)
[PROOFSTEP]
congr
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : D
f : X ⟶ Y
⊢ F.map ((Functor.inv F).map f) =
    NatTrans.app (Equivalence.counit (asEquivalence F)) X ≫ f ≫ NatTrans.app (Equivalence.counitInv (asEquivalence F)) Y
[PROOFSTEP]
erw [NatIso.naturality_2]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : D
f : X ⟶ Y
⊢ F.map ((Functor.inv F).map f) = ((asEquivalence F).inverse ⋙ (asEquivalence F).functor).map f
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
⊢ (Functor.inv F).map (F.map f) =
    NatTrans.app (Equivalence.unitInv (asEquivalence F)) X ≫ f ≫ NatTrans.app (Equivalence.unit (asEquivalence F)) Y
[PROOFSTEP]
erw [NatIso.naturality_1]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
⊢ (Functor.inv F).map (F.map f) = ((asEquivalence F).functor ⋙ (asEquivalence F).inverse).map f
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ G.map (NatTrans.app (unitIso ≪≫ hcomp e (Iso.refl (inverse F))).hom X) ≫
      NatTrans.app (hcomp (Iso.refl (inverse F)) e.symm ≪≫ counitIso).hom (G.obj X) =
    𝟙 (G.obj X)
[PROOFSTEP]
dsimp [NatIso.hcomp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ G.map (NatTrans.app unitIso.hom X ≫ 𝟙 ((inverse F).obj (F.obj X)) ≫ (inverse F).map (NatTrans.app e.hom X)) ≫
      (NatTrans.app e.inv ((inverse F).obj (G.obj X)) ≫ F.map (𝟙 ((inverse F).obj (G.obj X)))) ≫
        NatTrans.app counitIso.hom (G.obj X) =
    𝟙 (G.obj X)
[PROOFSTEP]
erw [id_comp, F.map_id, comp_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ G.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X)) ≫
      NatTrans.app e.inv ((inverse F).obj (G.obj X)) ≫ NatTrans.app counitIso.hom (G.obj X) =
    𝟙 (G.obj X)
[PROOFSTEP]
apply (cancel_epi (e.hom.app X)).mp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ NatTrans.app e.hom X ≫
      G.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X)) ≫
        NatTrans.app e.inv ((inverse F).obj (G.obj X)) ≫ NatTrans.app counitIso.hom (G.obj X) =
    NatTrans.app e.hom X ≫ 𝟙 (G.obj X)
[PROOFSTEP]
slice_lhs 1 2 => rw [← e.hom.naturality]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.hom X ≫ G.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.inv ((inverse F).obj (G.obj X))
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app counitIso.hom (G.obj X)
[PROOFSTEP]
rw [← e.hom.naturality]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.hom X ≫ G.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.inv ((inverse F).obj (G.obj X))
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app counitIso.hom (G.obj X)
[PROOFSTEP]
rw [← e.hom.naturality]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.hom X ≫ G.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.inv ((inverse F).obj (G.obj X))
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app counitIso.hom (G.obj X)
[PROOFSTEP]
rw [← e.hom.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ ((F.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X)) ≫
          NatTrans.app e.hom ((inverse F).obj (G.obj X))) ≫
        NatTrans.app e.inv ((inverse F).obj (G.obj X))) ≫
      NatTrans.app counitIso.hom (G.obj X) =
    NatTrans.app e.hom X ≫ 𝟙 (G.obj X)
[PROOFSTEP]
slice_lhs 2 3 => rw [← NatTrans.vcomp_app', e.hom_inv_id]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.hom ((inverse F).obj (G.obj X)) ≫ NatTrans.app e.inv ((inverse F).obj (G.obj X))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app counitIso.hom (G.obj X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| F.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X))
[PROOFSTEP]
rw [← NatTrans.vcomp_app', e.hom_inv_id]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.hom ((inverse F).obj (G.obj X)) ≫ NatTrans.app e.inv ((inverse F).obj (G.obj X))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app counitIso.hom (G.obj X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| F.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X))
[PROOFSTEP]
rw [← NatTrans.vcomp_app', e.hom_inv_id]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app e.hom ((inverse F).obj (G.obj X)) ≫ NatTrans.app e.inv ((inverse F).obj (G.obj X))
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| NatTrans.app counitIso.hom (G.obj X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| F.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X))
[PROOFSTEP]
rw [← NatTrans.vcomp_app', e.hom_inv_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ F.map (NatTrans.app unitIso.hom X ≫ (inverse F).map (NatTrans.app e.hom X)) ≫
      NatTrans.app (𝟙 F) ((inverse F).obj (G.obj X)) ≫ NatTrans.app counitIso.hom (G.obj X) =
    NatTrans.app e.hom X ≫ 𝟙 (G.obj X)
[PROOFSTEP]
simp only [NatTrans.id_app, id_comp, comp_id, F.map_comp, assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ F.map (NatTrans.app unitIso.hom X) ≫
      F.map ((inverse F).map (NatTrans.app e.hom X)) ≫ NatTrans.app counitIso.hom (G.obj X) =
    NatTrans.app e.hom X
[PROOFSTEP]
erw [hF.counitIso.hom.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ F.map (NatTrans.app unitIso.hom X) ≫ NatTrans.app counitIso.hom (F.obj X) ≫ (𝟭 D).map (NatTrans.app e.hom X) =
    NatTrans.app e.hom X
[PROOFSTEP]
slice_lhs 1 2 => rw [functor_unitIso_comp]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| F.map (NatTrans.app unitIso.hom X) ≫ NatTrans.app counitIso.hom (F.obj X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| (𝟭 D).map (NatTrans.app e.hom X)
[PROOFSTEP]
rw [functor_unitIso_comp]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| F.map (NatTrans.app unitIso.hom X) ≫ NatTrans.app counitIso.hom (F.obj X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| (𝟭 D).map (NatTrans.app e.hom X)
[PROOFSTEP]
rw [functor_unitIso_comp]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| F.map (NatTrans.app unitIso.hom X) ≫ NatTrans.app counitIso.hom (F.obj X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
| (𝟭 D).map (NatTrans.app e.hom X)
[PROOFSTEP]
rw [functor_unitIso_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
X : C
⊢ 𝟙 (F.obj X) ≫ (𝟭 D).map (NatTrans.app e.hom X) = NatTrans.app e.hom X
[PROOFSTEP]
simp only [Functor.id_map, id_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
⊢ ofIso e' (ofIso e hF) = ofIso (e ≪≫ e') hF
[PROOFSTEP]
dsimp [ofIso]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
⊢ mk' (inverse F) ((unitIso ≪≫ hcomp e (Iso.refl (inverse F))) ≪≫ hcomp e' (Iso.refl (inverse F)))
      (hcomp (Iso.refl (inverse F)) e'.symm ≪≫ hcomp (Iso.refl (inverse F)) e.symm ≪≫ counitIso) =
    mk' (inverse F) (unitIso ≪≫ hcomp (e ≪≫ e') (Iso.refl (inverse F)))
      (hcomp (Iso.refl (inverse F)) (e'.symm ≪≫ e.symm) ≪≫ counitIso)
[PROOFSTEP]
congr 1
[GOAL]
case e_unitIso
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
⊢ (unitIso ≪≫ hcomp e (Iso.refl (inverse F))) ≪≫ hcomp e' (Iso.refl (inverse F)) =
    unitIso ≪≫ hcomp (e ≪≫ e') (Iso.refl (inverse F))
[PROOFSTEP]
ext X
[GOAL]
case e_counitIso
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
⊢ hcomp (Iso.refl (inverse F)) e'.symm ≪≫ hcomp (Iso.refl (inverse F)) e.symm ≪≫ counitIso =
    hcomp (Iso.refl (inverse F)) (e'.symm ≪≫ e.symm) ≪≫ counitIso
[PROOFSTEP]
ext X
[GOAL]
case e_unitIso.w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
X : C
⊢ NatTrans.app ((unitIso ≪≫ hcomp e (Iso.refl (inverse F))) ≪≫ hcomp e' (Iso.refl (inverse F))).hom X =
    NatTrans.app (unitIso ≪≫ hcomp (e ≪≫ e') (Iso.refl (inverse F))).hom X
[PROOFSTEP]
dsimp [NatIso.hcomp]
[GOAL]
case e_counitIso.w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
X : D
⊢ NatTrans.app (hcomp (Iso.refl (inverse F)) e'.symm ≪≫ hcomp (Iso.refl (inverse F)) e.symm ≪≫ counitIso).hom X =
    NatTrans.app (hcomp (Iso.refl (inverse F)) (e'.symm ≪≫ e.symm) ≪≫ counitIso).hom X
[PROOFSTEP]
dsimp [NatIso.hcomp]
[GOAL]
case e_unitIso.w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
X : C
⊢ (NatTrans.app unitIso.hom X ≫ 𝟙 ((inverse F).obj (F.obj X)) ≫ (inverse F).map (NatTrans.app e.hom X)) ≫
      𝟙 ((inverse F).obj (G.obj X)) ≫ (inverse F).map (NatTrans.app e'.hom X) =
    NatTrans.app unitIso.hom X ≫
      𝟙 ((inverse F).obj (F.obj X)) ≫ (inverse F).map (NatTrans.app e.hom X ≫ NatTrans.app e'.hom X)
[PROOFSTEP]
simp only [id_comp, assoc, Functor.map_comp]
[GOAL]
case e_counitIso.w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ D
e : F ≅ G
e' : G ≅ H
hF : IsEquivalence F
X : D
⊢ (NatTrans.app e'.inv ((inverse F).obj X) ≫ G.map (𝟙 ((inverse F).obj X))) ≫
      (NatTrans.app e.inv ((inverse F).obj X) ≫ F.map (𝟙 ((inverse F).obj X))) ≫ NatTrans.app counitIso.hom X =
    ((NatTrans.app e'.inv ((inverse F).obj X) ≫ NatTrans.app e.inv ((inverse F).obj X)) ≫
        F.map (𝟙 ((inverse F).obj X))) ≫
      NatTrans.app counitIso.hom X
[PROOFSTEP]
simp only [Functor.map_id, comp_id, id_comp, assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : IsEquivalence F
⊢ ofIso (Iso.refl F) hF = hF
[PROOFSTEP]
rcases hF with ⟨Finv, Funit, Fcounit, Fcomp⟩
[GOAL]
case mk'
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (NatTrans.app Funit.hom X) ≫ NatTrans.app Fcounit.hom (F.obj X) = 𝟙 (F.obj X)
⊢ ofIso (Iso.refl F) (mk' Finv Funit Fcounit) = mk' Finv Funit Fcounit
[PROOFSTEP]
dsimp [ofIso]
[GOAL]
case mk'
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (NatTrans.app Funit.hom X) ≫ NatTrans.app Fcounit.hom (F.obj X) = 𝟙 (F.obj X)
⊢ mk' Finv (Funit ≪≫ hcomp (Iso.refl F) (Iso.refl Finv)) (hcomp (Iso.refl Finv) (Iso.refl F) ≪≫ Fcounit) =
    mk' Finv Funit Fcounit
[PROOFSTEP]
congr 1
[GOAL]
case mk'.e_unitIso
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (NatTrans.app Funit.hom X) ≫ NatTrans.app Fcounit.hom (F.obj X) = 𝟙 (F.obj X)
⊢ Funit ≪≫ hcomp (Iso.refl F) (Iso.refl Finv) = Funit
[PROOFSTEP]
ext X
[GOAL]
case mk'.e_counitIso
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (NatTrans.app Funit.hom X) ≫ NatTrans.app Fcounit.hom (F.obj X) = 𝟙 (F.obj X)
⊢ hcomp (Iso.refl Finv) (Iso.refl F) ≪≫ Fcounit = Fcounit
[PROOFSTEP]
ext X
[GOAL]
case mk'.e_unitIso.w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (NatTrans.app Funit.hom X) ≫ NatTrans.app Fcounit.hom (F.obj X) = 𝟙 (F.obj X)
X : C
⊢ NatTrans.app (Funit ≪≫ hcomp (Iso.refl F) (Iso.refl Finv)).hom X = NatTrans.app Funit.hom X
[PROOFSTEP]
dsimp [NatIso.hcomp]
[GOAL]
case mk'.e_counitIso.w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (NatTrans.app Funit.hom X) ≫ NatTrans.app Fcounit.hom (F.obj X) = 𝟙 (F.obj X)
X : D
⊢ NatTrans.app (hcomp (Iso.refl Finv) (Iso.refl F) ≪≫ Fcounit).hom X = NatTrans.app Fcounit.hom X
[PROOFSTEP]
dsimp [NatIso.hcomp]
[GOAL]
case mk'.e_unitIso.w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (NatTrans.app Funit.hom X) ≫ NatTrans.app Fcounit.hom (F.obj X) = 𝟙 (F.obj X)
X : C
⊢ NatTrans.app Funit.hom X ≫ 𝟙 (Finv.obj (F.obj X)) ≫ Finv.map (𝟙 (F.obj X)) = NatTrans.app Funit.hom X
[PROOFSTEP]
simp only [comp_id, map_id]
[GOAL]
case mk'.e_counitIso.w.w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Finv : D ⥤ C
Funit : 𝟭 C ≅ F ⋙ Finv
Fcounit : Finv ⋙ F ≅ 𝟭 D
Fcomp : ∀ (X : C), F.map (NatTrans.app Funit.hom X) ≫ NatTrans.app Fcounit.hom (F.obj X) = 𝟙 (F.obj X)
X : D
⊢ (𝟙 (F.obj (Finv.obj X)) ≫ F.map (𝟙 (Finv.obj X))) ≫ NatTrans.app Fcounit.hom X = NatTrans.app Fcounit.hom X
[PROOFSTEP]
simp only [id_comp, map_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence F
⊢ ofIso e.symm (ofIso e hF) = hF
[PROOFSTEP]
rw [ofIso_trans, Iso.self_symm_id, ofIso_refl]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hF : IsEquivalence G
⊢ ofIso e (ofIso e.symm hF) = hF
[PROOFSTEP]
rw [ofIso_trans, Iso.symm_self_id, ofIso_refl]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
⊢ f = g
[PROOFSTEP]
have p : F.inv.map (F.map f) = F.inv.map (F.map g) := congrArg F.inv.map h
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
p : (Functor.inv F).map (F.map f) = (Functor.inv F).map (F.map g)
⊢ f = g
[PROOFSTEP]
simpa only [cancel_epi, cancel_mono, IsEquivalence.inv_fun_map] using p
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : F.obj X ⟶ F.obj Y
⊢ (Functor.inv F).map
      (F.map
        ((fun {X Y} f =>
            NatTrans.app (unit (asEquivalence F)) X ≫
              (Functor.inv F).map f ≫ NatTrans.app (unitInv (asEquivalence F)) Y)
          f)) =
    (Functor.inv F).map f
[PROOFSTEP]
simpa only [IsEquivalence.inv_fun_map, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app] using comp_id _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : Full F
inst✝¹ : Faithful F
inst✝ : EssSurj F
X : D
⊢ { obj := fun X => objPreimage F X,
          map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => objPreimage F X,
            map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.obj
        X)
[PROOFSTEP]
apply F.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : Full F
inst✝¹ : Faithful F
inst✝ : EssSurj F
X : D
⊢ F.map
      ({ obj := fun X => objPreimage F X,
            map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.map
        (𝟙 X)) =
    F.map
      (𝟙
        ({ obj := fun X => objPreimage F X,
              map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.obj
          X))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : Full F
inst✝¹ : Faithful F
inst✝ : EssSurj F
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun X => objPreimage F X,
          map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.map
      (f ≫ g) =
    { obj := fun X => objPreimage F X,
            map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.map
        f ≫
      { obj := fun X => objPreimage F X,
            map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.map
        g
[PROOFSTEP]
apply F.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : Full F
inst✝¹ : Faithful F
inst✝ : EssSurj F
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map
      ({ obj := fun X => objPreimage F X,
            map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.map
        (f ≫ g)) =
    F.map
      ({ obj := fun X => objPreimage F X,
              map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.map
          f ≫
        { obj := fun X => objPreimage F X,
              map := fun {X Y} f => F.preimage ((objObjPreimageIso F X).hom ≫ f ≫ (objObjPreimageIso F Y).inv) }.map
          g)
[PROOFSTEP]
simp
  -- #align category_theory.equivalence.equivalence_inverse CategoryTheory.Equivalence.equivalenceInverse
  /- Porting note: this is a private def in mathlib -/

  --
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : Full F
inst✝¹ : Faithful F
inst✝ : EssSurj F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (𝟭 C).map f ≫ ((fun X => (preimageIso F (objObjPreimageIso F (F.obj X))).symm) Y✝).hom =
    ((fun X => (preimageIso F (objObjPreimageIso F (F.obj X))).symm) X✝).hom ≫
      (F ⋙ CategoryTheory.Equivalence.equivalenceInverse F).map f
[PROOFSTEP]
apply F.map_injective
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : Full F
inst✝¹ : Faithful F
inst✝ : EssSurj F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ F.map ((𝟭 C).map f ≫ ((fun X => (preimageIso F (objObjPreimageIso F (F.obj X))).symm) Y✝).hom) =
    F.map
      (((fun X => (preimageIso F (objObjPreimageIso F (F.obj X))).symm) X✝).hom ≫
        (F ⋙ CategoryTheory.Equivalence.equivalenceInverse F).map f)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
C' : Type u_1
e : C' ≃ D
Y : D
⊢ Nonempty ((inducedFunctor ↑e).obj (↑e.symm Y) ≅ Y)
[PROOFSTEP]
simpa using ⟨default⟩


[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → β
a : (ofTypeFunctor m ⋙ ofTypeFunctor m).obj α
⊢ ((ofTypeFunctor m ⋙ ofTypeFunctor m).map f ≫ joinM) a = (joinM ≫ (ofTypeFunctor m).map f) a
[PROOFSTEP]
apply joinM_map_map
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
α : Type u
a : (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj α)
⊢ ((ofTypeFunctor m).map (NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α) ≫
        NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α)
      a =
    (NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) ((ofTypeFunctor m).obj α) ≫
        NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α)
      a
[PROOFSTEP]
apply joinM_map_joinM
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
α : Type u
a : (𝟭 (Type u)).obj ((ofTypeFunctor m).obj α)
⊢ (NatTrans.app (NatTrans.mk (@pure m Applicative.toPure)) ((ofTypeFunctor m).obj α) ≫
        NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α)
      a =
    𝟙 ((𝟭 (Type u)).obj ((ofTypeFunctor m).obj α)) a
[PROOFSTEP]
apply joinM_pure
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
α : Type u
a : (ofTypeFunctor m).obj ((𝟭 (Type u)).obj α)
⊢ ((ofTypeFunctor m).map (NatTrans.app (NatTrans.mk (@pure m Applicative.toPure)) α) ≫
        NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α)
      a =
    𝟙 ((ofTypeFunctor m).obj ((𝟭 (Type u)).obj α)) a
[PROOFSTEP]
apply joinM_map_pure
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
[PROOFSTEP]
funext t
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t =
    ({ obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g) t
[PROOFSTEP]
change _ = joinM (g <$> (f t))
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t = joinM (g <$> f t)
[PROOFSTEP]
simp only [joinM, seq_bind_eq, Function.comp.left_id]
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ (f ≫ g) t = f t >>= g
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
[PROOFSTEP]
letI : _root_.Monad (ofTypeMonad m).obj := show _root_.Monad m from inferInstance
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
[PROOFSTEP]
letI : LawfulMonad (ofTypeMonad m).obj := show LawfulMonad m from inferInstance
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
[PROOFSTEP]
funext t
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t =
    ({ obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g) t
[PROOFSTEP]
dsimp
  -- Porting note: missing tactic `unfold_projs`, using `change` instead.
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ (f ≫ g) t = (f ≫ g) t
[PROOFSTEP]
change joinM (g <$> (f t)) = _
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ joinM (g <$> f t) = (f ≫ g) t
[PROOFSTEP]
simp only [joinM, seq_bind_eq, Function.comp.left_id]
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ f t >>= g = (f ≫ g) t
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
⊢ 𝟭 (KleisliCat m) ≅
    Functor.mk { obj := fun X => X, map := fun {X Y} f => f } ⋙
      Functor.mk { obj := fun X => X, map := fun {X Y} f => f }
[PROOFSTEP]
refine' NatIso.ofComponents (fun X => Iso.refl X) fun f => _
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f : X✝ ⟶ Y✝
⊢ (𝟭 (KleisliCat m)).map f ≫ ((fun X => Iso.refl X) Y✝).hom =
    ((fun X => Iso.refl X) X✝).hom ≫
      (Functor.mk { obj := fun X => X, map := fun {X Y} f => f } ⋙
            Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).map
        f
[PROOFSTEP]
change f >=> pure = pure >=> f
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f : X✝ ⟶ Y✝
⊢ f >=> pure = pure >=> f
[PROOFSTEP]
simp [functor_norm]