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
ι : Type u_1
X : ι → C
inst_2 : Small.{w, u_1} ι
i : ι
⊢ ∃ (a : ι),
    Eq (α := Subtype (ofObj X)) ((fun (i : ι) ↦ (Subtype.mk (p := ofObj X) (X i) ⋯ : Subtype (ofObj X))) a)
      (Subtype.mk (p := ofObj X) (X i) ⋯)

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
X Y : C
⊢ ObjectProperty.Small.{w, v, u} (C := C) (ofObj (ι := Unit ⊕ Unit) (Sum.elim (fun (x : Unit) ↦ X) fun (x : Unit) ↦ Y))

Tactic:
infer_instance
-- 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.Small.{w, v, u} Q
⊢ ObjectProperty.Small.{w, v, u} (P ⊓ Q)

Tactic:
Small.of_le inf_le_right

Premises used: CategoryTheory.ObjectProperty.Small.of_le, inf_le_right
-- 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.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} (P ⊓ Q)

Tactic:
Small.of_le inf_le_left

Premises used: CategoryTheory.ObjectProperty.Small.of_le, inf_le_left
-- 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.Small.{w, v, u} P
inst_3 : ObjectProperty.Small.{w, v, u} Q
x : C
hx : P x
⊢ ∃ (a : Subtype P ⊕ Subtype Q),
    Eq (α := Subtype (P ⊔ Q))
      ((fun (x : Subtype P ⊕ Subtype Q) ↦
          (match (motive := Subtype P ⊕ Subtype Q → Subtype (P ⊔ Q)) x with
            | Sum.inl x => Subtype.mk (p := P ⊔ Q) (↑x : C) ⋯
            | Sum.inr x => Subtype.mk (p := P ⊔ Q) (↑x : C) ⋯ :
            Subtype (P ⊔ Q)))
        a)
      (Subtype.mk (p := P ⊔ Q) x ⋯)

Tactic:
aesop
-- 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.Small.{w, v, u} P
inst_3 : ObjectProperty.Small.{w, v, u} Q
x : C
hx : Q x
⊢ ∃ (a : Subtype P ⊕ Subtype Q),
    Eq (α := Subtype (P ⊔ Q))
      ((fun (x : Subtype P ⊕ Subtype Q) ↦
          (match (motive := Subtype P ⊕ Subtype Q → Subtype (P ⊔ Q)) x with
            | Sum.inl x => Subtype.mk (p := P ⊔ Q) (↑x : C) ⋯
            | Sum.inr x => Subtype.mk (p := P ⊔ Q) (↑x : C) ⋯ :
            Subtype (P ⊔ Q)))
        a)
      (Subtype.mk (p := P ⊔ Q) x ⋯)

Tactic:
aesop
-- 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.Small.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
x : (a : α) × Subtype (P a)
⊢ (⨆ (a : α), P a) (↑(x.snd (β := fun (a : α) ↦ Subtype (P a))) : C)

Tactic:
aesop
-- 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.Small.{w, v, u} (P a)
inst_3 : Small.{w, u_1} α
x_1 : Subtype (α := C) (⨆ (a : α), P a)
x : C
hx : (⨆ (a : α), P a) x
⊢ ∃ (a : (a : α) × Subtype (P a)),
    (fun (x : (a : α) × Subtype (P a)) ↦
          Subtype.mk (p := ⨆ (a : α), P a) (↑(x.snd (β := fun (a : α) ↦ Subtype (P a))) : C) ⋯)
        a =
      Subtype.mk (p := ⨆ (a : α), P a) x hx

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ ObjectProperty.Small.{w, v, u} P.op ↔ ObjectProperty.Small.{w, v, u} P

Tactic:
small_congr
    { toFun x := ⟨x.1.unop, x.2⟩
      invFun x := ⟨op x.1, x.2⟩}

Premises used: small_congr, Equiv.mk, Subtype.mk, Opposite.op, Subtype.val, Opposite.unop, Subtype.property
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
rw : ObjectProperty.Small.{w, v, u} P.unop.op ↔ ObjectProperty.Small.{w, v, u} P
rw₁ rw₂ : ObjectProperty.Small.{w, v, u} P ↔ ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.unop ↔ ObjectProperty.Small.{w, v, u} P

Tactic:
rw [← small_op_iff, op_unop]

