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₀ : (i : ι) → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun (i : ι) ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun (i : ι) ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1},
    fst := fun (x : { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }) ↦ PUnit.unit,
    snd := fun (x : { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }) ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun (x : shape.L) ↦ (↑x : ι × ι × J).2.2, right := fun (x : shape.R) ↦ m₁,
    fst := fun (x : shape.L) ↦ (D (↑x : ι × ι × J).1).isTerminal.lift ⋯ ≫ u (↑x : ι × ι × J).1,
    snd := fun (x : shape.L) ↦ (D (↑x : ι × ι × J).2.1).isTerminal.lift ⋯ ≫ u (↑x : ι × ι × J).2.1 }
hκ : Cardinal.aleph0 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
hshape : HasCardinalLT (Arrow (WalkingMultispan shape)) κ
c : Multicofork index := cocone index.multispan hshape
⊢ ∃ (m : J) (u : (i : ι) → (D i).top ⟶ m),
    (∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)) ∧
      ∀ (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₂

Tactic:
exact ⟨c.pt, fun i ↦ u i ≫ c.π ⟨⟩,
    fun i ↦ ⟨fun hi ↦ (hm₀ i).false (t₁ i ≫ c.π ⟨⟩ ≫ hi)⟩,
    fun i₁ i₂ j h₁ h₂ ↦ by simpa [index, shape] using c.condition ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩⟩
-- 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
simp :
  ∀ {i j : J} {f : i ⟶ j},
    (((⨆ (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 →
      (∃ (a : ι), (D a).P i) ∨ m = i
⊢ ∀ {i j : J} {f : i ⟶ j},
    ((D₁ D hι m).W ⊔
          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 →
      (D₁ D hι m).P i

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

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
i j : J
f : i ⟶ j
hf : (⨆ (i : ι), (D i).W) f
⊢ ∃ (i_1 : ι), (D i_1).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
i j : J
f : i ⟶ j
hf : ∃ (i_1 : ι), (D i_1).W f
inl : ∀ (i_1 : ι) (hf : (D i_1).W f), (∃ (a : ι), (D a).P i) ∨ m = i
⊢ (∃ (a : ι), (D a).P i) ∨ m = i

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
i_1 j : J
f : i_1 ⟶ j
i : ι
hf : (D i).W f
⊢ (∃ (a : ι), (D a).P i_1) ∨ m = i_1

Tactic:
Or.inl ⟨i, (D i).src hf⟩

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.toDiagram, Exists.intro, Or.inl
-- 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
i_1 j : J
f : i_1 ⟶ j
i : ι
hf : (D i).W f
⊢ (∃ (a : ι), (D a).P i_1) ∨ m = i_1

Tactic:
exact Or.inl ⟨i, (D i).src hf⟩

Premises used: Or.inl
-- 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
X Y : J
i : Unit
⊢ (∃ (a : ι), (D a).P m) ∨ m = m

Tactic:
Or.inr rfl

Premises used: Or.inr, rfl
-- 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
X Y : J
i : Unit
⊢ (∃ (a : ι), (D a).P m) ∨ m = m

Tactic:
exact Or.inr rfl

Premises used: Or.inr, rfl
-- 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
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ (a : ι),
      (D a).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)) ∨
    m =
      (↑(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)

Tactic:
Or.inl ⟨i, hj⟩

Premises used: Exists.intro, Or.inl
-- 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
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ (a : ι),
      (D a).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)) ∨
    m =
      (↑(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)

Tactic:
exact Or.inl ⟨i, hj⟩

Premises used: Or.inl
-- 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
simp :
  ∀ {i j : J} {f : i ⟶ j},
    (((⨆ (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 →
      (∃ (a : ι), (D a).P j) ∨ m = j
⊢ ∀ {i j : J} {f : i ⟶ j},
    ((D₁ D hι m).W ⊔
          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 →
      (D₁ D hι m).P j

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

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
i j : J
f : i ⟶ j
hf : ∃ (i_1 : ι), (D i_1).W f
inl : ∀ (i_1 : ι) (hf : (D i_1).W f), (∃ (a : ι), (D a).P j) ∨ m = j
⊢ (∃ (a : ι), (D a).P j) ∨ m = j

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
i_1 j : J
f : i_1 ⟶ j
i : ι
hf : (D i).W f
⊢ (∃ (a : ι), (D a).P j) ∨ m = j

Tactic:
Or.inl ⟨i, (D i).tgt hf⟩

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.toDiagram, Exists.intro, Or.inl
-- 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
i_1 j : J
f : i_1 ⟶ j
i : ι
hf : (D i).W f
⊢ (∃ (a : ι), (D a).P j) ∨ m = j

Tactic:
exact Or.inl ⟨i, (D i).tgt hf⟩

Premises used: Or.inl
-- 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
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ (a : ι), (D a).P m) ∨ m = m

Tactic:
Or.inr rfl

Premises used: Or.inr, rfl
-- 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
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ (a : ι), (D a).P m) ∨ m = m

Tactic:
exact Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ 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 = 𝟙 m
inl₁ : ∀ ⦃X Y : J⦄ (i : Unit), Eq (α := m ⟶ m) (𝟙 m) (𝟙 m)
inr :
  ∀
    (hf :
      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),
    f = 𝟙 m
⊢ f = 𝟙 m

Tactic:
obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ 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
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf : ∃ (i : ι), (D i).W f
inl : ∀ (i : ι) (hi : (D i).W f), f = 𝟙 m
⊢ f = 𝟙 m

Tactic:
obtain ⟨i, hi⟩ := hf
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
hi : (D i).W f
⊢ f = 𝟙 m

Tactic:
(hD ((D i).src hi)).elim

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, False.elim, 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
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
hi : (D i).W f
⊢ f = 𝟙 m

Tactic:
exact (hD ((D i).src hi)).elim

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, False.elim, 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
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
X Y : J
i : Unit
⊢ Eq (α := m ⟶ m) (𝟙 m) (𝟙 m)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf :
  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
⊢ ∃ (i : (i : ι) × Subtype (D i).P),
    Arrow.mk f =
      Arrow.mk
        ((D (i.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
          u (i.fst (β := fun (i : ι) ↦ Subtype (D i).P)))

Tactic:
rw [MorphismProperty.ofHoms_iff] at hf

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf :
  ∃ (i : (i : ι) × Subtype (D i).P),
    Arrow.mk f =
      Arrow.mk
        ((D (i.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
          u (i.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
inr :
  ∀ (i : ι) (j : J) (hj : (D i).P j)
    (hi :
      Arrow.mk f =
        Arrow.mk
          ((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))))),
    f = 𝟙 m
⊢ f = 𝟙 m

Tactic:
obtain ⟨⟨i, j, hj⟩, hi⟩ := hf
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
j : J
hj : (D i).P j
hi :
  Arrow.mk f =
    Arrow.mk
      ((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))))
⊢ m = j

Tactic:
congr_arg Arrow.leftFunc.obj hi

Premises used: CategoryTheory.Arrow.leftFunc, congr_arg, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
j : J
hj : (D i).P j
hi :
  Arrow.mk f =
    Arrow.mk
      ((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))))
⊢ (D i).P m

Tactic:
obtain rfl : m = j := congr_arg Arrow.leftFunc.obj hi

Premises used: CategoryTheory.Arrow.leftFunc, congr_arg, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
j : J
hj : (D i).P j
hi :
  Arrow.mk f =
    Arrow.mk
      ((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))))
hj₁ : (D i).P m
⊢ Arrow.mk f =
    Arrow.mk
      ((D
                (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                  (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m 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) m hj₁))))

Tactic:
obtain rfl : m = j := congr_arg Arrow.leftFunc.obj hi

Premises used: CategoryTheory.Arrow.leftFunc, congr_arg, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
hj : (D i).P m
hi :
  Arrow.mk f =
    Arrow.mk
      ((D
                (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                  (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m 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) m hj))))
⊢ f = 𝟙 m

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
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
hj : (D i).P m
hi :
  Arrow.mk f =
    Arrow.mk
      ((D
                (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                  (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m 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) m hj))))
⊢ f = 𝟙 m

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ι : Cardinal.mk ι < κ
⊢ HasCardinalLT ι κ

Tactic:
rw [← hasCardinalLT_iff_cardinal_mk_lt] at hι

Premises used: hasCardinalLT_iff_cardinal_mk_lt
-- 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 ι κ
obtain :
  ∀ (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₂),
    ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j
⊢ ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j

Tactic:
obtain ⟨m, u, hm₀, hm⟩ := isCardinalFiltered_aux J κ hJ D hι

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux