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))
hD : ∀ {i : ι}, ¬(D i).P m
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
this : (∃ (a : ι), (D a).P j) ∨ m = j
inl : ∀ (i : ι) (hi : (D i).P j), j = m
inr : ∀ (hj : (D₂ D hι u).IsTerminal m), m = m
⊢ j = m

Tactic:
obtain (⟨i, hi⟩ | rfl) := this

Premises used: 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
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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
i : ι
hi : (D i).P j
inl : False
⊢ j = m

Tactic:
exfalso
-- 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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
i : ι
hi : (D i).P j
⊢ (D₂ D hι u).P m

Tactic:
simp
-- 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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
i : ι
hi : (D i).P j
⊢ False

Tactic:
exact (hm₀ i).false (hj.lift (by simp) ≫ (D i).isTerminal.lift hi)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.lift, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.isTerminal, CategoryTheory.CategoryStruct.comp, IsEmpty.false
-- 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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
hj : (D₂ D hι u).IsTerminal m
⊢ m = m

Tactic:
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
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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
⊢ ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j

Tactic:
⟨D₂', fun i ↦ ⟨?_, ?_⟩⟩

Premises used: And.intro, Exists.intro
-- 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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
refine_1 : ∀ (i : ι), (D i).W ≤ D₂'.W
refine_2 : ∀ (i : ι), (D i).P ≤ D₂'.P
⊢ ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j

Tactic:
refine ⟨D₂', fun i ↦ ⟨?_, ?_⟩⟩
-- 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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).W ≤ (D i).W

Tactic:
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
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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).W ≤ D₂'.W

Tactic:
exact le_trans (le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left) le_sup_left

Premises used: le_sup_left, le_iSup, le_trans
-- 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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).P ≤ (D i).P

Tactic:
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
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
he : (D₂ D hι u).IsTerminal m :=
  have 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)) :=
    ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).P ≤ D₂'.P

Tactic:
exact le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left

Premises used: le_sup_left, le_iSup, le_trans
-- 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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁
i j : J
f : i ⟶ j
hf : (D₃ D m₁).W f
⊢ (D₃ D m₁).P i

Tactic:
(D₃ D m₁).src hf

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃
-- 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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁
i j : J
f : i ⟶ j
hf : (D₃ D m₁).W f
⊢ (D₃ D m₁).P i

Tactic:
exact (D₃ D m₁).src hf

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃
-- 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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁
X Y j : J
hj : D.P j
⊢ (D₃ D m₁).P (↑(Subtype.mk (p := D.P) j hj) : J)

Tactic:
Or.inl 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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁
X Y j : J
hj : D.P j
⊢ (D₃ D m₁).P (↑(Subtype.mk (p := D.P) j hj) : J)

Tactic:
exact Or.inl 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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁
i j : J
f : i ⟶ j
hf : (D₃ D m₁).W f
⊢ (D₃ D m₁).P j

Tactic:
(D₃ D m₁).tgt hf

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃
-- 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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁
i j : J
f : i ⟶ j
hf : (D₃ D m₁).W f
⊢ (D₃ D m₁).P j

Tactic:
exact (D₃ D m₁).tgt hf

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃
-- 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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁
X Y j : J
hj : D.P j
⊢ (D₃ D m₁).P m₁

Tactic:
Or.inr ⟨⟨⟩⟩

Premises used: CategoryTheory.ObjectProperty.ofObj.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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁
X Y j : J
hj : D.P j
⊢ (D₃ D m₁).P m₁

Tactic:
exact Or.inr ⟨⟨⟩⟩

Premises used: 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)
⊢ IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ

Tactic:
have := isCardinalFiltered J κ hJ
-- 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)
this : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
⊢ IsFiltered J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- 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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this : IsFiltered J
⊢ IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)

