awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
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 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
left : P ≤ (P' ⊔ Q').isoClosure
right : Q ≤ (P' ⊔ Q').isoClosure
⊢ P ≤ (P' ⊔ Q').isoClosure ∧ Q ≤ (P' ⊔ Q').isoClosure

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
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 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ P ≤ (P' ⊔ Q').isoClosure

Tactic:
hP'.trans (monotone_isoClosure le_sup_left)

Premises used: le_sup_left, CategoryTheory.ObjectProperty.monotone_isoClosure, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
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 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ P ≤ (P' ⊔ Q').isoClosure

Tactic:
exact hP'.trans (monotone_isoClosure le_sup_left)

Premises used: le_sup_left, CategoryTheory.ObjectProperty.monotone_isoClosure, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
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 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ Q ≤ (P' ⊔ Q').isoClosure

Tactic:
hQ'.trans (monotone_isoClosure le_sup_right)

Premises used: le_sup_right, CategoryTheory.ObjectProperty.monotone_isoClosure, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
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 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ Q ≤ (P' ⊔ Q').isoClosure

Tactic:
exact hQ'.trans (monotone_isoClosure le_sup_right)

Premises used: le_sup_right, CategoryTheory.ObjectProperty.monotone_isoClosure, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
⊢ ∀ (a : α), ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P a ≤ Q.isoClosure

Tactic:
have h (a : α) := EssentiallySmall.exists_small_le' (P a)
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
h : ∀ (a : α), ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P a ≤ Q.isoClosure
choose :
  ∀ (Q : (a : α) → ObjectProperty.{v, u} C),
    (∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)) →
      ∀ (hQ : ∀ (a : α), P a ≤ (Q a).isoClosure),
        ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ (a : α), P a ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ (a : α), P a ≤ Q.isoClosure

Tactic:
choose Q _ hQ using h
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
Q : (a : α) → ObjectProperty.{v, u} C
h : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ (a : α), P a ≤ Q.isoClosure

Tactic:
⟨⨆ a, Q a, inferInstance, ?_⟩

Premises used: iSup, inferInstance, Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
Q : (a : α) → ObjectProperty.{v, u} C
h : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
refine : LE.le.{u} (α := ObjectProperty.{v, u} C) (⨆ (a : α), P a) (isoClosure (⨆ (a : α), Q a))
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ (a : α), P a ≤ Q.isoClosure

Tactic:
refine ⟨⨆ a, Q a, inferInstance, ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
Q : (a : α) → ObjectProperty.{v, u} C
h : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
simp : ∀ (i : α), P i ≤ isoClosure (⨆ (a : α), Q a)
⊢ LE.le.{u} (α := ObjectProperty.{v, u} C) (⨆ (a : α), P a) (isoClosure (⨆ (a : α), Q a))

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
Q : (a : α) → ObjectProperty.{v, u} C
h : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
a : α
⊢ P a ≤ isoClosure (⨆ (a : α), Q a)

Tactic:
(hQ a).trans (monotone_isoClosure (le_iSup Q a))

Premises used: le_iSup, CategoryTheory.ObjectProperty.monotone_isoClosure, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty.{v, u} C
inst_2 : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
Q : (a : α) → ObjectProperty.{v, u} C
h : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
a : α
⊢ P a ≤ isoClosure (⨆ (a : α), Q a)

Tactic:
exact (hQ a).trans (monotone_isoClosure (le_iSup Q a))

Premises used: le_iSup, CategoryTheory.ObjectProperty.monotone_isoClosure, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
refine_1 : ObjectProperty.EssentiallySmall.{w, v, u} P.op → ObjectProperty.EssentiallySmall.{w, v, u} P
refine_2 : ObjectProperty.EssentiallySmall.{w, v, u} P → ObjectProperty.EssentiallySmall.{w, v, u} P.op
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P.op
refine_1 :
  ∀ (Q : ObjectProperty.{v, u} Cᵒᵖ) (h₁ : ObjectProperty.Small.{w, v, u} Q),
    Q ≤ P.op → ∀ (h₂ : P.op ≤ Q.isoClosure), ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
obtain ⟨Q, h₁, _, h₂⟩ := EssentiallySmall.exists_small_le P.op

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le, CategoryTheory.ObjectProperty.op
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty.{v, u} Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
rwa : P ≤ Q.isoClosure.unop
rwa₁ : P.op ≤ Q.isoClosure.unop.op
rwa₂ rwa₃ rwa₄ rwa₅ : P.op ≤ Q.isoClosure
⊢ P ≤ Q.unop.isoClosure

Tactic:
rwa [← unop_isoClosure, ← op_monotone_iff, op_unop]

Premises used: CategoryTheory.ObjectProperty.unop_isoClosure, CategoryTheory.ObjectProperty.op_monotone_iff, CategoryTheory.ObjectProperty.op_unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty.{v, u} Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
exact ⟨Q.unop, inferInstance, by rwa [← unop_isoClosure, ← op_monotone_iff, op_unop]⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
refine_2 :
  ∀ (Q : ObjectProperty.{v, u} C) (h₁ : ObjectProperty.Small.{w, v, u} Q),
    Q ≤ P → ∀ (h₂ : P ≤ Q.isoClosure), ObjectProperty.EssentiallySmall.{w, v, u} P.op
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op

