awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isColocal J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isColocal J X
f₁ f₂ : X ⟶ Y
h : Eq.{v + 1} (α := X ⟶ Z) ((fun (f : X ⟶ Y) ↦ f ≫ g) f₁) ((fun (f : X ⟶ Y) ↦ f ≫ g) f₂)
j : J
⊢ Eq.{v + 1} (α := p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Z)
    ((fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y) ↦ f ≫ g)
      ({ pt := X, ι := p.toColimitPresentation (P := W.isColocal).ι :
                Cocone p.toColimitPresentation (P := W.isColocal).diag }.ι.app
          j ≫
        f₁))
    ((fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y) ↦ f ≫ g)
      ({ pt := X, ι := p.toColimitPresentation (P := W.isColocal).ι :
                Cocone p.toColimitPresentation (P := W.isColocal).diag }.ι.app
          j ≫
        f₂))

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isColocal J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isColocal J X
refine : ∀ (f : X ⟶ Z), ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f
⊢ Function.Bijective (β := X ⟶ Z) fun (f : X ⟶ Y) ↦ f ≫ g

Tactic:
refine ⟨fun f₁ f₂ h ↦ p.isColimit.hom_ext
      (fun j ↦ (p.prop_diag_obj j g hg).1 (by simp [h])), fun f ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isColocal J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isColocal J X
f : X ⟶ Z
choose :
  ∀ (app : (j : J) → p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y)
    (h :
      ∀ (j : J),
        (fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y) ↦ f ≫ g) (app j) =
          p.toColimitPresentation (P := W.isColocal).ι.app j ≫ f),
    ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f
⊢ ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f

Tactic:
choose app h using fun j ↦ (p.prop_diag_obj j g hg).2 (p.ι.app j ≫ f)

Premises used: CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, And.right, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.app, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isColocal J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isColocal J X
f : X ⟶ Z
app : (j : J) → p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y
h :
  ∀ (j : J),
    (fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y) ↦ f ≫ g) (app j) =
      p.toColimitPresentation (P := W.isColocal).ι.app j ≫ f
x x_1 : J
a : x ⟶ x_1
⊢ Eq.{v + 1} (α := p.toColimitPresentation (P := W.isColocal).diag.obj x ⟶ Z)
    ((fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj x ⟶ Y) ↦ f ≫ g)
      (p.toColimitPresentation (P := W.isColocal).diag.map a ≫ app x_1))
    ((fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj x ⟶ Y) ↦ f ≫ g)
      (app x ≫ Functor.map (Functor.obj (Functor.const J) Y) a))

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isColocal J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isColocal J X
f : X ⟶ Z
app : (j : J) → p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y
h :
  ∀ (j : J),
    (fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y) ↦ f ≫ g) (app j) =
      p.toColimitPresentation (P := W.isColocal).ι.app j ≫ f
j : J
⊢ { pt := X, ι := p.toColimitPresentation (P := W.isColocal).ι :
              Cocone p.toColimitPresentation (P := W.isColocal).diag }.ι.app
        j ≫
      (fun (f : X ⟶ Y) ↦ f ≫ g)
        (p.toColimitPresentation (P := W.isColocal).isColimit.desc { pt := Y, ι := { app := app, naturality := ⋯ } }) =
    { pt := X, ι := p.toColimitPresentation (P := W.isColocal).ι :
              Cocone p.toColimitPresentation (P := W.isColocal).diag }.ι.app
        j ≫
      f

Tactic:
simp [p.isColimit.fac_assoc, h]

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.IsColimit.fac_assoc, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isColocal J X
Y Z : C
g : Y ⟶ Z
hg : W g
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isColocal J X
f : X ⟶ Z
app : (j : J) → p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y
h :
  ∀ (j : J),
    (fun (f : p.toColimitPresentation (P := W.isColocal).diag.obj j ⟶ Y) ↦ f ≫ g) (app j) =
      p.toColimitPresentation (P := W.isColocal).ι.app j ≫ f
⊢ ∃ (a : X ⟶ Y), (fun (f : X ⟶ Y) ↦ f ≫ g) a = f

Tactic:
exact ⟨p.isColimit.desc (Cocone.mk _
      { app := app
        naturality _ _ a := (p.prop_diag_obj _ g hg).1
          (by simp [h]) }),
      p.isColimit.hom_ext (fun j ↦ by simp [p.isColimit.fac_assoc, h])⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