Premises used: CategoryTheory.ObjectProperty.op_unop, CategoryTheory.ObjectProperty.small_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.Small.{w, v, u} P
⊢ ObjectProperty.Small.{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.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.unop

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
obtain :
  ∀ (Q : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q →
      ∀ (hQ : P ≤ Q.isoClosure),
        ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure

Tactic:
obtain ⟨Q, _, hQ⟩ := 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
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
⊢ ∀ (X' : Subtype P'), ∃ (X : Subtype P), Nonempty.{v + 1} ((↑X' : C) ≅ (↑X : C))

Tactic:
have h (X' : Subtype P') : ∃ (X : Subtype P), Nonempty (X'.1 ≅ X.1) :=
    ⟨⟨X'.2.2.choose, X'.2.2.choose_spec.choose⟩, X'.2.2.choose_spec.choose_spec⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
h : ∀ (X' : Subtype P'), ∃ (X : Subtype P), Nonempty.{v + 1} ((↑X' : C) ≅ (↑X : C))
choose :
  ∀ (φ : (X' : Subtype P') → Subtype P) (hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))),
    ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure

Tactic:
choose φ hφ using h
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure

Tactic:
⟨fun X ↦ X ∈ Set.range (Subtype.val ∘ φ), ?_, ?_, ?_⟩

Premises used: Function.comp, Membership.mem, And.intro, Exists.intro, Set.range, Subtype.val
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
refine_1 : ObjectProperty.Small.{w, v, u} (C := C) fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)
refine_2 : (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) ≤ P
refine_3 : P ≤ isoClosure fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure

Tactic:
refine ⟨fun X ↦ X ∈ Set.range (Subtype.val ∘ φ), ?_, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : Subtype P'
⊢ (↑(φ X) : C) ∈ Set.range (Subtype.val (p := P) ∘ φ)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
Z : Subtype P'
⊢ ∃ (a : Subtype P'),
    Eq (α := { X : C // X ∈ Set.range (Subtype.val (p := P) ∘ φ) })
      ((fun (X : Subtype P') ↦
          (Subtype.mk (p := fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) (↑(φ X) : C) ⋯ :
            { X : C // X ∈ Set.range (Subtype.val (p := P) ∘ φ) }))
        a)
      (Subtype.mk (p := fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) ((Subtype.val (p := P) ∘ φ) Z) ⋯)

Tactic:
⟨Z, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
Z : Subtype P'
⊢ ∃ (a : Subtype P'),
    Eq (α := { X : C // X ∈ Set.range (Subtype.val (p := P) ∘ φ) })
      ((fun (X : Subtype P') ↦
          (Subtype.mk (p := fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) (↑(φ X) : C) ⋯ :
            { X : C // X ∈ Set.range (Subtype.val (p := P) ∘ φ) }))
        a)
      (Subtype.mk (p := fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) ((Subtype.val (p := P) ∘ φ) Z) ⋯)

Tactic:
exact ⟨Z, rfl⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
⊢ ObjectProperty.Small.{w, v, u} (C := C) fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)

Tactic:
exact small_of_surjective (f := fun X ↦ ⟨(φ X).1, by tauto⟩)
      (by rintro ⟨_, Z, rfl⟩; exact ⟨Z, rfl⟩)

Premises used: small_of_surjective
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : C
hX : X ∈ Set.range (Subtype.val (p := P) ∘ φ)
⊢ ∃ (a : C) (b : P' a), (↑(φ (Subtype.mk (p := fun (a : C) ↦ P' a) a b)) : C) = X

Tactic:
simp only [Set.mem_range, Function.comp_apply, Subtype.exists] at hX

Premises used: Set.mem_range, Subtype.exists, Function.comp_apply
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : C
hX : ∃ (a : C) (b : P' a), (↑(φ (Subtype.mk (p := fun (a : C) ↦ P' a) a b)) : C) = X
refine_2 : ∀ (Y : C) (hY : P' Y), P (↑(φ (Subtype.mk (p := fun (a : C) ↦ P' a) Y hY)) : C)
⊢ P X

Tactic:
obtain ⟨Y, hY, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
Y : C
hY : P' Y
⊢ P (↑(φ (Subtype.mk (p := fun (a : C) ↦ P' a) Y hY)) : C)

Tactic:
(φ ⟨Y, hY⟩).2

Premises used: Subtype.mk, Subtype.property
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
Y : C
hY : P' Y
⊢ P (↑(φ (Subtype.mk (p := fun (a : C) ↦ P' a) Y hY)) : C)

Tactic:
exact (φ ⟨Y, hY⟩).2

Premises used: Subtype.mk, Subtype.property
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : C
hX : P X
refine_3 :
  ∀ (Y : C) (hY : Q Y) (e : X ≅ Y), isoClosure.{v, u} (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) X
⊢ isoClosure.{v, u} (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) X

Tactic:
obtain ⟨Y, hY, ⟨e⟩⟩ := hQ _ hX
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : C
hX : P X
Y : C
hY : Q Y
e : X ≅ Y
Z : Subtype P' := Subtype.mk (p := P') Y ⋯
⊢ isoClosure.{v, u} (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) X

Tactic:
⟨_, ⟨Z, rfl⟩, ⟨e ≪≫ (hφ Z).some⟩⟩

Premises used: Nonempty.some, Nonempty.intro, CategoryTheory.Iso.trans, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty.{v, u} C := Q ⊓ P.isoClosure
φ : (X' : Subtype P') → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty.{v + 1} ((↑X' : C) ≅ (↑(φ X') : C))
X : C
hX : P X
Y : C
hY : Q Y
e : X ≅ Y
Z : Subtype P' := Subtype.mk (p := P') Y ⋯
⊢ isoClosure.{v, u} (fun (X : C) ↦ X ∈ Set.range (Subtype.val (p := P) ∘ φ)) X

Tactic:
exact ⟨_, ⟨Z, rfl⟩, ⟨e ≪≫ (hφ Z).some⟩⟩
-- 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
obtain :
  ∀ (Q : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q →
      Q ≤ P →
        P ≤ Q.isoClosure →
          ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure

Tactic:
obtain ⟨Q, _, _, _⟩ := EssentiallySmall.exists_small_le.{w} P
-- 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
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P
right rwa rwa₁ rwa₂ rwa₃ : P ≤ Q.isoClosure
⊢ P.isoClosure ≤ Q.isoClosure

Tactic:
rwa [isoClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.isoClosure_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
P : ObjectProperty.{v, u} C
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
left : Q ≤ P
right : P ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure

Tactic:
exact ⟨Q, inferInstance, by rwa [isoClosure_le_iff]⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
obtain :
  ∀ (Q : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q →
      ∀ (hQ₁ : Q ≤ P) (hQ₂ : P ≤ Q.isoClosure),
        ∃ (P₀ : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P₀), P = P₀.isoClosure
⊢ ∃ (P₀ : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P₀), P = P₀.isoClosure

Tactic:
obtain ⟨Q, _, hQ₁, hQ₂⟩ := 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
inst_1 : P.IsClosedUnderIsomorphisms
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
rwa rwa₁ rwa₂ rwa₃ : Q ≤ P
⊢ Q.isoClosure ≤ P

Tactic:
rwa [isoClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.isoClosure_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ ∃ (P₀ : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P₀), P = P₀.isoClosure

Tactic:
exact ⟨Q, inferInstance, le_antisymm hQ₂ (by rwa [isoClosure_le_iff])⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} Q
h : P ≤ Q
obtain :
  ∀ (R : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} R →
      ∀ (hR : Q ≤ R.isoClosure),
        ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure

Tactic:
obtain ⟨R, _, hR⟩ := EssentiallySmall.exists_small_le' Q

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le'
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} Q
h : P ≤ Q
R : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} R
hR : Q ≤ R.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure

Tactic:
⟨R, inferInstance, h.trans hR⟩

Premises used: inferInstance, Exists.intro, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.Small
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} Q
h : P ≤ Q
R : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} R
hR : Q ≤ R.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure

Tactic:
exact ⟨R, inferInstance, h.trans hR⟩
-- 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
obtain :
  ∀ (P' : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} P' → ∀ (hP' : P ≤ P'.isoClosure), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

Tactic:
obtain ⟨P', _, hP'⟩ := 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 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
obtain :
  ∀ (Q' : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q' → ∀ (hQ' : Q ≤ Q'.isoClosure), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

Tactic:
obtain ⟨Q', _, hQ'⟩ := EssentiallySmall.exists_small_le' Q

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 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
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

Tactic:
⟨P' ⊔ Q', inferInstance, ?_⟩

Premises used: inferInstance, Max.max, Exists.intro, CategoryTheory.ObjectProperty.EssentiallySmall.mk
-- 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
refine : P ⊔ Q ≤ (P' ⊔ Q').isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

Tactic:
refine ⟨P' ⊔ Q', inferInstance, ?_⟩
-- 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
simp : P ≤ (P' ⊔ Q').isoClosure ∧ Q ≤ (P' ⊔ Q').isoClosure
⊢ P ⊔ Q ≤ (P' ⊔ Q').isoClosure

Tactic:
simp only [sup_le_iff]

Premises used: sup_le_iff