awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ (lift : j ⟶ e), D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ (li : i ⟶ e) (lj : j ⟶ e), D.W li ∧ D.W lj ∧ f ≫ lj = li
i j : J
x : i ⟶ j
hf : D.W x
li : i ⟶ e
lj : j ⟶ e
hli : D.W li
hlj : D.W lj
fac : x ≫ lj = li
rw : x ≫ ⋯.choose (p := D.W) = li
rw₁ : x ≫ lj = li
rw₂ rw₃ : li = li
⊢ x ≫ ⋯.choose (p := D.W) = ⋯.choose (p := D.W)

Tactic:
rw [h₂ (D.src hf) _ li (h₁ (D.src hf)).choose_spec hli,
      h₂ (D.tgt hf) _ lj (h₁ (D.tgt hf)).choose_spec hlj, fac]

Premises used: Exists.choose_spec, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ D₂ : DiagramWithUniqueTerminal J κ
hW : D₁.W = D₂.W
hP : D₁.P = D₂.P
obtain :
  ∀ (D₁ : Diagram J κ) (top : J) (h₁ : D₁.IsTerminal top) (h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top)
    (hW :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W = D₂.W)
    (hP :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P = D₂.P),
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } = D₂
⊢ D₁ = D₂

Tactic:
obtain ⟨D₁, top, h₁, h₁'⟩ := D₁

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.top
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₂ : DiagramWithUniqueTerminal J κ
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
hW : { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W = D₂.W
hP : { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P = D₂.P
obtain :
  ∀ (D₂ : Diagram J κ) (top' : J) (h₂ : D₂.IsTerminal top') (h₂' : ∀ (j : J) (hj : D₂.IsTerminal j), j = top')
    (hW :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
        { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W)
    (hP :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
        { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P),
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
      { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } = D₂

Tactic:
obtain ⟨D₂, top', h₂, h₂'⟩ := D₂
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
D₂ : Diagram J κ
top' : J
h₂ : D₂.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₂.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
⊢ D₁ = D₂

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
D₂ : Diagram J κ
top' : J
h₂ : D₂.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₂.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
obtain :
  ∀ (h₂ : D₁.IsTerminal top') (h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top')
    (hW :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
        { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W)
    (hP :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
        { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P),
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
      { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }

Tactic:
obtain rfl : D₁ = D₂ := by aesop

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
top' : J
h₂ : D₁.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
⊢ top = top'

Tactic:
h₂' _ h₁
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
top' : J
h₂ : D₁.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
obtain :
  ∀ (h₂ : D₁.IsTerminal top) (h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top)
    (hW :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
        { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W)
    (hP :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
        { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P),
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
      { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' }
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }

Tactic:
obtain rfl : top = top' := h₂' _ h₁

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
h₂ : D₁.IsTerminal top
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
⊢ h₁ = h₂

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
h₂ : D₁.IsTerminal top
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
obtain :
  ∀
    (hW :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
        { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W)
    (hP :
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
        { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P),
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' }
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' }

Tactic:
obtain rfl : h₁ = h₂ := by subsingleton

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x : DiagramWithUniqueTerminal J κ
⊢ x.W ≤ x.W

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x : DiagramWithUniqueTerminal J κ
⊢ x.P ≤ x.P

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x x_1 : DiagramWithUniqueTerminal J κ
h₁ : x.W ≤ x_1.W ∧ x.P ≤ x_1.P
h₂ : x_1.W ≤ x.W ∧ x_1.P ≤ x.P
hW : x.W = x_1.W
hP : x.P = x_1.P
⊢ x = x_1

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x x_1 : DiagramWithUniqueTerminal J κ
h₁ : x.W ≤ x_1.W ∧ x.P ≤ x_1.P
h₂ : x_1.W ≤ x.W ∧ x_1.P ≤ x.P
⊢ x.W = x_1.W

Tactic:
le_antisymm h₁.1 h₂.1

Premises used: le_antisymm, And.left
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x x_1 : DiagramWithUniqueTerminal J κ
h₁ : x.W ≤ x_1.W ∧ x.P ≤ x_1.P
h₂ : x_1.W ≤ x.W ∧ x_1.P ≤ x.P
⊢ x.W = x_1.W

Tactic:
exact le_antisymm h₁.1 h₂.1

Premises used: le_antisymm, And.left
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x x_1 : DiagramWithUniqueTerminal J κ
h₁ : x.W ≤ x_1.W ∧ x.P ≤ x_1.P
h₂ : x_1.W ≤ x.W ∧ x_1.P ≤ x.P
⊢ x.P = x_1.P

Tactic:
le_antisymm h₁.2 h₂.2

Premises used: le_antisymm, And.right
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x x_1 : DiagramWithUniqueTerminal J κ
h₁ : x.W ≤ x_1.W ∧ x.P ≤ x_1.P
h₂ : x_1.W ≤ x.W ∧ x_1.P ≤ x.P
⊢ x.P = x_1.P

Tactic:
exact le_antisymm h₁.2 h₂.2

Premises used: le_antisymm, And.right
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : DiagramWithUniqueTerminal J κ
⊢ functorMap ⋯ = 𝟙 D.top

Tactic:
simp [functorMap]

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ D₂ D₃ : DiagramWithUniqueTerminal J κ
h₁₂ : D₁ ≤ D₂
h₂₃ : D₂ ≤ D₃
⊢ functorMap h₁₂ ≫ functorMap h₂₃ = functorMap ⋯

Tactic:
D₃.isTerminal.comm _ (h₂₃.1 _ (D₂.isTerminal.hlift _))

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.comm, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.hlift, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.isTerminal, And.left
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j X Y : J
i : Unit
⊢ ObjectProperty.ofObj (fun (x : Unit) ↦ j) j

Tactic:
⟨⟨⟩⟩

Premises used: CategoryTheory.ObjectProperty.ofObj.mk
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j X Y : J
i : Unit
⊢ ObjectProperty.ofObj (fun (x : Unit) ↦ j) j

Tactic:
exact ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
f : Arrow J
hf :
  Membership.mem (γ := Set (Arrow J))
    (MorphismProperty.toSet
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
    f
⊢ ∃ (a : Unit),
    (fun (x : Unit) ↦
          (Subtype.mk (p := fun (x : Arrow J) ↦
              Membership.mem (γ := Set (Arrow J))
                (MorphismProperty.toSet
                  (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                x)
              (Arrow.mk (𝟙 j)) ⋯ :
            { x : Arrow J //
              Membership.mem (γ := Set (Arrow J))
                (MorphismProperty.toSet
                  (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                x }))
        a =
      Subtype.mk (p := fun (x : Arrow J) ↦
        Membership.mem (γ := Set (Arrow J))
          (MorphismProperty.toSet
            (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
          x)
        f hf

Tactic:
⟨⟨⟩, ?_⟩

Premises used: Exists.intro, PUnit.unit
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
f : Arrow J
hf :
  Membership.mem (γ := Set (Arrow J))
    (MorphismProperty.toSet
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
    f
refine :
  (fun (x : Unit) ↦
        (Subtype.mk (p := fun (x : Arrow J) ↦
            Membership.mem (γ := Set (Arrow J))
              (MorphismProperty.toSet
                (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
              x)
            (Arrow.mk (𝟙 j)) ⋯ :
          { x : Arrow J //
            Membership.mem (γ := Set (Arrow J))
              (MorphismProperty.toSet
                (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
              x }))
      PUnit.unit =
    Subtype.mk (p := fun (x : Arrow J) ↦
      Membership.mem (γ := Set (Arrow J))
        (MorphismProperty.toSet
          (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
        x)
      f hf
⊢ ∃ (a : Unit),
    (fun (x : Unit) ↦
          (Subtype.mk (p := fun (x : Arrow J) ↦
              Membership.mem (γ := Set (Arrow J))
                (MorphismProperty.toSet
                  (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                x)
              (Arrow.mk (𝟙 j)) ⋯ :
            { x : Arrow J //
              Membership.mem (γ := Set (Arrow J))
                (MorphismProperty.toSet
                  (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                x }))
        a =
      Subtype.mk (p := fun (x : Arrow J) ↦
        Membership.mem (γ := Set (Arrow J))
          (MorphismProperty.toSet
            (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
          x)
        f hf

Tactic:
refine ⟨⟨⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
f : Arrow J
hf :
  Membership.mem (γ := Set (Arrow J))
    (MorphismProperty.toSet
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
    f
a :
  (↑((fun (x : Unit) ↦
            (Subtype.mk (p := fun (x : Arrow J) ↦
                Membership.mem (γ := Set (Arrow J))
                  (MorphismProperty.toSet
                    (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                  x)
                (Arrow.mk (𝟙 j)) ⋯ :
              { x : Arrow J //
                Membership.mem (γ := Set (Arrow J))
                  (MorphismProperty.toSet
                    (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                  x }))
          PUnit.unit) :
      Arrow J) =
    (↑(Subtype.mk (p := fun (x : Arrow J) ↦
          Membership.mem (γ := Set (Arrow J))
            (MorphismProperty.toSet
              (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
            x)
          f hf) :
      Arrow J)
⊢ (fun (x : Unit) ↦
        (Subtype.mk (p := fun (x : Arrow J) ↦
            Membership.mem (γ := Set (Arrow J))
              (MorphismProperty.toSet
                (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
              x)
            (Arrow.mk (𝟙 j)) ⋯ :
          { x : Arrow J //
            Membership.mem (γ := Set (Arrow J))
              (MorphismProperty.toSet
                (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
              x }))
      PUnit.unit =
    Subtype.mk (p := fun (x : Arrow J) ↦
      Membership.mem (γ := Set (Arrow J))
        (MorphismProperty.toSet
          (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
        x)
      f hf

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
f : Arrow J
hf :
  Membership.mem (γ := Set (Arrow J))
    (MorphismProperty.toSet
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
    f
⊢ (↑((fun (x : Unit) ↦
            (Subtype.mk (p := fun (x : Arrow J) ↦
                Membership.mem (γ := Set (Arrow J))
                  (MorphismProperty.toSet
                    (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                  x)
                (Arrow.mk (𝟙 j)) ⋯ :
              { x : Arrow J //
                Membership.mem (γ := Set (Arrow J))
                  (MorphismProperty.toSet
                    (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                  x }))
          PUnit.unit) :
      Arrow J) =
    (↑(Subtype.mk (p := fun (x : Arrow J) ↦
          Membership.mem (γ := Set (Arrow J))
            (MorphismProperty.toSet
              (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
            x)
          f hf) :
      Arrow J)

Tactic:
((MorphismProperty.ofHoms_iff _ _).1
        ((MorphismProperty.arrow_mk_mem_toSet_iff _ _).1 hf)).choose_spec.symm

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff, Exists.choose_spec, CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff, Iff.mp, CategoryTheory.Arrow, CategoryTheory.Arrow.mk, Eq.symm
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
f : Arrow J
hf :
  Membership.mem (γ := Set (Arrow J))
    (MorphismProperty.toSet
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
    f
⊢ (↑((fun (x : Unit) ↦
            (Subtype.mk (p := fun (x : Arrow J) ↦
                Membership.mem (γ := Set (Arrow J))
                  (MorphismProperty.toSet
                    (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                  x)
                (Arrow.mk (𝟙 j)) ⋯ :
              { x : Arrow J //
                Membership.mem (γ := Set (Arrow J))
                  (MorphismProperty.toSet
                    (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                  x }))
          PUnit.unit) :
      Arrow J) =
    (↑(Subtype.mk (p := fun (x : Arrow J) ↦
          Membership.mem (γ := Set (Arrow J))
            (MorphismProperty.toSet
              (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
            x)
          f hf) :
      Arrow J)

Tactic:
exact ((MorphismProperty.ofHoms_iff _ _).1
        ((MorphismProperty.arrow_mk_mem_toSet_iff _ _).1 hf)).choose_spec.symm

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff, Exists.choose_spec, CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff, Iff.mp, Eq.symm
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
x : Unit
⊢ ObjectProperty.ofObj (fun (x : Unit) ↦ j) j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
x : Subtype (α := J) (ObjectProperty.ofObj fun (x : Unit) ↦ j)
k : J
hk : ObjectProperty.ofObj (fun (x : Unit) ↦ j) k
⊢ (fun (x : Unit) ↦
        (Subtype.mk (p := ObjectProperty.ofObj fun (x : Unit) ↦ j) j ⋯ :
          Subtype (α := J) (ObjectProperty.ofObj fun (x : Unit) ↦ j)))
      PUnit.unit =
    Subtype.mk (p := ObjectProperty.ofObj fun (x : Unit) ↦ j) k hk

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
x : Unit
⊢ Diagram.P (κ := κ) (Diagram.single j) j

Tactic:
simp