awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P ≤ P.retractClosure

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

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.ObjectProperty.retractClosure, CategoryTheory.Retract.refl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.Nonempty
⊢ P.retractClosure.Nonempty

Tactic:
.mono P.le_retractClosure

Premises used: CategoryTheory.ObjectProperty.Nonempty.mono, CategoryTheory.ObjectProperty.le_retractClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
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 : Retract X X'
⊢ Q.retractClosure X

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

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.ObjectProperty.retractClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
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 : Retract X X'
⊢ Q.retractClosure X

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

Tactic:
apply le_antisymm

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

Tactic:
⟨Y, hY, ⟨e⟩⟩
-- 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
hY : P Y
e : Retract X Y
⊢ P X

Tactic:
prop_of_retract P e hY

Premises used: CategoryTheory.ObjectProperty.prop_of_retract
-- 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
hY : P Y
e : Retract X Y
⊢ P X

Tactic:
exact prop_of_retract P e hY

Premises used: CategoryTheory.ObjectProperty.prop_of_retract
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
⊢ P ≤ P.retractClosure

Tactic:
le_retractClosure P

Premises used: CategoryTheory.ObjectProperty.le_retractClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
⊢ P ≤ P.retractClosure

Tactic:
exact le_retractClosure P

Premises used: CategoryTheory.ObjectProperty.le_retractClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (retractClosure ⊥) ⊥

Tactic:
retractClosure_eq_self _

Premises used: CategoryTheory.ObjectProperty.retractClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq.{u + 1} (α := ObjectProperty.{v, u} C) (retractClosure ⊤) ⊤

Tactic:
retractClosure_eq_self _

Premises used: CategoryTheory.ObjectProperty.retractClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
inst_1 : Q.IsStableUnderRetracts
h : P ≤ Q
rw rw₁ : Q ≤ Q
⊢ Q.retractClosure ≤ Q

Tactic:
rw [retractClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.retractClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.isoClosure.retractClosure = P.retractClosure

Tactic:
le_antisymm ?_ (monotone_retractClosure P.le_isoClosure)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.monotone_retractClosure, le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
refine : P.isoClosure.retractClosure ≤ P.retractClosure
⊢ P.isoClosure.retractClosure = P.retractClosure

Tactic:
refine le_antisymm ?_ (monotone_retractClosure P.le_isoClosure)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.monotone_retractClosure, le_antisymm
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
Y X X' : C
hX' : P X'
e : X ≅ X'
h : Retract Y X
⊢ P.retractClosure Y

Tactic:
⟨_, hX', ⟨h.trans (Retract.ofIso e)⟩⟩

Premises used: CategoryTheory.Retract.trans, CategoryTheory.Retract.ofIso, Nonempty.intro, Exists.intro, CategoryTheory.ObjectProperty.retractClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
Y X X' : C
hX' : P X'
e : X ≅ X'
h : Retract Y X
⊢ P.retractClosure Y

Tactic:
exact ⟨_, hX', ⟨h.trans (Retract.ofIso e)⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
r₁ : Retract X Y
Z : C
hZ : P Z
r₂ : Retract Y Z
⊢ P.retractClosure X

Tactic:
⟨Z, hZ, ⟨r₁.trans r₂⟩⟩

Premises used: CategoryTheory.Retract.trans, Nonempty.intro, Exists.intro, CategoryTheory.ObjectProperty.retractClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
r₁ : Retract X Y
Z : C
hZ : P Z
r₂ : Retract Y Z
⊢ P.retractClosure X

Tactic:
refine ⟨Z, hZ, ⟨r₁.trans r₂⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.retractClosure.retractClosure = P.retractClosure

Tactic:
retractClosure_eq_self P.retractClosure

Premises used: CategoryTheory.ObjectProperty.retractClosure_eq_self, CategoryTheory.ObjectProperty.retractClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
obtain :
  ∀ (Q : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q →
      ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure),
        ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := ObjectProperty.EssentiallySmall.exists_small_le.{w} P
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
X Y : C
h : Retract Y X
hX : Q X
⊢ (h.r ≫ h.i) ≫ h.r ≫ h.i = h.r ≫ h.i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
choose :
  ∀ (X Y : (a : Subtype R) → C) (h : (a : Subtype R) → Retract (Y a) (X a))
    (hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)),
    ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure

Tactic:
choose X Y h hX using fun (a : Subtype R) ↦ a.2

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure

Tactic:
⟨.ofObj Y, inferInstance, (monotone_retractClosure h₂).trans ?_⟩

Premises used: CategoryTheory.ObjectProperty.ofObj, CategoryTheory.ObjectProperty.monotone_retractClosure, inferInstance, Exists.intro, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
refine : Q.isoClosure.retractClosure ≤ isoClosure (ofObj Y)
⊢ ∃ (Q : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} Q), P.retractClosure ≤ Q.isoClosure

Tactic:
refine ⟨.ofObj Y, inferInstance, (monotone_retractClosure h₂).trans ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
rw : Q.retractClosure ≤ isoClosure (ofObj Y)
⊢ Q.isoClosure.retractClosure ≤ isoClosure (ofObj Y)

Tactic:
rw [retractClosure_isoClosure]