Tactic:
obtain ⟨Q, h₁, _, h₂⟩ := EssentiallySmall.exists_small_le P

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
h₁ : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P
h₂ : P ≤ Q.isoClosure
rwa : P.op ≤ Q.isoClosure.op
rwa₁ rwa₂ rwa₃ rwa₄ : P ≤ Q.isoClosure
⊢ P.op ≤ Q.op.isoClosure

Tactic:
rwa [← op_isoClosure, op_monotone_iff]

Premises used: CategoryTheory.ObjectProperty.op_monotone_iff, CategoryTheory.ObjectProperty.op_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
h₁ : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op

Tactic:
exact ⟨Q.op, inferInstance, by rwa [← op_isoClosure, op_monotone_iff]⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
rw : ObjectProperty.EssentiallySmall.{w, v, u} P.unop.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
rw₁ rw₂ : ObjectProperty.EssentiallySmall.{w, v, u} P ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
rw [← essentiallySmall_op_iff, op_unop]

Premises used: CategoryTheory.ObjectProperty.op_unop, CategoryTheory.ObjectProperty.essentiallySmall_op_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} Cᵒᵖ
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
obtain :
  ∀ (Q : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q →
      ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure), EssentiallySmall.{w, v, u} P.FullSubcategory
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le P

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : 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:
have := (isEquivalence_ιOfLE_iff h₁).2 h₂
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : 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
this : (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence
rw : EssentiallySmall.{w, v, u} Q.FullSubcategory
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
rw [← essentiallySmall_congr (ιOfLE h₁).asEquivalence]

Premises used: CategoryTheory.ObjectProperty.ιOfLE, CategoryTheory.Functor.asEquivalence, CategoryTheory.essentiallySmall_congr
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : 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
this : (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence
⊢ EssentiallySmall.{w, v, u} Q.FullSubcategory

Tactic:
essentiallySmall_of_small_of_locallySmall _

Premises used: CategoryTheory.essentiallySmall_of_small_of_locallySmall
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : 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
this : (ιOfLE (P := Q) (P' := P) h₁).IsEquivalence
⊢ EssentiallySmall.{w, v, u} Q.FullSubcategory

Tactic:
exact essentiallySmall_of_small_of_locallySmall _

Premises used: CategoryTheory.essentiallySmall_of_small_of_locallySmall
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.Small.{w, v, u} P
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ ∃ (a : Subtype P),
    (fun (X : Subtype P) ↦ Subtype.mk (p := P.strictMap F) (F.obj (↑X : C)) ⋯) a =
      Subtype.mk (p := P.strictMap F) (F.obj X) ⋯

Tactic:
⟨⟨X, hX⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.Small.{w, v, u} P
F : Functor.{v, v', u, u'} C D
X : C
hX : P X
⊢ ∃ (a : Subtype P),
    (fun (X : Subtype P) ↦ Subtype.mk (p := P.strictMap F) (F.obj (↑X : C)) ⋯) a =
      Subtype.mk (p := P.strictMap F) (F.obj X) ⋯

Tactic:
exact ⟨⟨X, hX⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
F : Functor.{v, v', u, u'} C D
obtain :
  ∀ (Q : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q →
      ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure), ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le P

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
F : Functor.{v, v', u, u'} C D
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ Q.isoClosure.map F ≤ (Q.strictMap F).isoClosure

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
F : Functor.{v, v', u, u'} C D
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)

Tactic:
exact ⟨Q.strictMap F, inferInstance, (map_monotone h₂ F).trans (by simp)⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y))
choose :
  ∀ (P₁ : ObjectProperty.{v', u'} D) (hP₁ : ObjectProperty.Small.{w, v', u'} P₁) (x : (i : D) → P.map F i → D)
    (hP₁x : ∀ (i : D) (a : P.map F i), P₁ (x i a)) (hx : ∀ (i : D) (a : P.map F i), Nonempty.{v' + 1} (i ≅ x i a)),
    ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
choose P₁ hP₁ x hP₁x hx using H₁.1

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le'
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y))
P₁ : ObjectProperty.{v', u'} D
hP₁ : ObjectProperty.Small.{w, v', u'} P₁
x : (i : D) → P.map F i → D
hP₁x : ∀ (i : D) (a : P.map F i), P₁ (x i a)
hx : ∀ (i : D) (a : P.map F i), Nonempty.{v' + 1} (i ≅ x i a)
choose :
  ∀ (P₂ : (Y : D) → ObjectProperty.{v, u} C) (hP₂ : ∀ (Y : D), ObjectProperty.Small.{w, v, u} (P₂ Y))
    (y : (Y : D) → (i : C) → (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i → C)
    (hP₂y : ∀ (Y : D) (i : C) (a : (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i), P₂ Y (y Y i a))
    (hy :
      ∀ (Y : D) (i : C) (a : (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i), Nonempty.{v + 1} (i ≅ y Y i a)),
    ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
choose P₂ hP₂ y hP₂y hy using fun Y ↦ (H₂ Y).1

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le', CategoryTheory.Iso, Nonempty, CategoryTheory.Functor.obj, Min.min
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y))
P₁ : ObjectProperty.{v', u'} D
hP₁ : ObjectProperty.Small.{w, v', u'} P₁
x : (i : D) → P.map F i → D
hP₁x : ∀ (i : D) (a : P.map F i), P₁ (x i a)
hx : ∀ (i : D) (a : P.map F i), Nonempty.{v' + 1} (i ≅ x i a)
P₂ : (Y : D) → ObjectProperty.{v, u} C
hP₂ : ∀ (Y : D), ObjectProperty.Small.{w, v, u} (P₂ Y)
y : (Y : D) → (i : C) → (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i → C
hP₂y : ∀ (Y : D) (i : C) (a : (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i), P₂ Y (y Y i a)
hy : ∀ (Y : D) (i : C) (a : (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i), Nonempty.{v + 1} (i ≅ y Y i a)
f : Subtype P → (i : Subtype P₁) × Subtype (P₂ (↑i : D)) :=
  fun (c : Subtype P) ↦
    Sigma.mk (β := fun (i : Subtype P₁) ↦ Subtype (P₂ (↑i : D))) (Subtype.mk (p := P₁) (x (F.obj (↑c : C)) ⋯) ⋯)
      (Subtype.mk (p := P₂ (↑(Subtype.mk (p := P₁) (x (F.obj (↑c : C)) ⋯) ⋯) : D)) (y (x (F.obj (↑c : C)) ⋯) (↑c : C) ⋯)
        ⋯)
g : (i : Subtype P₁) × Subtype (P₂ (↑i : D)) → C :=
  fun (i : (i : Subtype P₁) × Subtype (P₂ (↑i : D))) ↦
    (↑(i.snd (β := fun (i : Subtype P₁) ↦ Subtype (P₂ (↑i : D)))) : C)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
⟨.ofObj g, inferInstance, fun X hX ↦ ⟨_, ⟨f ⟨X, hX⟩⟩, hy _ _ _⟩⟩

Premises used: CategoryTheory.ObjectProperty.ofObj, inferInstance, CategoryTheory.Iso.refl, Nonempty.intro, Subtype.mk, CategoryTheory.ObjectProperty.ofObj.mk, And.intro, Exists.intro, Subtype.val, CategoryTheory.Functor.obj, CategoryTheory.ObjectProperty.EssentiallySmall.mk, Subtype.property
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y))
P₁ : ObjectProperty.{v', u'} D
hP₁ : ObjectProperty.Small.{w, v', u'} P₁
x : (i : D) → P.map F i → D
hP₁x : ∀ (i : D) (a : P.map F i), P₁ (x i a)
hx : ∀ (i : D) (a : P.map F i), Nonempty.{v' + 1} (i ≅ x i a)
P₂ : (Y : D) → ObjectProperty.{v, u} C
hP₂ : ∀ (Y : D), ObjectProperty.Small.{w, v, u} (P₂ Y)
y : (Y : D) → (i : C) → (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i → C
hP₂y : ∀ (Y : D) (i : C) (a : (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i), P₂ Y (y Y i a)
hy : ∀ (Y : D) (i : C) (a : (P ⊓ fun (x : C) ↦ Nonempty.{v' + 1} (F.obj x ≅ Y)) i), Nonempty.{v + 1} (i ≅ y Y i a)
f : Subtype P → (i : Subtype P₁) × Subtype (P₂ (↑i : D)) :=
  fun (c : Subtype P) ↦
    Sigma.mk (β := fun (i : Subtype P₁) ↦ Subtype (P₂ (↑i : D))) (Subtype.mk (p := P₁) (x (F.obj (↑c : C)) ⋯) ⋯)
      (Subtype.mk (p := P₂ (↑(Subtype.mk (p := P₁) (x (F.obj (↑c : C)) ⋯) ⋯) : D)) (y (x (F.obj (↑c : C)) ⋯) (↑c : C) ⋯)
        ⋯)
g : (i : Subtype P₁) × Subtype (P₂ (↑i : D)) → C :=
  fun (i : (i : Subtype P₁) × Subtype (P₂ (↑i : D))) ↦
    (↑(i.snd (β := fun (i : Subtype P₁) ↦ Subtype (P₂ (↑i : D)))) : C)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
exact ⟨.ofObj g, inferInstance, fun X hX ↦ ⟨_, ⟨f ⟨X, hX⟩⟩, hy _ _ _⟩⟩
-- 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
⊢ (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (Equivalence.{v, w', u, w} P.FullSubcategory J)) ↔
    ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
⟨fun ⟨J, _, ⟨e⟩⟩ ↦ ?_, fun _ ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall, _private.0.CategoryTheory.ObjectProperty.exists_equivalence_iff.match_1, Iff.intro