h : W ≤ W'
f : C
hf : W'.isLocal f
⊢ W.isLocal f

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
W W' : MorphismProperty.{v, u} C
h : W ≤ W'
f : C
hf : W'.isColocal f
⊢ W.isColocal f

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
ι : Sort u_1
W : ι → MorphismProperty.{v, u} C
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (isLocal (⨆ (i : ι), W i)) (⨅ (i : ι), (W i).isLocal)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
ι : Sort u_1
W : ι → MorphismProperty.{v, u} C
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (isColocal (⨆ (i : ι), W i)) (⨅ (i : ι), (W i).isColocal)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
Z : C
h : Function.Bijective (β := X_1 ⟶ Z) fun (g : Y_1 ⟶ Z) ↦ f ≫ g
X Y : C
i : Unit
⊢ Function.Bijective (β := X_1 ⟶ Z) fun (g : Y_1 ⟶ Z) ↦ f ≫ g

Tactic:
h
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
Z : C
h : Function.Bijective (β := X_1 ⟶ Z) fun (g : Y_1 ⟶ Z) ↦ f ≫ g
X Y : C
i : Unit
⊢ Function.Bijective (β := X_1 ⟶ Z) fun (g : Y_1 ⟶ Z) ↦ f ≫ g

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
Z : C
h : Function.Bijective (β := Z ⟶ Y_1) fun (g : Z ⟶ X_1) ↦ g ≫ f
X Y : C
i : Unit
⊢ Function.Bijective (β := Z ⟶ Y_1) fun (f_1 : Z ⟶ X_1) ↦ f_1 ≫ f

Tactic:
h
-- Module: Mathlib.CategoryTheory.ObjectProperty.Local
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
Z : C
h : Function.Bijective (β := Z ⟶ Y_1) fun (g : Z ⟶ X_1) ↦ g ≫ f
X Y : C
i : Unit
⊢ Function.Bijective (β := Z ⟶ Y_1) fun (f_1 : Z ⟶ X_1) ↦ f_1 ≫ f

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
X : Cᵒᵖ
⊢ P.op X ↔ P (unop X)

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.op
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
X : C
⊢ P.unop X ↔ P (op X)

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.Nonempty
⊢ P.op.Nonempty

Tactic:
⟨op P.arbitrary, P.prop_arbitrary⟩

Premises used: CategoryTheory.ObjectProperty.arbitrary, CategoryTheory.ObjectProperty.Nonempty.mk, Opposite.op, Exists.intro, CategoryTheory.ObjectProperty.prop_arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
inst_1 : P.Nonempty
⊢ P.unop.Nonempty

Tactic:
⟨P.arbitrary.unop, P.prop_arbitrary⟩

Premises used: CategoryTheory.ObjectProperty.arbitrary, CategoryTheory.ObjectProperty.Nonempty.mk, Exists.intro, Opposite.unop, CategoryTheory.ObjectProperty.prop_arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
⊢ P.unop.op = P

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.op, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.op.unop = P

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.op, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P.op = Q.op
rw : P.op.unop = Q
rw₁ : P.op.unop = Q.op.unop
rw₂ rw₃ : Q.op.unop = Q.op.unop
⊢ P = Q

Tactic:
rw [← P.unop_op, ← Q.unop_op, h]

Premises used: CategoryTheory.ObjectProperty.unop_op
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} Cᵒᵖ
h : P.unop = Q.unop
rw : P.unop.op = Q
rw₁ : P.unop.op = Q.unop.op
rw₂ rw₃ : Q.unop.op = Q.unop.op
⊢ P = Q

Tactic:
rw [← P.op_unop, ← Q.op_unop, h]

Premises used: CategoryTheory.ObjectProperty.op_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.op = P.op

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
⊢ P.unop = P.unop

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ P.op ≤ Q.op

Tactic:
fun _ hX ↦ h _ hX

Premises used: CategoryTheory.ObjectProperty.op, Opposite.unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} Cᵒᵖ
h : P ≤ Q
⊢ P.unop ≤ Q.unop

Tactic:
fun _ hX ↦ h _ hX

Premises used: CategoryTheory.ObjectProperty.unop, Opposite.op
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
⊢ P.op ≤ Q.op ↔ P ≤ Q

Tactic:
⟨unop_monotone, op_monotone⟩

Premises used: CategoryTheory.ObjectProperty.op_monotone, Iff.intro, CategoryTheory.ObjectProperty.unop_monotone
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} Cᵒᵖ
⊢ P.unop ≤ Q.unop ↔ P ≤ Q

Tactic:
⟨op_monotone, unop_monotone⟩

