[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (f.op ≫ (inv f).op).unop = (𝟙 (op Y)).unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ ((inv f).op ≫ f.op).unop = (𝟙 (op X)).unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ (f ≫ (inv f.op).unop).op = (𝟙 X).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ ((inv f.op).unop ≫ f).op = (𝟙 Y).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ IsIso f.unop ↔ IsIso f
[PROOFSTEP]
rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).op = inv f.op
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case hom_inv_id
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ f.op ≫ (inv f).op = 𝟙 (op Y)
[PROOFSTEP]
rw [← op_comp, IsIso.inv_hom_id, op_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).unop = inv f.unop
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case hom_inv_id
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso f
⊢ f.unop ≫ (inv f).unop = 𝟙 Y.unop
[PROOFSTEP]
rw [← unop_comp, IsIso.inv_hom_id, unop_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : Faithful F
X✝ Y✝ : Cᵒᵖ
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F.op.map a₁✝ = F.op.map a₂✝
⊢ a₁✝.unop = a₂✝.unop
[PROOFSTEP]
simpa using map_injective F (Quiver.Hom.op_inj h)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
⊢ F.rightOp.leftOp = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
toPrefunctor✝ : Cᵒᵖ ⥤q D
map_id✝ : ∀ (X : Cᵒᵖ), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ (mk toPrefunctor✝).rightOp.leftOp = mk toPrefunctor✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.op.map f ≫ (fun X => (app α X.unop).op) Y).unop = ((fun X => (app α X.unop).op) X ≫ F.op.map f).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ ((Functor.unop G).map f ≫ (fun X => (app α (op X)).unop) Y).op =
    ((fun X => (app α (op X)).unop) X ≫ (Functor.unop F).map f).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ⟶ G.op
