awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.NatIso
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
⊢ IsIso τ ↔ ∀ (X : C), IsIso (τ.app X)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ NatIso.isIso_of_isIso_app _⟩

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.NatIso
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : Functor.{v₁, v₂, u₁, u₂} C D
obj : C → D
e : (X : C) → F.obj X ≅ obj X
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ (F.copyObj obj e).map f

Tactic:
simp [Functor.copyObj]

Premises used: CategoryTheory.Functor.copyObj
-- Module: Mathlib.CategoryTheory.NatIso
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
e : X ≅ Y
⊢ F.map e.inv ≫ α.app X ≫ G.map e.hom = α.app Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.NatIso
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
e : X ≅ Y
⊢ F.map e.hom ≫ α.app Y ≫ G.map e.inv = α.app X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.NatTrans
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
self : NatTrans G F
X Y : C
f : Y ⟶ X
⊢ self.app Y ≫ F.map f = G.map f ≫ self.app X

Tactic:
(self.naturality f).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.NatTrans
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
α β : NatTrans F G
h : α = β
X : C
⊢ α.app X = β.app X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.NatTrans
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 : C
⊢ (NatTrans.id F).app X = 𝟙 (F.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.NatTrans
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
α : NatTrans F G
β : NatTrans G H
X : C
⊢ (α.vcomp β).app X = α.app X ≫ β.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.NatTrans
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
α : NatTrans F G
X Y U V : C
f : X ⟶ Y
g : Y ⟶ U
h : U ⟶ V
⊢ α.app X ≫ G.map f ≫ G.map g ≫ G.map h = F.map f ≫ F.map g ≫ F.map h ≫ α.app V

Tactic:
grind
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
⊢ P ≤ Q ↔ ∀ (X : C), P X → Q X

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
⊢ ¬P ≤ Q ↔ ∃ (X : C), P X ∧ ¬Q X

Tactic:
simp [le_def]

Premises used: CategoryTheory.ObjectProperty.le_def
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
X : C
inst_1 rwa rwa₁ rwa₂ rwa₃ : P.Is X
⊢ P X

Tactic:
rwa [← P.is_iff]

Premises used: CategoryTheory.ObjectProperty.is_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
X : C
hX rwa rwa₁ rwa₂ rwa₃ : P X
⊢ P.Is X

Tactic:
rwa [P.is_iff]

Premises used: CategoryTheory.ObjectProperty.is_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.Nonempty
⊢ ∃ (X : C), P X

Tactic:
Nonempty.exists_prop

Premises used: CategoryTheory.ObjectProperty.Nonempty.exists_prop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
X : C
h : P X
⊢ P.Nonempty

Tactic:
⟨X, h⟩

Premises used: CategoryTheory.ObjectProperty.Nonempty.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.Nonempty
⊢ P P.arbitrary

Tactic:
(exists_prop_of_nonempty P).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.ObjectProperty.exists_prop_of_nonempty, CategoryTheory.ObjectProperty.arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : P.Nonempty
hPQ : P ≤ Q
⊢ Q.Nonempty

Tactic:
nonempty_of_prop (hPQ _ P.prop_arbitrary)

Premises used: CategoryTheory.ObjectProperty.nonempty_of_prop, CategoryTheory.ObjectProperty.prop_arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P < Q
⊢ Q.Nonempty

Tactic:
nonempty_of_prop (not_le_iff_exists.mp (not_le_of_gt h)).choose_spec.1

Premises used: Exists.choose_spec, CategoryTheory.ObjectProperty.not_le_iff_exists, CategoryTheory.ObjectProperty.nonempty_of_prop, And.left, Iff.mp, not_le_of_gt
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
i : ι
⊢ ofObj.{v, u, u'} X (X i)

Tactic:
⟨i⟩

Premises used: CategoryTheory.ObjectProperty.ofObj.mk
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
mp : ofObj.{v, u, u'} X Y → ∃ (i : ι), X i = Y
mpr : (∃ (i : ι), X i = Y) → ofObj.{v, u, u'} X Y
⊢ ofObj.{v, u, u'} X Y ↔ ∃ (i : ι), X i = Y

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
i : ι
⊢ ∃ (i_1 : ι), X i_1 = X i

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
i : ι
⊢ ∃ (i_1 : ι), X i_1 = X i

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
i : ι
⊢ ofObj.{v, u, u'} X (X i)

Tactic:
exact ⟨i⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty.{v, u} C
h : ofObj X ≤ P
i : ι
⊢ ofObj.{v, u, u'} X (X i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty.{v, u} C
h : ∀ (i : ι), P (X i)
i : ι
⊢ P (X i)

Tactic:
h i
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty.{v, u} C
h : ∀ (i : ι), P (X i)
i : ι
⊢ P (X i)

Tactic:
exact h i
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : CategoryStruct.{v, u} C
inst_1 : CategoryStruct.{v', u'} D
ι : Type u'
X : ι → C
inst_2 : Nonempty ι
⊢ ObjectProperty.Nonempty.{v, u} (ofObj X)

Tactic:
nonempty_of_prop (ofObj_apply X (Classical.arbitrary ι))

Premises used: CategoryTheory.ObjectProperty.ofObj_apply, CategoryTheory.ObjectProperty.nonempty_of_prop, Classical.arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
h : ∀ (X : C), ofObj.{v, u, u} (ι := Subtype P) (Subtype.val (p := P)) X ↔ P X
⊢ ofObj (ι := Subtype P) (Subtype.val (p := P)) = P

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
X : C
hX : P X
⊢ P (↑(Subtype.mk (p := P) X hX) : C)

Tactic:
hX
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
X : C
hX : P X
⊢ P (↑(Subtype.mk (p := P) X hX) : C)

Tactic:
exact hX
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
X : C
⊢ ofObj.{v, u, u} (ι := Subtype P) (Subtype.val (p := P)) X ↔ P X

Tactic:
exact ⟨by rintro ⟨X, hX⟩; exact hX,
    fun hX ↦ ofObj_apply Subtype.val ⟨X, hX⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
⊢ singleton.{v, u} X Y ↔ X = Y

Tactic:
simp [ofObj_iff]

Premises used: CategoryTheory.ObjectProperty.ofObj_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X : C
P : ObjectProperty.{v, u} C
⊢ singleton X ≤ P ↔ P X

Tactic:
simp [ofObj_le_iff]

Premises used: CategoryTheory.ObjectProperty.ofObj_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y Z : C
mp : pair.{v, u} X Y Z → X = Z ∨ Y = Z
mpr : X = Z ∨ Y = Z → pair.{v, u} X Y Z
⊢ pair.{v, u} X Y Z ↔ X = Z ∨ Y = Z

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
val : Unit
mp mp₁ :
  ¬X = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inl val) →
    Y = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inl val)
⊢ X = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inl val) ∨
    Y = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inl val)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
val : Unit
mp mp₁ mp₂ mp₃ mp₄ :
  ¬X = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inr val) →
    Y = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inr val)
⊢ X = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inr val) ∨
    Y = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inr val)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
