awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
refine_1 :
  (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)) →
    ∀ (J : Type w) (w : Category.{w', w} J) (e : Equivalence.{v, w', u, w} P.FullSubcategory J),
      ObjectProperty.EssentiallySmall.{w, v, u} P
refine_2 :
  ObjectProperty.EssentiallySmall.{w, v, u} P →
    ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)
⊢ (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)) ↔
    ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
refine ⟨fun ⟨J, _, ⟨e⟩⟩ ↦ ?_, fun _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
h : ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)
J : Type w
w : Category.{w', w} J
e : Equivalence.{v, w', u, w} P.FullSubcategory J
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
⟨.ofObj (e.inverse ⋙ P.ι).obj, inferInstance,
      fun X hX ↦ ⟨_, ⟨⟨(e.functor.obj ⟨X, hX⟩)⟩, ⟨P.ι.mapIso (e.unitIso.app ⟨X, hX⟩)⟩⟩⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.ofObj, CategoryTheory.Equivalence.unitIso, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Equivalence.functor, Nonempty.intro, CategoryTheory.ObjectProperty.ofObj.mk, Exists.intro, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj, CategoryTheory.ObjectProperty.EssentiallySmall.mk, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
h : ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)
J : Type w
w : Category.{w', w} J
e : Equivalence.{v, w', u, w} P.FullSubcategory J
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
exact ⟨.ofObj (e.inverse ⋙ P.ι).obj, inferInstance,
      fun X hX ↦ ⟨_, ⟨⟨(e.functor.obj ⟨X, hX⟩)⟩, ⟨P.ι.mapIso (e.unitIso.app ⟨X, hX⟩)⟩⟩⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
refine_2 :
  ∀ (Q : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q →
      ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure),
        ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)
⊢ ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le.{w} P
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence

Tactic:
rw [← isEquivalence_ιOfLE_iff h₁] at h₂

Premises used: CategoryTheory.ObjectProperty.isEquivalence_ιOfLE_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence
⊢ ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)

Tactic:
⟨_, _, ⟨((ιOfLE h₁).asEquivalence.symm.trans
      (Shrink.equivalence.{w} Q.FullSubcategory)).trans (ShrinkHoms.equivalence.{w'} _)⟩⟩

Premises used: CategoryTheory.ObjectProperty.ιOfLE, CategoryTheory.Functor.asEquivalence, Nonempty.intro, Exists.intro, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Shrink.equivalence, CategoryTheory.Equivalence.trans, CategoryTheory.ObjectProperty.FullSubcategory, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence
⊢ ∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)

Tactic:
exact ⟨_, _, ⟨((ιOfLE h₁).asEquivalence.symm.trans
      (Shrink.equivalence.{w} Q.FullSubcategory)).trans (ShrinkHoms.equivalence.{w'} _)⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : LocallySmall.{w', v_1, u_1} C
rw :
  (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v_1, w', u_1, w} C J)) ↔
    ∃ (J : Type w) (x : Category.{w', w} J),
      Nonempty (Equivalence.{v_1, w', u_1, w} (ObjectProperty.FullSubcategory.{v_1, u_1} (C := C) ⊤) J)
⊢ (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v_1, w', u_1, w} C J)) ↔
    ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤

Tactic:
rw [← ObjectProperty.exists_equivalence_iff]

Premises used: CategoryTheory.ObjectProperty.exists_equivalence_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : LocallySmall.{w', v_1, u_1} C
⊢ (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v_1, w', u_1, w} C J)) ↔
    ∃ (J : Type w) (x : Category.{w', w} J),
      Nonempty (Equivalence.{v_1, w', u_1, w} (ObjectProperty.FullSubcategory.{v_1, u_1} (C := C) ⊤) J)

Tactic:
⟨fun ⟨J, _, ⟨e⟩⟩ ↦ ⟨J, _, ⟨(ObjectProperty.topEquivalence C).trans e⟩⟩,
    fun ⟨J, _, ⟨e⟩⟩ ↦ ⟨J, _, ⟨(ObjectProperty.topEquivalence C).symm.trans e⟩⟩⟩

Premises used: CategoryTheory.Equivalence, Exists, Nonempty.intro, _private.0.CategoryTheory.exists_equivalence_iff_of_locallySmall.match_2, _private.0.CategoryTheory.exists_equivalence_iff_of_locallySmall.match_1, Iff.intro, Exists.intro, Nonempty, CategoryTheory.Equivalence.trans, Top.top, CategoryTheory.ObjectProperty.FullSubcategory, CategoryTheory.ObjectProperty.topEquivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : LocallySmall.{w', v_1, u_1} C
⊢ (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v_1, w', u_1, w} C J)) ↔
    ∃ (J : Type w) (x : Category.{w', w} J),
      Nonempty (Equivalence.{v_1, w', u_1, w} (ObjectProperty.FullSubcategory.{v_1, u_1} (C := C) ⊤) J)

Tactic:
exact ⟨fun ⟨J, _, ⟨e⟩⟩ ↦ ⟨J, _, ⟨(ObjectProperty.topEquivalence C).trans e⟩⟩,
    fun ⟨J, _, ⟨e⟩⟩ ↦ ⟨J, _, ⟨(ObjectProperty.topEquivalence C).symm.trans e⟩⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
rw : EssentiallySmall.{w, v, u} C ↔ ∃ (J : Type w) (x : Category.{w, w} J), Nonempty (Equivalence.{v, w, u, w} C J)
⊢ EssentiallySmall.{w, v, u} C ↔ ObjectProperty.EssentiallySmall.{w, v, u} (C := C) ⊤

Tactic:
rw [← exists_equivalence_iff_of_locallySmall]

Premises used: CategoryTheory.exists_equivalence_iff_of_locallySmall
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ ∃ (J : Type w) (x : Category.{w, w} J), Nonempty (Equivalence.{v, w, u, w} C J)

Tactic:
⟨fun _ ↦ ⟨_, _, ⟨equivSmallModel.{w} C⟩⟩,
    fun ⟨C₀, _, ⟨e⟩⟩ ↦ ⟨C₀, inferInstance, ⟨e⟩⟩⟩

Premises used: CategoryTheory.EssentiallySmall.mk, inferInstance, Nonempty.intro, CategoryTheory.EssentiallySmall, Iff.intro, Exists.intro, CategoryTheory.smallCategorySmallModel, CategoryTheory.SmallModel, _private.0.CategoryTheory.essentiallySmall_iff_objectPropertyEssentiallySmall_top.match_1, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ ∃ (J : Type w) (x : Category.{w, w} J), Nonempty (Equivalence.{v, w, u, w} C J)

Tactic:
exact ⟨fun _ ↦ ⟨_, _, ⟨equivSmallModel.{w} C⟩⟩,
    fun ⟨C₀, _, ⟨e⟩⟩ ↦ ⟨C₀, inferInstance, ⟨e⟩⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inr :
  ∀
    (this :
      ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C] (hC : LocallySmall.{w, v_1, u_1} C),
        EssentiallySmall.{w, v_1, u_1} C ↔
          LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤)
    (hC : ¬LocallySmall.{w, v_1, u_1} C),
    EssentiallySmall.{w, v_1, u_1} C ↔
      LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
wlog :
  ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C] (hC : LocallySmall.{w, v_1, u_1} C),
    EssentiallySmall.{w, v_1, u_1} C ↔
      LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
⊢ EssentiallySmall.{w, v_1, u_1} C ↔
    LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤

Tactic:
wlog hC : LocallySmall.{w} C
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
this :
  ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C] (hC : LocallySmall.{w, v_1, u_1} C),
    EssentiallySmall.{w, v_1, u_1} C ↔
      LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
hC : ¬LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔
    LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤

Tactic:
simp [essentiallySmall_iff, hC]

Premises used: CategoryTheory.essentiallySmall_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
hC : LocallySmall.{w, v_1, u_1} C
simp :
  EssentiallySmall.{w, v_1, u_1} C ↔ ∃ (J : Type w) (x : Category.{w, w} J), Nonempty (Equivalence.{v_1, w, u_1, w} C J)
⊢ EssentiallySmall.{w, v_1, u_1} C ↔
    LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤

Tactic:
simp only [hC, ← exists_equivalence_iff_of_locallySmall, true_and]

Premises used: CategoryTheory.exists_equivalence_iff_of_locallySmall, true_and
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
hC : LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ ∃ (J : Type w) (x : Category.{w, w} J), Nonempty (Equivalence.{v_1, w, u_1, w} C J)

Tactic:
⟨fun H ↦ H.1, fun H ↦ ⟨H⟩⟩

Premises used: CategoryTheory.EssentiallySmall.equiv_smallCategory, CategoryTheory.EssentiallySmall.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
hC : LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ ∃ (J : Type w) (x : Category.{w, w} J), Nonempty (Equivalence.{v_1, w, u_1, w} C J)

Tactic:
refine ⟨fun H ↦ H.1, fun H ↦ ⟨H⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) fun (x : C) ↦ Nonempty.{v_2 + 1} (F.obj x ≅ Y)
rw : LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤
⊢ EssentiallySmall.{w, v_1, u_1} C

Tactic:
rw [essentiallySmall_iff_objectPropertyEssentiallySmall]

Premises used: CategoryTheory.essentiallySmall_iff_objectPropertyEssentiallySmall
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) fun (x : C) ↦ Nonempty.{v_2 + 1} (F.obj x ≅ Y)
Y : D
⊢ ObjectProperty.map ⊤ F Y ≤ F.essImage Y

Tactic:
simp [ObjectProperty.map, Functor.essImage]

Premises used: CategoryTheory.Functor.essImage, CategoryTheory.ObjectProperty.map
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) fun (x : C) ↦ Nonempty.{v_2 + 1} (F.obj x ≅ Y)
⊢ ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) (⊤ ⊓ fun (x : C) ↦ Nonempty.{v_2 + 1} (F.obj x ≅ Y))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) fun (x : C) ↦ Nonempty.{v_2 + 1} (F.obj x ≅ Y)
⊢ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (C := C) ⊤

Tactic:
exact ⟨‹_›, .of_functor _ F (.of_le (Q := F.essImage)
    fun Y ↦ by simp [ObjectProperty.map, Functor.essImage]) (by simpa)⟩
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Quiver.{v₁, u₁} C
X Y : C
⊢ Function.Injective.{v₁ + 1, v₁ + 1} (α := X ⟶ Y) op

Tactic:
fun _ _ H =>
  congr_arg Quiver.Hom.unop H

Premises used: Quiver.Hom.unop, congr_arg, Function.Injective
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Quiver.{v₁, u₁} C
X Y : Cᵒᵖ
⊢ Function.Injective.{v₁ + 1, v₁ + 1} (α := X ⟶ Y) unop

Tactic:
fun _ _ H => congr_arg Quiver.Hom.op H

Premises used: Quiver.Hom.op, congr_arg, Function.Injective
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Quiver.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ f.op.unop = f

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Quiver.{v₁, u₁} C
X Y : Cᵒᵖ
x : Opposite.unop Y ⟶ Opposite.unop X
⊢ unop (Opposite.op x) = x

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Quiver.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ f.unop.op = f

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Quiver.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ unop (Opposite.op f) = f

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := unop X ⟶ unop X) (Quiver.Hom.unop (𝟙 X)) (𝟙 (unop X))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := op (unop X) ⟶ op (unop X)) (Quiver.Hom.op (𝟙 (unop X))) (𝟙 X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).op = g.op ≫ f.op

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := op X ⟶ op X) (Quiver.Hom.op (𝟙 X)) (𝟙 (op X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Quiver.Hom.unop (f ≫ g) = g.unop ≫ f.unop

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := unop (op X) ⟶ unop (op X)) (Quiver.Hom.unop (𝟙 (op X))) (𝟙 X)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (g.unop ≫ f.unop).op = f ≫ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw : Quiver.Hom.op (f.unop ≫ Quiver.Hom.unop (𝟙 X)) = f
rw₁ : (f.unop ≫ 𝟙 (unop X)).op = f
rw₂ : f.unop.op = f
rw₃ rw₄ : f = f
⊢ 𝟙 X ≫ f = f

Tactic:
rw [← op_comp_unop, unop_id, comp_id, Quiver.Hom.op_unop]

Premises used: Quiver.Hom.op_unop, CategoryTheory.Category.comp_id, CategoryTheory.op_comp_unop, CategoryTheory.unop_id
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw : Quiver.Hom.op (Quiver.Hom.unop (𝟙 Y) ≫ f.unop) = f
rw₁ : (𝟙 (unop Y) ≫ f.unop).op = f
rw₂ : f.unop.op = f
rw₃ rw₄ : f = f
⊢ f ≫ 𝟙 Y = f

Tactic:
rw [← op_comp_unop, unop_id, id_comp, Quiver.Hom.op_unop]

Premises used: Quiver.Hom.op_unop, CategoryTheory.op_comp_unop, CategoryTheory.unop_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
simp only [← op_comp_unop, Quiver.Hom.unop_op, assoc]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.op_comp_unop
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
Z' : Cᵒᵖ
h : op X ⟶ Z'
⊢ Eq.{v₁ + 1} (α := op Z ⟶ Z') ((f ≫ g).op ≫ h) (g.op ≫ f.op ≫ h)

Tactic:
simp only [op_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
Z' : C
h : unop X ⟶ Z'
⊢ Quiver.Hom.unop (f ≫ g) ≫ h = g.unop ≫ f.unop ≫ h

Tactic:
simp only [unop_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ IsEquivalence.{v₁, v₁, u₁, u₁} (opOp C)

Tactic:
(opOpEquivalence C).isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.opOp, CategoryTheory.opOpEquivalence
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ IsEquivalence.{v₁, v₁, u₁, u₁} (unopUnop C)

Tactic:
(opOpEquivalence C).isEquivalence_functor

Premises used: CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.unopUnop, CategoryTheory.opOpEquivalence
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ Eq.{v₁ + 1} (α := unop (op Y) ⟶ unop (op Y)) (Quiver.Hom.unop (f.op ≫ (inv f).op)) (Quiver.Hom.unop (𝟙 (op Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ Eq.{v₁ + 1} (α := unop (op X) ⟶ unop (op X)) (Quiver.Hom.unop ((inv f).op ≫ f.op)) (Quiver.Hom.unop (𝟙 (op X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op
⊢ Quiver.Hom.op (f ≫ Quiver.Hom.unop (inv f.op)) = Quiver.Hom.op (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op
⊢ Quiver.Hom.op (Quiver.Hom.unop (inv f.op) ≫ f) = Quiver.Hom.op (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op Y) (Y := op X) f.op ↔ IsIso f

Tactic:
⟨fun _ => isIso_of_op _, fun _ => inferInstance⟩

Premises used: CategoryTheory.isIso_of_op, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
rw :
  IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop X)) (Y := op (unop Y)) f.unop.op ↔
    IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
rw₁ rw₂ :
  IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := op (unop X)) (Y := op (unop Y)) f ↔ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ IsIso f.unop ↔ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f

Tactic:
rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]

Premises used: Quiver.Hom.op_unop, Quiver.Hom.unop, CategoryTheory.isIso_op_iff
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
⊢ IsIso f.unop

Tactic:
(isIso_unop_iff _).2 inferInstance

Premises used: Iff.mpr, CategoryTheory.isIso_unop_iff, inferInstance
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
hom_inv_id : Eq.{v₁ + 1} (α := op Y ⟶ op Y) (f.op ≫ (inv f).op) (𝟙 (op Y))
⊢ (inv f).op = inv f.op

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
hom_inv_id : (inv f ≫ f).op = 𝟙 (op Y)
hom_inv_id₁ : Eq.{v₁ + 1} (α := op Y ⟶ op Y) (Quiver.Hom.op (𝟙 Y)) (𝟙 (op Y))
hom_inv_id₂ hom_inv_id₃ : Eq.{v₁ + 1} (α := op Y ⟶ op Y) (𝟙 (op Y)) (𝟙 (op Y))
⊢ Eq.{v₁ + 1} (α := op Y ⟶ op Y) (f.op ≫ (inv f).op) (𝟙 (op Y))

Tactic:
rw [← op_comp, IsIso.inv_hom_id, op_id]

Premises used: CategoryTheory.op_comp, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
hom_inv_id : f.unop ≫ Quiver.Hom.unop (inv f) = 𝟙 (unop Y)
⊢ Quiver.Hom.unop (inv f) = inv f.unop

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f
hom_inv_id : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (inv f ≫ f)) (𝟙 (unop Y))
hom_inv_id₁ : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (𝟙 Y)) (𝟙 (unop Y))
hom_inv_id₂ hom_inv_id₃ : Eq.{v₁ + 1} (α := unop Y ⟶ unop Y) (𝟙 (unop Y)) (𝟙 (unop Y))
⊢ f.unop ≫ Quiver.Hom.unop (inv f) = 𝟙 (unop Y)

Tactic:
rw [← unop_comp, IsIso.inv_hom_id, unop_id]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.unop_comp, 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 : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
X Y : C
f : X ⟶ Y
⊢ (F.rightOp.map f).unop = F.map f.op

Tactic:
rfl

Premises used: Quiver.Hom.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 : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : Cᵒᵖ
f : F.op.obj X ⟶ F.op.obj Y
⊢ F.op.map (F.preimage f.unop).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
inst_2 : F.Faithful
X Y : Cᵒᵖ
a₁ a₂ : X ⟶ Y
h : F.op.map a₁ = F.op.map a₂
⊢ a₁.unop = a₂.unop

Tactic:
simpa using map_injective F (Quiver.Hom.op_inj h)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Functor.map_injective
-- 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.rightOp.obj X ⟶ F.rightOp.obj Y
⊢ F.rightOp.map (F.preimage f.unop).unop = f

Tactic:
simp