Premises used: CategoryTheory.ObjectProperty.op_monotone, Iff.intro, CategoryTheory.ObjectProperty.unop_monotone
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
h : ∀ (Z : Cᵒᵖ), ObjectProperty.op.{v, u} (ofObj X) Z ↔ ofObj.{v, u, u_1} (fun (i : ι) ↦ op (X i)) Z
⊢ Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (ObjectProperty.op (ofObj X)) (ofObj fun (i : ι) ↦ op (X i))

Tactic:
ext Z
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
h : (∃ (i : ι), X i = unop Z) ↔ ∃ (i : ι), op (X i) = Z
⊢ ObjectProperty.op.{v, u} (ofObj X) Z ↔ ofObj.{v, u, u_1} (fun (i : ι) ↦ op (X i)) Z

Tactic:
simp only [op_iff, ofObj_iff]

Premises used: CategoryTheory.ObjectProperty.ofObj_iff, CategoryTheory.ObjectProperty.op_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
h : (∃ (i : ι), X i = unop Z) → ∃ (i : ι), op (X i) = Z
h₁ : (∃ (i : ι), op (X i) = Z) → ∃ (i : ι), X i = unop Z
⊢ (∃ (i : ι), X i = unop Z) ↔ ∃ (i : ι), op (X i) = Z

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : X i = unop Z
rw rw₁ : op (unop Z) = Z
⊢ op (X i) = Z

Tactic:
rw [hi]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : X i = unop Z
⊢ ∃ (i : ι), op (X i) = Z

Tactic:
exact ⟨i, by rw [hi]⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : op (X i) = Z
rw rw₁ : X i = unop (op (X i))
⊢ X i = unop Z

Tactic:
rw [← hi]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : op (X i) = Z
⊢ ∃ (i : ι), X i = unop Z

Tactic:
exact ⟨i, by rw [← hi]⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → Cᵒᵖ
⊢ Eq (α := ObjectProperty.{v, u} C) (ObjectProperty.unop (ofObj X)) (ofObj fun (i : ι) ↦ unop (X i))

Tactic:
op_injective ((op_ofObj _).symm)