⊢ pair.{v, u} X Y X

Tactic:
⟨Sum.inl .unit⟩

Premises used: CategoryTheory.ObjectProperty.pair, Sum.inl, CategoryTheory.ObjectProperty.ofObj.mk, Sum.elim
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
⊢ pair.{v, u} X Y Y

Tactic:
⟨Sum.inr .unit⟩

Premises used: CategoryTheory.ObjectProperty.pair, CategoryTheory.ObjectProperty.ofObj.mk, Sum.inr, Sum.elim
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
⊢ pair.{v, u} X Y X

Tactic:
exacts [⟨Sum.inl .unit⟩, ⟨Sum.inr .unit⟩]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : CategoryStruct.{v, u} C
inst_1 : CategoryStruct.{v', u'} D
X Y : C
⊢ ObjectProperty.Nonempty.{v, u} (pair X Y)

Tactic:
inferInstanceAs (ofObj _).Nonempty

Premises used: _private.0.CategoryTheory.ObjectProperty.instNonemptyPair._proof_1
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v', u'} D
F : Functor.{v, v', u, u'} C D
X : C
⊢ P.inverseImage F X ↔ P (F.obj X)

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.inverseImage
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
Y : D
⊢ P.map F Y ↔ ∃ (X : C), P X ∧ Nonempty.{v' + 1} (F.obj X ≅ Y)

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.map
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ P.map F (F.obj X)

Tactic:
⟨X, hX, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Iso.refl, Nonempty.intro, And.intro, Exists.intro, CategoryTheory.ObjectProperty.map
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
inst_2 : P.Nonempty
⊢ (P.map F).Nonempty

Tactic:
nonempty_of_prop (P.prop_map_obj F P.prop_arbitrary)

Premises used: CategoryTheory.ObjectProperty.prop_map_obj, CategoryTheory.ObjectProperty.nonempty_of_prop, CategoryTheory.ObjectProperty.prop_arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
F : Functor.{v, v', u, u'} C D
X : D
Y : C
hY : P Y
e : F.obj Y ≅ X
⊢ Q.map F X

Tactic:
⟨Y, h _ hY, ⟨e⟩⟩

Premises used: Nonempty.intro, And.intro, Exists.intro, CategoryTheory.ObjectProperty.map
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
F : Functor.{v, v', u, u'} C D
X : D
Y : C
hY : P Y
e : F.obj Y ≅ X
⊢ Q.map F X

Tactic:
exact ⟨Y, h _ hY, ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ ∃ (X_1 : C), P X_1 ∧ F.obj X_1 = F.obj X

Tactic:
⟨X, hX, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ ∃ (X_1 : C), P X_1 ∧ F.obj X_1 = F.obj X

Tactic:
exact ⟨X, hX, rfl⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ P.strictMap F (F.obj X)

Tactic:
⟨X, hX⟩

Premises used: CategoryTheory.ObjectProperty.strictMap.mk
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ P.strictMap F (F.obj X)

Tactic:
exact ⟨X, hX⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
inst_2 : P.Nonempty
⊢ (P.strictMap F).Nonempty

Tactic:
nonempty_of_prop (P.strictMap_obj F P.prop_arbitrary)

Premises used: CategoryTheory.ObjectProperty.strictMap_obj, CategoryTheory.ObjectProperty.nonempty_of_prop, CategoryTheory.ObjectProperty.prop_arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ Q.strictMap F (F.obj X)

Tactic:
⟨X, h _ hX⟩

Premises used: CategoryTheory.ObjectProperty.strictMap.mk
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ Q.strictMap F (F.obj X)

Tactic:
exact ⟨X, h _ hX⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ P.map F (F.obj X)

Tactic:
exact ⟨X, hX, ⟨Iso.refl _⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
ι : Type u'
X : ι → C
F : Functor.{v, v', u, u'} C D
h : ∀ (Y : D), strictMap (ofObj X) F Y ↔ ofObj.{v', u', u'} (F.obj ∘ X) Y
⊢ strictMap (ofObj X) F = ofObj (F.obj ∘ X)

Tactic:
ext Y
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
ι : Type u'
X : ι → C
F : Functor.{v, v', u, u'} C D
Y : D
⊢ strictMap (ofObj X) F Y ↔ ofObj.{v', u', u'} (F.obj ∘ X) Y

Tactic:
simp [ofObj_iff, strictMap_iff]

Premises used: CategoryTheory.ObjectProperty.ofObj_iff, CategoryTheory.ObjectProperty.strictMap_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
X : C
F : Functor.{v, v', u, u'} C D
h : ∀ (x : D), strictMap (singleton X) F x ↔ singleton.{v', u'} (F.obj X) x
⊢ strictMap (singleton X) F = singleton (F.obj X)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ObjectProperty.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
X : C
F : Functor.{v, v', u, u'} C D
x : D
⊢ strictMap (singleton X) F x ↔ singleton.{v', u'} (F.obj X) x

Tactic:
simp [strictMap_iff]

Premises used: CategoryTheory.ObjectProperty.strictMap_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
X Y : C
e : X ≅ Y
hX : P X
⊢ P Y

Tactic:
IsClosedUnderIsomorphisms.of_iso e hX

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.of_iso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
X Y : C
e : X ≅ Y
⊢ P X ↔ P Y

Tactic:
⟨prop_of_iso P e, prop_of_iso P e.symm⟩

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
hX : P X
⊢ P Y

Tactic:
prop_of_iso P (asIso f) hX

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
⊢ P X ↔ P Y

Tactic:
prop_iff_of_iso P (asIso f)

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
⊢ P.isoClosure X ↔ ∃ (Y : C), ∃ (x : P Y), Nonempty.{v + 1} (X ≅ Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
h : P X
e : X ⟶ Y
inst_1 : IsIso e
⊢ P.isoClosure Y

Tactic:
⟨X, h, ⟨(asIso e).symm⟩⟩

Premises used: Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P ≤ P.isoClosure

Tactic:
fun X hX => ⟨X, hX, ⟨Iso.refl X⟩⟩

Premises used: CategoryTheory.Iso.refl, Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.Nonempty
⊢ P.isoClosure.Nonempty

Tactic:
.mono P.le_isoClosure

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.Nonempty.mono
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Q.isoClosure X

Tactic:
⟨X', h _ hX', ⟨e⟩⟩

Premises used: Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Q.isoClosure X

Tactic:
exact ⟨X', h _ hX', ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
a : P.isoClosure ≤ P
a₁ : P ≤ P.isoClosure
⊢ P.isoClosure = P

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
X : C
a : ∀ (Y : C) (hY : P Y) (e : X ≅ Y), P X
⊢ P.isoClosure X ≤ P X

Tactic:
⟨Y, hY, ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
X Y : C
hY : P Y
e : X ≅ Y
⊢ P X

Tactic:
prop_of_iso P e.symm hY

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
X Y : C
hY : P Y
e : X ≅ Y
⊢ P X

Tactic:
exact prop_of_iso P e.symm hY

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure

Tactic:
le_isoClosure P

Premises used: CategoryTheory.ObjectProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure

Tactic:
exact le_isoClosure P

Premises used: CategoryTheory.ObjectProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : Q.IsClosedUnderIsomorphisms
h : P ≤ Q
rw rw₁ : Q ≤ Q
⊢ Q.isoClosure ≤ Q

Tactic:
rw [isoClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
Z : C
hZ : P Z
f : X ≅ Z
⊢ P.isoClosure Y

Tactic:
⟨Z, hZ, ⟨e.symm.trans f⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Iso.trans, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
X Y : C
e : X ≅ Y
Z : C
hZ : P Z
f : X ≅ Z
⊢ P.isoClosure Y

Tactic:
exact ⟨Z, hZ, ⟨e.symm.trans f⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P.isoClosure = P
rw : P.isoClosure.IsClosedUnderIsomorphisms
⊢ P.IsClosedUnderIsomorphisms

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P.isoClosure = P
⊢ P.isoClosure.IsClosedUnderIsomorphisms

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X_1 Y : D
e : X_1 ≅ Y
X : C
hX : P X
e' : F.obj X ≅ X_1
⊢ P.map F Y

Tactic:
⟨X, hX, ⟨e' ≪≫ e⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Iso.trans, And.intro, Exists.intro, CategoryTheory.ObjectProperty.map
-- Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
X_1 Y : D
e : X_1 ≅ Y
X : C
hX : P X
e' : F.obj X ≅ X_1
⊢ P.map F Y

Tactic:
exact ⟨X, hX, ⟨e' ≪≫ e⟩⟩