awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_2 : F.Full
X Y : Cᵒᵖ
f : F.leftOp.obj X ⟶ F.leftOp.obj Y
⊢ F.leftOp.map (F.preimage f.op).op = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
mk :
  ∀ (obj : Cᵒᵖ → D) (map : {X Y : Cᵒᵖ} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : Cᵒᵖ), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
            Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D }.rightOp.leftOp =
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp }
⊢ F.rightOp.leftOp = F

Tactic:
cases F
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
obj : Cᵒᵖ → D
map : {X Y : Cᵒᵖ} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : Cᵒᵖ), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D }.rightOp.leftOp =
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.op.map f ≫ Quiver.Hom.op (α.app (unop Y))).unop = Quiver.Hom.unop (Quiver.Hom.op (α.app (unop X)) ≫ F.op.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ NatTrans.op (𝟙 F) = 𝟙 F.op

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.op, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : G ⟶ H
⊢ NatTrans.op (α ≫ β) = NatTrans.op β ≫ NatTrans.op α

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Quiver.Hom.unop, CategoryTheory.NatTrans.op, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G_1 : Functor.{v₁, v₂, u₁, u₂} C D
F G : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ (G.unop.map f ≫ Quiver.Hom.unop (α.app (op Y))).op = (Quiver.Hom.unop (α.app (op X)) ≫ F.unop.map f).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
⊢ NatTrans.unop (𝟙 F) = 𝟙 F.unop

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.NatTrans.id, CategoryTheory.NatTrans.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
α : F ⟶ G
β : G ⟶ H
⊢ NatTrans.unop (α ≫ β) = NatTrans.unop β ≫ NatTrans.unop α

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Quiver.Hom.unop, CategoryTheory.NatTrans.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F.op ⟶ G.op
X Y : C
f : X ⟶ Y
⊢ (G.map f ≫ Quiver.Hom.unop (α.app (op Y))).op = (Quiver.Hom.unop (α.app (op X)) ≫ F.map f).op

Tactic:
simpa only [Functor.op_map] using (α.naturality f.op).symm

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Functor.op_map
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ NatTrans.removeOp (𝟙 F.op) = 𝟙 F

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.removeOp, Quiver.Hom.unop, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G_1 : Functor.{v₁, v₂, u₁, u₂} C D
F G : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
α : F.unop ⟶ G.unop
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.map f ≫ Quiver.Hom.op (α.app (unop Y))).unop = Quiver.Hom.unop (Quiver.Hom.op (α.app (unop X)) ≫ F.map f)

Tactic:
simpa only [Functor.unop_map] using (α.naturality f.unop).symm

Premises used: Quiver.Hom.unop, CategoryTheory.Functor.unop_map, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
⊢ NatTrans.removeUnop (𝟙 F.unop) = 𝟙 F

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.removeUnop, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
α : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.leftOp.map f ≫ Quiver.Hom.unop (α.app (unop Y))).op = (Quiver.Hom.unop (α.app (unop X)) ≫ F.leftOp.map f).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
⊢ NatTrans.leftOp (𝟙 F) = 𝟙 F.leftOp

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.NatTrans.leftOp, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
α : F ⟶ G
β : G ⟶ H
⊢ NatTrans.leftOp (α ≫ β) = NatTrans.leftOp β ≫ NatTrans.leftOp α

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Quiver.Hom.unop, CategoryTheory.NatTrans.leftOp, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
α : F.leftOp ⟶ G.leftOp
X Y : C
f : X ⟶ Y
⊢ (G.map f ≫ Quiver.Hom.op (α.app (op Y))).unop = Quiver.Hom.unop (Quiver.Hom.op (α.app (op X)) ≫ F.map f)

Tactic:
simpa only [Functor.leftOp_map] using (α.naturality f.op).symm

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.leftOp_map, Eq.symm
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
⊢ NatTrans.removeLeftOp (𝟙 F.leftOp) = 𝟙 F

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.removeLeftOp, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ (G.rightOp.map f ≫ Quiver.Hom.op (α.app (op Y))).unop =
    Quiver.Hom.unop (Quiver.Hom.op (α.app (op X)) ≫ F.rightOp.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
⊢ NatTrans.rightOp (𝟙 F) = 𝟙 F.rightOp

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.rightOp, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
α : F ⟶ G
β : G ⟶ H
⊢ NatTrans.rightOp (α ≫ β) = NatTrans.rightOp β ≫ NatTrans.rightOp α

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Quiver.Hom.unop, CategoryTheory.NatTrans.rightOp, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
α : F.rightOp ⟶ G.rightOp
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.map f ≫ Quiver.Hom.unop (α.app (unop Y))).op = (Quiver.Hom.unop (α.app (unop X)) ≫ F.map f).op