Premises used: CategoryTheory.ObjectProperty.retractClosure_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y x : C
hx : Q x
r : Retract y x
⊢ (r.r ≫ r.i) ≫ r.r ≫ r.i = r.r ≫ r.i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y x : C
hx : Q x
r : Retract y x
⊢ Q
    (X
      (Subtype.mk (p := R)
        (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
          (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦ p ≫ p = p)
            (r.r ≫ r.i) ⋯))
        ⋯))

Tactic:
obtain ⟨_, hr⟩ := hX ⟨⟨⟨_, hx⟩, r.r ≫ r.i, by simp⟩, ⟨_, _, r, hx, rfl⟩⟩

Premises used: CategoryTheory.Retract.i, Subtype.mk, CategoryTheory.Retract.r, Exists.intro, CategoryTheory.CategoryStruct.comp, Sigma.mk, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y x : C
hx : Q x
r : Retract y x
w :
  Q
    (X
      (Subtype.mk (p := R)
        (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
          (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦ p ≫ p = p)
            (r.r ≫ r.i) ⋯))
        ⋯))
⊢ g
      (h
        (Subtype.mk (p := R)
          (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
            (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦
              p ≫ p = p) (r.r ≫ r.i) ⋯))
          ⋯))
      w =
    (↑(Subtype.mk (p := R)
          (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
            (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦
              p ≫ p = p) (r.r ≫ r.i) ⋯))
          ⋯) :
      α)

Tactic:
obtain ⟨_, hr⟩ := hX ⟨⟨⟨_, hx⟩, r.r ≫ r.i, by simp⟩, ⟨_, _, r, hx, rfl⟩⟩

Premises used: CategoryTheory.Retract.i, Subtype.mk, CategoryTheory.Retract.r, Exists.intro, CategoryTheory.CategoryStruct.comp, Sigma.mk, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y x : C
hx : Q x
r : Retract y x
w_1 :
  Q
    (X
      (Subtype.mk (p := R)
        (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
          (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦ p ≫ p = p)
            (r.r ≫ r.i) ⋯))
        ⋯))
hr :
  g
      (h
        (Subtype.mk (p := R)
          (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
            (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦
              p ≫ p = p) (r.r ≫ r.i) ⋯))
          ⋯))
      w_1 =
    (↑(Subtype.mk (p := R)
          (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
            (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦
              p ≫ p = p) (r.r ≫ r.i) ⋯))
          ⋯) :
      α)
⊢ ∃ (a : Subtype R) (h₁ : Q (X a)), g (h a) h₁ = g r hx

Tactic:
⟨_, _, hr⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y x : C
hx : Q x
r : Retract y x
w_1 :
  Q
    (X
      (Subtype.mk (p := R)
        (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
          (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦ p ≫ p = p)
            (r.r ≫ r.i) ⋯))
        ⋯))
hr :
  g
      (h
        (Subtype.mk (p := R)
          (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
            (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦
              p ≫ p = p) (r.r ≫ r.i) ⋯))
          ⋯))
      w_1 =
    (↑(Subtype.mk (p := R)
          (Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) x hx)
            (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) x hx) : C) ⟶ (↑(Subtype.mk (p := Q) x hx) : C)) ↦
              p ≫ p = p) (r.r ≫ r.i) ⋯))
          ⋯) :
      α)
⊢ ∃ (a : Subtype R) (h₁ : Q (X a)), g (h a) h₁ = g r hx

Tactic:
exact ⟨_, _, hr⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y x : C
hx : Q x
r : Retract y x
obtain : ∀ (a : Subtype R) (h₁ : Q (X a)) (h₂ : g (h a) h₁ = g r hx), isoClosure.{v, u} (ofObj Y) y
⊢ isoClosure.{v, u} (ofObj Y) y

Tactic:
obtain ⟨a, h₁, h₂⟩ : ∃ (a : Subtype R) (h₁ : Q (X a)), g (h a) h₁ = g r hx := by
      obtain ⟨_, hr⟩ := hX ⟨⟨⟨_, hx⟩, r.r ≫ r.i, by simp⟩, ⟨_, _, r, hx, rfl⟩⟩
      exact ⟨_, _, hr⟩

Premises used: Subtype
-- Module: Mathlib.CategoryTheory.ObjectProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_2 : LocallySmall.{w, v, u} C
Q : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} Q
h₁_1 : Q ≤ P
h₂_1 : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }
g : {X Y : C} → (h : Retract Y X) → (hX : Q X) → α :=
  fun {X Y : C} (h : Retract Y X) (hX : Q X) ↦
    Sigma.mk (β := fun (X : Subtype Q) ↦ { p : (↑X : C) ⟶ (↑X : C) // p ≫ p = p }) (Subtype.mk (p := Q) X hX)
      (Subtype.mk (p := fun (p : (↑(Subtype.mk (p := Q) X hX) : C) ⟶ (↑(Subtype.mk (p := Q) X hX) : C)) ↦ p ≫ p = p)
        (h.r ≫ h.i) ⋯)
R : (a : α) → Prop := fun (a : α) ↦ ∃ (X : C) (Y : C) (h : Retract Y X) (hX : Q X), g h hX = a
X Y : (a : Subtype R) → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = (↑a : α)
y x : C
hx : Q x
r : Retract y x
a : Subtype R
h₁ : Q (X a)
h₂ : g (h a) h₁ = g r hx
⊢ x = X a

Tactic:
Subtype.ext_iff.1 (congr_arg Sigma.fst h₂.symm)

Premises used: Sigma.fst, Subtype.ext_iff, congr_arg, Iff.mp, Eq.symm