Tactic:
have := isFiltered_of_isCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
-- 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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
rw :
  (∀ (d : J), ∃ (c : DiagramWithUniqueTerminal J κ), Nonempty.{w + 1} (d ⟶ Functor.obj (functor J κ) c)) ∧
    ∀ {d : J} {c : DiagramWithUniqueTerminal J κ} (s s' : d ⟶ Functor.obj (functor J κ) c),
      ∃ (c' : DiagramWithUniqueTerminal J κ) (t : c ⟶ c'),
        s ≫ Functor.map (functor J κ) t = s' ≫ Functor.map (functor J κ) t
⊢ Functor.Final (C := DiagramWithUniqueTerminal J κ) (functor J κ)

Tactic:
rw [Functor.final_iff_of_isFiltered]

Premises used: CategoryTheory.Functor.final_iff_of_isFiltered
-- 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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
⊢ (∀ (d : J), ∃ (c : DiagramWithUniqueTerminal J κ), Nonempty.{w + 1} (d ⟶ Functor.obj (functor J κ) c)) ∧
    ∀ {d : J} {c : DiagramWithUniqueTerminal J κ} (s s' : d ⟶ Functor.obj (functor J κ) c),
      ∃ (c' : DiagramWithUniqueTerminal J κ) (t : c ⟶ c'),
        s ≫ Functor.map (functor J κ) t = s' ≫ Functor.map (functor J κ) t

Tactic:
⟨fun j ↦ ⟨.single j, ⟨𝟙 _⟩⟩, fun {j D} (f₁ f₂ : j ⟶ D.top) ↦ ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, Nonempty.intro, And.intro, Exists.intro, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.single
-- 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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
refine :
  ∀ {j : J} {D : DiagramWithUniqueTerminal J κ} (f₁ f₂ : j ⟶ D.top),
    ∃ (c' : DiagramWithUniqueTerminal J κ) (t : D ⟶ c'),
      Eq (α := j ⟶ Functor.obj (functor J κ) c') (f₁ ≫ Functor.map (functor J κ) t) (f₂ ≫ Functor.map (functor J κ) t)
⊢ (∀ (d : J), ∃ (c : DiagramWithUniqueTerminal J κ), Nonempty.{w + 1} (d ⟶ Functor.obj (functor J κ) c)) ∧
    ∀ {d : J} {c : DiagramWithUniqueTerminal J κ} (s s' : d ⟶ Functor.obj (functor J κ) c),
      ∃ (c' : DiagramWithUniqueTerminal J κ) (t : c ⟶ c'),
        s ≫ Functor.map (functor J κ) t = s' ≫ Functor.map (functor J κ) t

Tactic:
refine ⟨fun j ↦ ⟨.single j, ⟨𝟙 _⟩⟩, fun {j D} (f₁ f₂ : j ⟶ D.top) ↦ ?_⟩
-- 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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
obtain :
  ∀ (m₀ : J) (t : D.top ⟶ m₀) (hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)),
    ∃ (c' : DiagramWithUniqueTerminal J κ) (t : D ⟶ c'),
      Eq (α := j ⟶ Functor.obj (functor J κ) c') (f₁ ≫ Functor.map (functor J κ) t) (f₂ ≫ Functor.map (functor J κ) t)
⊢ ∃ (c' : DiagramWithUniqueTerminal J κ) (t : D ⟶ c'),
    Eq (α := j ⟶ Functor.obj (functor J κ) c') (f₁ ≫ Functor.map (functor J κ) t) (f₂ ≫ Functor.map (functor J κ) t)

Tactic:
obtain ⟨m₀, t, hm₀⟩ := hJ D.top

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.top
-- 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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
⊢ Eq (α := j ⟶ IsFiltered.coeq (f₁ ≫ t) (f₂ ≫ t)) (f₁ ≫ t ≫ IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t))
    (f₂ ≫ t ≫ IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t))

Tactic:
simpa using IsFiltered.coeq_condition (f₁ ≫ t) (f₂ ≫ t)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFiltered.coeq_condition