Tactic:
simpa only [Functor.rightOp_map] using (α.naturality f.unop).symm

Premises used: CategoryTheory.Functor.rightOp_map, Quiver.Hom.unop, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
⊢ NatTrans.removeRightOp (𝟙 F.rightOp) = 𝟙 F

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.NatTrans.removeRightOp, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.hom.unop ≫ f.inv.unop = 𝟙 (Opposite.unop Y)

Tactic:
simp only [← unop_comp, f.inv_hom_id, unop_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.unop_comp, CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.inv.unop ≫ f.hom.unop = 𝟙 (Opposite.unop X)

Tactic:
simp only [← unop_comp, f.hom_inv_id, unop_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.unop_comp, CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
w : f.unop.op.hom = f.hom
⊢ f.unop.op = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op.hom = f.hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
w : f.op.unop.hom = f.hom
⊢ f.op.unop = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop.hom = f.hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := op X ≅ op X) (Iso.op (refl X)) (refl (op X))

Tactic:
rfl

Premises used: CategoryTheory.Iso.op, CategoryTheory.Iso.refl, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ (α ≪≫ β).op = β.op ≪≫ α.op

Tactic:
rfl

Premises used: CategoryTheory.Iso.op, Quiver.Hom.unop, CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
α : X ≅ Y
⊢ α.symm.op = α.op.symm

Tactic:
rfl

Premises used: Quiver.Hom.op, CategoryTheory.Iso.op, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := Opposite.unop X ≅ Opposite.unop X) (unop (refl X)) (refl (Opposite.unop X))

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.Iso.refl, rfl, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
α : X ≅ Y
β : Y ≅ Z
⊢ (α ≪≫ β).unop = β.unop ≪≫ α.unop

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.Iso.trans, rfl, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
α : X ≅ Y
⊢ α.symm.unop = α.unop.symm

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.Iso.symm, rfl, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C Dᵒᵖ
e : F ≅ G
X : C
rw : (e.inv.app X ≫ e.hom.app X).unop = 𝟙 (Opposite.unop (G.obj X))
rw₁ :
  Eq.{v_1 + 1} (α := Opposite.unop (G.obj X) ⟶ Opposite.unop (G.obj X)) (Quiver.Hom.unop (𝟙 (G.obj X)))
    (𝟙 (Opposite.unop (G.obj X)))
rw₂ rw₃ :
  Eq.{v_1 + 1} (α := Opposite.unop (G.obj X) ⟶ Opposite.unop (G.obj X)) (𝟙 (Opposite.unop (G.obj X)))
    (𝟙 (Opposite.unop (G.obj X)))
⊢ (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 (Opposite.unop (G.obj X))

Tactic:
rw [← unop_comp, inv_hom_id_app, unop_id]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C Dᵒᵖ
e : F ≅ G
X : C
rw : (e.hom.app X ≫ e.inv.app X).unop = 𝟙 (Opposite.unop (F.obj X))
rw₁ :
  Eq.{v_1 + 1} (α := Opposite.unop (F.obj X) ⟶ Opposite.unop (F.obj X)) (Quiver.Hom.unop (𝟙 (F.obj X)))
    (𝟙 (Opposite.unop (F.obj X)))
rw₂ rw₃ :
  Eq.{v_1 + 1} (α := Opposite.unop (F.obj X) ⟶ Opposite.unop (F.obj X)) (𝟙 (Opposite.unop (F.obj X)))
    (𝟙 (Opposite.unop (F.obj X)))
⊢ (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 (Opposite.unop (F.obj X))

Tactic:
rw [← unop_comp, hom_inv_id_app, unop_id]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
w : ∀ (x : Cᵒᵖ), (NatTrans.op α.hom ≫ NatTrans.op α.inv).app x = NatTrans.app (𝟙 G.op) x
⊢ NatTrans.op α.hom ≫ NatTrans.op α.inv = 𝟙 G.op

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
x : Cᵒᵖ
w :
  Eq.{v₂ + 1} (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x)))
    (Quiver.Hom.op (α.hom.app (unop x)) ≫ Quiver.Hom.op (α.inv.app (unop x))) (𝟙 (op (G.obj (unop x))))