X Y : C
f : X ⟶ Y
⊢ (G.map f ≫ (fun X => (app α (op X)).unop) Y).op = ((fun X => (app α (op X)).unop) X ≫ F.map f).op
[PROOFSTEP]
simpa only [Functor.op_map] using (α.naturality f.op).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : Functor.unop F ⟶ Functor.unop G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.map f ≫ (fun X => (app α X.unop).op) Y).unop = ((fun X => (app α X.unop).op) X ≫ F.map f).unop
[PROOFSTEP]
simpa only [Functor.unop_map] using (α.naturality f.unop).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ Dᵒᵖ
α : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.leftOp.map f ≫ (fun X => (app α X.unop).unop) Y).op = ((fun X => (app α X.unop).unop) X ≫ F.leftOp.map f).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ Dᵒᵖ
α : F.leftOp ⟶ G.leftOp
X Y : C
f : X ⟶ Y
⊢ (G.map f ≫ (fun X => (app α (op X)).op) Y).unop = ((fun X => (app α (op X)).op) X ≫ F.map f).unop
[PROOFSTEP]
simpa only [Functor.leftOp_map] using (α.naturality f.op).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ (G.rightOp.map f ≫ (fun X => (app α (op X)).op) Y).unop = ((fun X => (app α (op X)).op) X ≫ F.rightOp.map f).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ D
α : F.rightOp ⟶ G.rightOp
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.map f ≫ (fun X => (app α X.unop).unop) Y).op = ((fun X => (app α X.unop).unop) X ≫ F.map f).op
[PROOFSTEP]
simpa only [Functor.rightOp_map] using (α.naturality f.unop).symm
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.hom.unop ≫ f.inv.unop = 𝟙 Y.unop
[PROOFSTEP]
simp only [← unop_comp, f.inv_hom_id, unop_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.inv.unop ≫ f.hom.unop = 𝟙 X.unop
[PROOFSTEP]
simp only [← unop_comp, f.hom_inv_id, unop_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ Iso.op (unop f) = f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ (Iso.op (unop f)).hom = f.hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ X Y : C
f : X ≅ Y
⊢ unop (Iso.op f) = f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ X Y : C
f : X ≅ Y
⊢ (unop (Iso.op f)).hom = f.hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
⊢ NatTrans.op α.hom ≫ NatTrans.op α.inv = 𝟙 G.op
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ NatTrans.app (NatTrans.op α.hom ≫ NatTrans.op α.inv) x✝ = NatTrans.app (𝟙 G.op) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.app α.hom x✝.unop).op ≫ (NatTrans.app α.inv x✝.unop).op = 𝟙 (op (G.obj x✝.unop))
[PROOFSTEP]
rw [← op_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.app α.inv x✝.unop ≫ NatTrans.app α.hom x✝.unop).op = 𝟙 (op (G.obj x✝.unop))
[PROOFSTEP]
rw [α.inv_hom_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (G.obj x✝.unop)).op = 𝟙 (op (G.obj x✝.unop))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
⊢ NatTrans.op α.inv ≫ NatTrans.op α.hom = 𝟙 F.op
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ NatTrans.app (NatTrans.op α.inv ≫ NatTrans.op α.hom) x✝ = NatTrans.app (𝟙 F.op) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.app α.inv x✝.unop).op ≫ (NatTrans.app α.hom x✝.unop).op = 𝟙 (op (F.obj x✝.unop))
[PROOFSTEP]
rw [← op_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.app α.hom x✝.unop ≫ NatTrans.app α.inv x✝.unop).op = 𝟙 (op (F.obj x✝.unop))
[PROOFSTEP]
rw [α.hom_inv_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (F.obj x✝.unop)).op = 𝟙 (op (F.obj x✝.unop))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
⊢ NatTrans.removeOp α.hom ≫ NatTrans.removeOp α.inv = 𝟙 G
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ NatTrans.app (NatTrans.removeOp α.hom ≫ NatTrans.removeOp α.inv) x✝ = NatTrans.app (𝟙 G) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (NatTrans.app α.hom (op x✝)).unop ≫ (NatTrans.app α.inv (op x✝)).unop = 𝟙 (G.obj x✝)
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (NatTrans.app α.inv (op x✝) ≫ NatTrans.app α.hom (op x✝)).unop = 𝟙 (G.obj x✝)
[PROOFSTEP]
rw [α.inv_hom_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (𝟙 (G.op.obj (op x✝))).unop = 𝟙 (G.obj x✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
⊢ NatTrans.removeOp α.inv ≫ NatTrans.removeOp α.hom = 𝟙 F
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ NatTrans.app (NatTrans.removeOp α.inv ≫ NatTrans.removeOp α.hom) x✝ = NatTrans.app (𝟙 F) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (NatTrans.app α.inv (op x✝)).unop ≫ (NatTrans.app α.hom (op x✝)).unop = 𝟙 (F.obj x✝)
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (NatTrans.app α.hom (op x✝) ≫ NatTrans.app α.inv (op x✝)).unop = 𝟙 (F.obj x✝)
[PROOFSTEP]
rw [α.hom_inv_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (𝟙 (F.op.obj (op x✝))).unop = 𝟙 (F.obj x✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
⊢ NatTrans.unop α.hom ≫ NatTrans.unop α.inv = 𝟙 (Functor.unop G)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ NatTrans.app (NatTrans.unop α.hom ≫ NatTrans.unop α.inv) x✝ = NatTrans.app (𝟙 (Functor.unop G)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (NatTrans.app α.hom (op x✝)).unop ≫ (NatTrans.app α.inv (op x✝)).unop = 𝟙 (G.obj (op x✝)).unop
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (NatTrans.app α.inv (op x✝) ≫ NatTrans.app α.hom (op x✝)).unop = 𝟙 (G.obj (op x✝)).unop
[PROOFSTEP]
rw [α.inv_hom_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (𝟙 (G.obj (op x✝))).unop = 𝟙 (G.obj (op x✝)).unop
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
⊢ NatTrans.unop α.inv ≫ NatTrans.unop α.hom = 𝟙 (Functor.unop F)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ NatTrans.app (NatTrans.unop α.inv ≫ NatTrans.unop α.hom) x✝ = NatTrans.app (𝟙 (Functor.unop F)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (NatTrans.app α.inv (op x✝)).unop ≫ (NatTrans.app α.hom (op x✝)).unop = 𝟙 (F.obj (op x✝)).unop
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (NatTrans.app α.hom (op x✝) ≫ NatTrans.app α.inv (op x✝)).unop = 𝟙 (F.obj (op x✝)).unop
[PROOFSTEP]
rw [α.hom_inv_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (𝟙 (F.obj (op x✝))).unop = 𝟙 (F.obj (op x✝)).unop
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : Cᵒᵖ
⊢ e.functor.op.map (NatTrans.app (NatIso.op e.unitIso).symm.hom X) ≫
      NatTrans.app (NatIso.op e.counitIso).symm.hom (e.functor.op.obj X) =
    𝟙 (e.functor.op.obj X)
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : Cᵒᵖ
⊢ (e.functor.op.map (NatTrans.app (NatIso.op e.unitIso).symm.hom X) ≫
        NatTrans.app (NatIso.op e.counitIso).symm.hom (e.functor.op.obj X)).unop =
    (𝟙 (e.functor.op.obj X)).unop
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : Cᵒᵖ
⊢ NatTrans.app e.counitIso.inv (e.functor.obj X.unop) ≫ e.functor.map (NatTrans.app e.unitIso.inv X.unop) =
    𝟙 (e.functor.obj X.unop)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ (Functor.unop e.functor).map (NatTrans.app (NatIso.unop e.unitIso).symm.hom X) ≫
      NatTrans.app (NatIso.unop e.counitIso).symm.hom ((Functor.unop e.functor).obj X) =
    𝟙 ((Functor.unop e.functor).obj X)
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ ((Functor.unop e.functor).map (NatTrans.app (NatIso.unop e.unitIso).symm.hom X) ≫
        NatTrans.app (NatIso.unop e.counitIso).symm.hom ((Functor.unop e.functor).obj X)).op =
    (𝟙 ((Functor.unop e.functor).obj X)).op
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ NatTrans.app e.counitIso.inv (e.functor.obj (Opposite.op X)) ≫
      e.functor.map (NatTrans.app e.unitIso.inv (Opposite.op X)) =
    𝟙 (e.functor.obj (Opposite.op X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ
x✝ : A ≅ B
⊢ (fun g => Iso.op g) ((fun f => Iso.unop f) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ
x✝ : A ≅ B
⊢ ((fun g => Iso.op g) ((fun f => Iso.unop f) x✝)).hom = x✝.hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ
x✝ : B.unop ≅ A.unop
⊢ (fun f => Iso.unop f) ((fun g => Iso.op g) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ
x✝ : B.unop ≅ A.unop
⊢ ((fun f => Iso.unop f) ((fun g => Iso.op g) x✝)).hom = x✝.hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (C ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ ((fun F => Iso.op (opUnopIso F.unop)) Y).hom =
      ((fun F => Iso.op (opUnopIso F.unop)) X).hom ≫ (opHom C D ⋙ opInv C D).map f
[PROOFSTEP]
intro F G f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ ((fun F => Iso.op (opUnopIso F.unop)) G).hom =
    ((fun F => Iso.op (opUnopIso F.unop)) F).hom ≫ (opHom C D ⋙ opInv C D).map f
[PROOFSTEP]
dsimp [opUnopIso]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ f ≫ (NatIso.ofComponents fun X => Iso.refl (G.unop.obj X)).hom.op =
    (NatIso.ofComponents fun X => Iso.refl (F.unop.obj X)).hom.op ≫ (NatTrans.mk fun X => NatTrans.app f.unop X).op
[PROOFSTEP]
rw [show f = f.unop.op by simp, ← op_comp, ← op_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ f = f.unop.op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ ((NatIso.ofComponents fun X => Iso.refl (G.unop.obj X)).hom ≫ f.unop).op =
    ((NatTrans.mk fun X => NatTrans.app f.unop.op.unop X) ≫
        (NatIso.ofComponents fun X => Iso.refl (F.unop.obj X)).hom).op
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ (NatIso.ofComponents fun X => Iso.refl (G.unop.obj X)).hom ≫ f.unop =
    (NatTrans.mk fun X => NatTrans.app f.unop.op.unop X) ≫ (NatIso.ofComponents fun X => Iso.refl (F.unop.obj X)).hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (Cᵒᵖ ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ ((fun F => Iso.op (rightOpLeftOpIso F.unop)) Y).hom =
      ((fun F => Iso.op (rightOpLeftOpIso F.unop)) X).hom ≫
        (mk { obj := fun F => F.unop.rightOp, map := fun {X Y} η => NatTrans.rightOp η.unop } ⋙
              mk { obj := fun F => op F.leftOp, map := fun {X Y} η => (NatTrans.leftOp η).op }).map
          f
[PROOFSTEP]
intro F G η
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map η ≫ ((fun F => Iso.op (rightOpLeftOpIso F.unop)) G).hom =
    ((fun F => Iso.op (rightOpLeftOpIso F.unop)) F).hom ≫
      (mk { obj := fun F => F.unop.rightOp, map := fun {X Y} η => NatTrans.rightOp η.unop } ⋙
            mk { obj := fun F => op F.leftOp, map := fun {X Y} η => (NatTrans.leftOp η).op }).map
        η
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ η ≫ (rightOpLeftOpIso G.unop).hom.op =
    (rightOpLeftOpIso F.unop).hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op
[PROOFSTEP]
rw [show η = η.unop.op by simp, ← op_comp, ← op_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ η = η.unop.op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ ((rightOpLeftOpIso G.unop).hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (rightOpLeftOpIso F.unop).hom).op
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ (rightOpLeftOpIso G.unop).hom ≫ η.unop =
    NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (rightOpLeftOpIso F.unop).hom
[PROOFSTEP]
aesop_cat