Premises used: CategoryTheory.ObjectProperty.op_injective, CategoryTheory.ObjectProperty.op_ofObj, Eq.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X : C
⊢ Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (ObjectProperty.op (singleton X)) (singleton (op X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X : Cᵒᵖ
⊢ Eq (α := ObjectProperty.{v, u} C) (ObjectProperty.unop (singleton X)) (singleton (unop X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ∀ (X : C), P.isoClosure.op (op X) ↔ isoClosure.{v, u} P.op (op X)
⊢ P.isoClosure.op = P.op.isoClosure

Tactic:
ext ⟨X⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
⊢ P.isoClosure.op (op X) ↔ isoClosure.{v, u} P.op (op X)

Tactic:
⟨fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨op Y, h, ⟨e.op.symm⟩⟩,
    fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨Y.unop, h, ⟨e.unop.symm⟩⟩⟩

Premises used: CategoryTheory.Iso.op, _private.0.CategoryTheory.ObjectProperty.op_isoClosure.match_2, Nonempty.intro, _private.0.CategoryTheory.ObjectProperty.op_isoClosure.match_1, Opposite.op, CategoryTheory.ObjectProperty.isoClosure, Iff.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.op, Opposite.unop, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
⊢ P.isoClosure.op (op X) ↔ isoClosure.{v, u} P.op (op X)

Tactic:
exact ⟨fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨op Y, h, ⟨e.op.symm⟩⟩,
    fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨Y.unop, h, ⟨e.unop.symm⟩⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
rw : ObjectProperty.op (ObjectProperty.unop P.isoClosure) = P.unop.isoClosure.op
rw₁ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (ObjectProperty.op (ObjectProperty.unop P.isoClosure)) P.unop.op.isoClosure
rw₂ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (P.isoClosure : ObjectProperty.{v, u} Cᵒᵖ) P.unop.op.isoClosure
rw₃ rw₄ : Eq (α := ObjectProperty.{v, u} Cᵒᵖ) (P.isoClosure : ObjectProperty.{v, u} Cᵒᵖ) P.isoClosure
⊢ ObjectProperty.unop P.isoClosure = P.unop.isoClosure

Tactic:
rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]

Premises used: CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.op_injective_iff, CategoryTheory.ObjectProperty.op_isoClosure, CategoryTheory.ObjectProperty.op_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
⊢ (P ⊓ Q).op = P.op ⊓ Q.op

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.op, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
⊢ (P ⊔ Q).op = P.op ⊔ Q.op

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.op, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} Cᵒᵖ
⊢ (P ⊓ Q).unop = P.unop ⊓ Q.unop

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.unop, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} Cᵒᵖ
⊢ (P ⊔ Q).unop = P.unop ⊔ Q.unop

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.unop, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
Y : C
⊢ P.rightOrthogonal Y ↔ ∀ ⦃X : C⦄ (f : X ⟶ Y), P X → f = 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.rightOrthogonal
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X : C
⊢ P.leftOrthogonal X ↔ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P Y → f = 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.leftOrthogonal
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X_1 Y : C
e : X_1 ≅ Y
h : P.rightOrthogonal X_1
X : C
f : X ⟶ Y
hX : P X
rw : f ≫ e.inv = 0
⊢ f = 0

Tactic:
rw [← cancel_mono e.inv, zero_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X_1 Y : C
e : X_1 ≅ Y
h : P.rightOrthogonal X_1
X : C
f : X ⟶ Y
hX : P X
⊢ f ≫ e.inv = 0

Tactic:
h _ hX
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X_1 Y : C
e : X_1 ≅ Y
h : P.rightOrthogonal X_1
X : C
f : X ⟶ Y
hX : P X
⊢ f ≫ e.inv = 0

Tactic:
exact h _ hX
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X Y_1 : C
e : X ≅ Y_1
h : P.leftOrthogonal X
Y : C
f : Y_1 ⟶ Y
hY : P Y
rw : e.hom ≫ f = 0
⊢ f = 0

Tactic:
rw [← cancel_epi e.hom, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X Y_1 : C
e : X ≅ Y_1
h : P.leftOrthogonal X
Y : C
f : Y_1 ⟶ Y
hY : P Y
⊢ e.hom ≫ f = 0

Tactic:
h _ hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
X Y_1 : C
e : X ≅ Y_1
h : P.leftOrthogonal X
Y : C
f : Y_1 ⟶ Y
hY : P Y
⊢ e.hom ≫ f = 0

Tactic:
exact h _ hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
x : C
x_1 : x ⟶ 0
h : P x
⊢ x_1 = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
x : C
x_1 : 0 ⟶ x
h : P x
⊢ x_1 = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
X Y : C
h : Retract X Y
hY : P Y
⊢ P X

Tactic:
IsStableUnderRetracts.of_retract h hY

Premises used: CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_retract
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
x : Retract X Y
h : ⊤ Y
⊢ ⊤ X

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
c : BinaryBicone.{v, u} X Y
h : P c.pt
⊢ P X

Tactic:
of_retract c.retract_left h

Premises used: CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_retract, CategoryTheory.Limits.BinaryBicone.retract_left
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
c : BinaryBicone.{v, u} X Y
h : P c.pt
⊢ P Y

Tactic:
of_retract c.retract_right h

Premises used: CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_retract, CategoryTheory.Limits.BinaryBicone.retract_right
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
inst_3 : HasBinaryBiproduct.{v, u} X Y
h : P (biprod.{v, u} X Y)
⊢ P X

Tactic:
of_binaryBicone_left P (BinaryBiproduct.bicone X Y) h

Premises used: CategoryTheory.Limits.BinaryBiproduct.bicone, CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_binaryBicone_left
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
inst_3 : HasBinaryBiproduct.{v, u} X Y
h : P (biprod.{v, u} X Y)
⊢ P Y

Tactic:
of_binaryBicone_right P (BinaryBiproduct.bicone X Y) h

Premises used: CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_binaryBicone_right, CategoryTheory.Limits.BinaryBiproduct.bicone
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
inst_2 : HasZeroMorphisms.{v, u} C
J : Type u_1
F : J → C
c : Bicone.{u_1, v, u} F
h : P c.pt
j : J
⊢ P (F j)

Tactic:
of_retract (c.retract j) h

Premises used: CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_retract, CategoryTheory.Limits.Bicone.retract
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
inst_2 : HasZeroMorphisms.{v, u} C
J : Type u_1
F : J → C
inst_3 : HasBiproduct.{u_1, v, u} F
h : P (biproduct.{u_1, v, u} F)
j : J
⊢ P (F j)

Tactic:
of_bicone P F (biproduct.bicone F) h j

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_bicone
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
⊢ P.retractClosure X ↔ ∃ (Y : C) (_ : P Y), Nonempty.{v + 1} (Retract X Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
h : P Y
r : Retract X Y
⊢ P.retractClosure X

Tactic:
⟨Y, h, ⟨r⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.ObjectProperty.retractClosure