⊢ (NatTrans.op α.hom ≫ NatTrans.op α.inv).app x = NatTrans.app (𝟙 G.op) x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
x : Cᵒᵖ
w :
  Eq (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x))) (Quiver.Hom.op (α.inv.app (unop x) ≫ α.hom.app (unop x)))
    (𝟙 (op (G.obj (unop x))))
⊢ Eq.{v₂ + 1} (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x)))
    (Quiver.Hom.op (α.hom.app (unop x)) ≫ Quiver.Hom.op (α.inv.app (unop x))) (𝟙 (op (G.obj (unop x))))

Tactic:
rw [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
x : Cᵒᵖ
w :
  Eq.{v₂ + 1} (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x))) (Quiver.Hom.op (𝟙 (G.obj (unop x))))
    (𝟙 (op (G.obj (unop x))))
⊢ Eq (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x))) (Quiver.Hom.op (α.inv.app (unop x) ≫ α.hom.app (unop x)))
    (𝟙 (op (G.obj (unop x))))

Tactic:
rw [α.inv_hom_id_app]

Premises used: CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
x : Cᵒᵖ
⊢ Eq.{v₂ + 1} (α := op (G.obj (unop x)) ⟶ op (G.obj (unop x))) (Quiver.Hom.op (𝟙 (G.obj (unop x))))
    (𝟙 (op (G.obj (unop x))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
w : ∀ (x : Cᵒᵖ), (NatTrans.op α.inv ≫ NatTrans.op α.hom).app x = NatTrans.app (𝟙 F.op) x
⊢ NatTrans.op α.inv ≫ NatTrans.op α.hom = 𝟙 F.op

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
x : Cᵒᵖ
w :
  Eq.{v₂ + 1} (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x)))
    (Quiver.Hom.op (α.inv.app (unop x)) ≫ Quiver.Hom.op (α.hom.app (unop x))) (𝟙 (op (F.obj (unop x))))
⊢ (NatTrans.op α.inv ≫ NatTrans.op α.hom).app x = NatTrans.app (𝟙 F.op) x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
x : Cᵒᵖ
w :
  Eq (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x))) (Quiver.Hom.op (α.hom.app (unop x) ≫ α.inv.app (unop x)))
    (𝟙 (op (F.obj (unop x))))
⊢ Eq.{v₂ + 1} (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x)))
    (Quiver.Hom.op (α.inv.app (unop x)) ≫ Quiver.Hom.op (α.hom.app (unop x))) (𝟙 (op (F.obj (unop x))))

Tactic:
rw [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
x : Cᵒᵖ
w :
  Eq.{v₂ + 1} (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x))) (Quiver.Hom.op (𝟙 (F.obj (unop x))))
    (𝟙 (op (F.obj (unop x))))
⊢ Eq (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x))) (Quiver.Hom.op (α.hom.app (unop x) ≫ α.inv.app (unop x)))
    (𝟙 (op (F.obj (unop x))))

Tactic:
rw [α.hom_inv_id_app]

