awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
⊢ ∀ {i : ι}, ¬(D i).P m

Tactic:
have hD {i : ι} : ¬ (D i).P m := fun hi ↦ (hm₀ i).false ((D i).isTerminal.lift hi)
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf :
  (((⨆ (i : ι), (D i).W) ⊔
        MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
      MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
        (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
        fun (x : (i : ι) × Subtype (D i).P) ↦
        (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
          u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
    f
inl :
  ∀ (hf : (⨆ (i : ι), (D i).W) f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
inl₁ :
  ∀ ⦃X Y : J⦄ (i_1 : Unit) (hj : (D i).P m),
    Eq (α := m ⟶ m) (𝟙 m) (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m hj)))
inr :
  ∀ ⦃X Y : J⦄ (i' : ι) (j : J) (hj' : (D i').P j)
    (hj :
      (D i).P
        (↑(Sigma.snd (β := fun (i : ι) ↦ Subtype (D i).P)
              (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) :
          J)),
    (D
                (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                  (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i'
                    (Subtype.mk (p := (D i').P) j hj')))).isTerminal.lift
          ⋯ ≫
        u
          (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
            (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) =
      φ
        (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i
          (Subtype.mk (p := (D i).P)
            (↑(Sigma.snd (β := fun (i : ι) ↦ Subtype (D i).P)
                  (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) :
              J)
            hj))
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))

Tactic:
obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨i', j, hj'⟩⟩) := hf
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf : (⨆ (i : ι), (D i).W) f
⊢ ∃ (i : ι), (D i).W f

Tactic:
simp only [MorphismProperty.iSup_iff] at hf

Premises used: CategoryTheory.MorphismProperty.iSup_iff
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf : ∃ (i : ι), (D i).W f
inl :
  ∀ (i_1 : ι) (hf : (D i_1).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))

Tactic:
obtain ⟨i, hf⟩ := hf
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
i_1 : ι
j : J
hj : (D i_1).P j
f : j ⟶ m
i : ι
hf : (D i).W f
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i_1 (Subtype.mk (p := (D i_1).P) j hj))

Tactic:
(hD ((D i).tgt hf)).elim

Premises used: False.elim, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.toDiagram
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
i_1 : ι
j : J
hj : (D i_1).P j
f : j ⟶ m
i : ι
hf : (D i).W f
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i_1 (Subtype.mk (p := (D i_1).P) j hj))

Tactic:
exact (hD ((D i).tgt hf)).elim

Premises used: False.elim, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.toDiagram
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
X Y : J
i_1 : Unit
hj : (D i).P m
⊢ Eq (α := m ⟶ m) (𝟙 m) (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m hj)))

Tactic:
(hD hj).elim

Premises used: False.elim
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
X Y : J
i_1 : Unit
hj : (D i).P m
⊢ Eq (α := m ⟶ m) (𝟙 m) (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m hj)))

Tactic:
exact (hD hj).elim

Premises used: False.elim
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
X Y : J
i' : ι
j : J
hj' : (D i').P j
hj :
  (D i).P
    (↑(Sigma.snd (β := fun (i : ι) ↦ Subtype (D i).P)
          (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) :
      J)
⊢ (D
              (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj')))).isTerminal.lift
        ⋯ ≫
      u
        (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
          (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) =
    φ
      (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i
        (Subtype.mk (p := (D i).P)
          (↑(Sigma.snd (β := fun (i : ι) ↦ Subtype (D i).P)
                (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) :
            J)
          hj))

Tactic:
apply hm
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
⊢ ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))

Tactic:
have H {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f) :
          f = φ ⟨i, ⟨_, hj⟩⟩ := by
        simp only [D₂_W] at hf
        obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨i', j, hj'⟩⟩) := hf
        · simp only [MorphismProperty.iSup_iff] at hf
          obtain ⟨i, hf⟩ := hf
          exact (hD ((D i).tgt hf)).elim
        · exact (hD hj).elim
        · apply hm
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
refine_1 : (D₂ D hι u).W (𝟙 m)
refine_2 : ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∃ (lift : j ⟶ m), (D₂ D hι u).W lift
refine_3 : ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∀ (l₁ l₂ : j ⟶ m), (D₂ D hι u).W l₁ → (D₂ D hι u).W l₂ → l₁ = l₂
refine_4 :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    (D₂ D hι u).W f → ∃ (li : i ⟶ m) (lj : j ⟶ m), (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li
⊢ (D₂ D hι u).IsTerminal m

Tactic:
refine .ofExistsUnique ?_ ?_ ?_ ?_
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
⊢ (D₂ D hι u).W (𝟙 m)

Tactic:
Or.inl (Or.inr ⟨⟨⟩⟩)

Premises used: CategoryTheory.MorphismProperty.ofHoms.mk, Or.inl, Or.inr
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
⊢ (D₂ D hι u).W (𝟙 m)

Tactic:
exact Or.inl (Or.inr ⟨⟨⟩⟩)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
refine_2 :
  ∀ ⦃j : J⦄,
    (∃ (a : ι), (D a).P j) ∨ m = j →
      ∃ (lift : j ⟶ m),
        (((⨆ (i : ι), (D i).W) ⊔
              MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
            MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
              (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
              fun (x : (i : ι) × Subtype (D i).P) ↦
              (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
                u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
          lift
⊢ ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∃ (lift : j ⟶ m), (D₂ D hι u).W lift

Tactic:
simp only [D₂_P, D₂_W]

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_P
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
j : J
i : ι
hi : (D i).P j
⊢ ∃ (lift : j ⟶ m),
    (((⨆ (i : ι), (D i).W) ⊔
          MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
        MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
          (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
          fun (x : (i : ι) × Subtype (D i).P) ↦
          (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
            u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
      lift

Tactic:
⟨φ ⟨i, _, hi⟩, Or.inr (.mk _)⟩

Premises used: Subtype.mk, Exists.intro, CategoryTheory.MorphismProperty.ofHoms.mk, Sigma.mk, Or.inr
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
j : J
i : ι
hi : (D i).P j
⊢ ∃ (lift : j ⟶ m),
    (((⨆ (i : ι), (D i).W) ⊔
          MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
        MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
          (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
          fun (x : (i : ι) × Subtype (D i).P) ↦
          (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
            u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
      lift

Tactic:
exact ⟨φ ⟨i, _, hi⟩, Or.inr (.mk _)⟩
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
⊢ ∃ (lift : m ⟶ m),
    (((⨆ (i : ι), (D i).W) ⊔
          MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
        MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
          (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
          fun (x : (i : ι) × Subtype (D i).P) ↦
          (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
            u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
      lift

Tactic:
⟨𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩)⟩

Premises used: CategoryTheory.CategoryStruct.id, Exists.intro, CategoryTheory.MorphismProperty.ofHoms.mk, Or.inl, Or.inr