Premises used: CategoryTheory.Iso.hom_inv_id_app
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
x : Cᵒᵖ
⊢ Eq.{v₂ + 1} (α := op (F.obj (unop x)) ⟶ op (F.obj (unop x))) (Quiver.Hom.op (𝟙 (F.obj (unop x))))
    (𝟙 (op (F.obj (unop x))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ NatIso.op (Iso.refl F) = Iso.refl F.op

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.NatTrans.op, CategoryTheory.NatIso.op, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
β : G ≅ H
⊢ NatIso.op (α ≪≫ β) = NatIso.op β ≪≫ NatIso.op α

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Quiver.Hom.unop, CategoryTheory.NatTrans.op, CategoryTheory.Iso.trans, CategoryTheory.NatIso.op, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
⊢ NatIso.op α.symm = (NatIso.op α).symm

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.op, CategoryTheory.Iso.symm, CategoryTheory.NatIso.op, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
⊢ NatIso.unop (Iso.refl F) = Iso.refl F.unop

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.Iso.refl, CategoryTheory.NatIso.unop, CategoryTheory.NatTrans.id, CategoryTheory.NatTrans.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
α : F ≅ G
β : G ≅ H
⊢ NatIso.unop (α ≪≫ β) = NatIso.unop β ≪≫ NatIso.unop α

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Quiver.Hom.unop, CategoryTheory.Iso.trans, CategoryTheory.NatIso.unop, CategoryTheory.NatTrans.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
α : F ≅ G
⊢ NatIso.unop α.symm = (NatIso.unop α).symm

Tactic:
rfl

Premises used: CategoryTheory.Iso.symm, CategoryTheory.NatIso.unop, CategoryTheory.NatTrans.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C D
α : F ⟶ G
inst_2 : IsIso α
⊢ IsIso (NatTrans.op α)

Tactic:
(NatIso.op (asIso α)).isIso_hom

Premises used: CategoryTheory.NatTrans.op, CategoryTheory.Iso.isIso_hom, CategoryTheory.NatIso.op, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v₁, v_1, u₁, u_1} C D
α : F ⟶ G
inst_2 : IsIso α
⊢ NatTrans.op α ≫ NatTrans.op (inv α) = 𝟙 G.op

Tactic:
simp [← NatTrans.op_comp]

Premises used: CategoryTheory.NatTrans.op_comp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X : Cᵒᵖ
a :
  (e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫
        (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X)).unop =
    Quiver.Hom.unop (𝟙 (e.functor.op.obj X))
⊢ e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫ (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X) =
    𝟙 (e.functor.op.obj X)

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X : Cᵒᵖ
⊢ (e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫
        (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X)).unop =
    Quiver.Hom.unop (𝟙 (e.functor.op.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
X : C
a :
  (e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
        (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X)).op =
    Quiver.Hom.op (𝟙 (e.functor.unop.obj X))
⊢ e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
      (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X) =
    𝟙 (e.functor.unop.obj X)

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} Cᵒᵖ Dᵒᵖ
X : C
⊢ (e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
        (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X)).op =
    Quiver.Hom.op (𝟙 (e.functor.unop.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Cᵒᵖ
inst_1 : Subsingleton.{v₁ + 1} (unop B ⟶ unop A)
⊢ Subsingleton.{v₁ + 1} (A ⟶ B)

Tactic:
(opEquiv A B).subsingleton

Premises used: CategoryTheory.opEquiv, Equiv.subsingleton
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ
f : F ⟶ G
dsimp :
  f ≫ (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) ⋯).hom.op =
    (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) ⋯).hom.op ≫
      Quiver.Hom.op { app := fun (X : C) ↦ f.unop.app X, naturality := ⋯ }
⊢ Eq (α := obj (𝟭 (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) F ⟶ obj (opHom C D ⋙ opInv C D) G)
    (map (𝟭 (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) f ≫
      Iso.hom ((fun (F : (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) ↦ (unop F).opUnopIso.op) G))
    (Iso.hom ((fun (F : (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ) ↦ (unop F).opUnopIso.op) F) ≫ map (opHom C D ⋙ opInv C D) f)

Tactic:
dsimp [opUnopIso]

Premises used: CategoryTheory.Functor.opUnopIso
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ
f : F ⟶ G
⊢ f = f.unop.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (Functor.{v₁, v₂, u₁, u₂} C D)ᵒᵖ
f : F ⟶ G
rw :
  ((NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop).op =
    Quiver.Hom.op
      ({ app := fun (X : C) ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
        (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) ⋯).hom)
⊢ f ≫ (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop G).obj x)) ⋯).hom.op =
    (NatIso.ofComponents (fun (x : C) ↦ Iso.refl ((unop F).obj x)) ⋯).hom.op ≫
      Quiver.Hom.op { app := fun (X : C) ↦ f.unop.app X, naturality := ⋯ }

Tactic:
rw [show f = f.unop.op by simp, ← op_comp, ← op_comp]

Premises used: CategoryTheory.op_comp