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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
j : J
hj : D.P j
l₁ l₂ : j ⟶ m₁
hl₁ : (D₄ D φ).W l₁
hl₂ : (D₄ D φ).W l₂
inl :
  ∀ (hl₁ : (D₄ D φ).W (X := j) (φ (Subtype.mk (p := D.P) j hj) : (↑(Subtype.mk (p := D.P) j hj) : J) ⟶ m₁)),
    φ (Subtype.mk (p := D.P) j hj) = l₂
⊢ l₁ = l₂

Tactic:
obtain rfl := h₂ hj hl₁

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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
j : J
hj : D.P j
l₂ : j ⟶ m₁
hl₂ : (D₄ D φ).W l₂
hl₁ : (D₄ D φ).W (X := j) (φ (Subtype.mk (p := D.P) j hj) : (↑(Subtype.mk (p := D.P) j hj) : J) ⟶ m₁)
inl :
  ∀ (hl₂ : (D₄ D φ).W (X := j) (φ (Subtype.mk (p := D.P) j hj) : (↑(Subtype.mk (p := D.P) j hj) : J) ⟶ m₁)),
    Eq.{w + 1} (α := j ⟶ m₁) (φ (Subtype.mk (p := D.P) j hj) : (↑(Subtype.mk (p := D.P) j hj) : J) ⟶ m₁)
      (φ (Subtype.mk (p := D.P) j hj))
⊢ φ (Subtype.mk (p := D.P) j hj) = l₂

Tactic:
obtain rfl := h₂ hj hl₂

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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
j : J
hj : D.P j
hl₁ hl₂ : (D₄ D φ).W (X := j) (φ (Subtype.mk (p := D.P) j hj) : (↑(Subtype.mk (p := D.P) j hj) : J) ⟶ m₁)
⊢ Eq.{w + 1} (α := j ⟶ m₁) (φ (Subtype.mk (p := D.P) j hj) : (↑(Subtype.mk (p := D.P) j hj) : J) ⟶ m₁)
    (φ (Subtype.mk (p := D.P) j hj))

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)
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)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
l₁ l₂ : m₁ ⟶ m₁
hl₁ : (D₄ D φ).W l₁
hl₂ : (D₄ D φ).W l₂
inr : 𝟙 m₁ = l₂
inr₁ inr₂ : Eq (α := m₁ ⟶ m₁) (𝟙 m₁) (𝟙 m₁)
⊢ l₁ = l₂

Tactic:
rw [h₃ hl₁, h₃ hl₂]
-- 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_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
j k : J
f : j ⟶ k
hf : D.W f
⊢ ∃ (li : j ⟶ m₁) (lj : k ⟶ m₁), (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ f ≫ lj = li

Tactic:
⟨φ ⟨_, D.src hf⟩, φ ⟨_, D.tgt hf⟩,
          Or.inr ⟨_⟩, Or.inr ⟨_⟩, D.isTerminal.comm_assoc _ hf _⟩

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, Subtype.mk, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.toDiagram, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.isTerminal, And.intro, Exists.intro, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.comm_assoc, CategoryTheory.MorphismProperty.ofHoms.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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
j k : J
f : j ⟶ k
hf : D.W f
⊢ ∃ (li : j ⟶ m₁) (lj : k ⟶ m₁), (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ f ≫ lj = li

Tactic:
exact ⟨φ ⟨_, D.src hf⟩, φ ⟨_, D.tgt hf⟩,
          Or.inr ⟨_⟩, Or.inr ⟨_⟩, D.isTerminal.comm_assoc _ 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)
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)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
X Y : J
i : Unit
⊢ Eq (α := m₁ ⟶ m₁) (𝟙 m₁ ≫ 𝟙 m₁) (𝟙 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)
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)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
X Y : J
i : Unit
⊢ ∃ (li : m₁ ⟶ m₁) (lj : m₁ ⟶ m₁), (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ 𝟙 m₁ ≫ lj = li

Tactic:
exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by 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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
X Y j : J
hj : D.P j
⊢ Eq (α := (↑(Subtype.mk (p := D.P) j hj) : J) ⟶ m₁) (φ (Subtype.mk (p := D.P) j hj) ≫ 𝟙 m₁)
    (φ (Subtype.mk (p := D.P) j hj))

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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
X Y j : J
hj : D.P j
⊢ ∃ (li : (↑(Subtype.mk (p := D.P) j hj) : J) ⟶ m₁) (lj : m₁ ⟶ m₁),
    (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ φ (Subtype.mk (p := D.P) j hj) ≫ lj = li

Tactic:
exact ⟨φ ⟨_, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by 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)
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)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
⊢ ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ (Subtype.mk (p := D.P) j hj)

Tactic:
have lift_eq (j : J) (hj : D.P j) : hm₁.lift (Or.inl hj) = φ ⟨_, hj⟩ :=
    hm₁.uniq _ (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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ (Subtype.mk (p := D.P) j hj)
j : J
hj : (D₄ D φ).IsTerminal j
inl : ∀ (hj' : D.P j), j = m₁
inr : ∀ (i : Unit) (hj : (D₄ D φ).IsTerminal m₁), m₁ = m₁
⊢ j = m₁

Tactic:
obtain (hj' | ⟨⟨⟩⟩) := hj.prop

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.prop
-- 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_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ (Subtype.mk (p := D.P) j hj)
j : J
hj : (D₄ D φ).IsTerminal j
hj' : D.P j
⊢ j = m₁

Tactic:
hm₀.elim (u ≫ hj.lift (Or.inr ⟨⟨⟩⟩) ≫ D.isTerminal.lift hj')

Premises used: IsEmpty.elim, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.lift, CategoryTheory.ObjectProperty.ofObj.mk, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.isTerminal, CategoryTheory.CategoryStruct.comp, 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)
this_1 : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this_2 : IsFiltered J
this : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
j_1 : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j_1 ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty.{w + 1} (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ (Subtype.mk (p := D.P) j hj)
j : J
hj : (D₄ D φ).IsTerminal j
hj' : D.P j
⊢ j = m₁

Tactic:
exact hm₀.elim (u ≫ hj.lift (Or.inr ⟨⟨⟩⟩) ≫ D.isTerminal.lift 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_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)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ (Subtype.mk (p := D.P) j hj)
i : Unit
hj : (D₄ D φ).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)
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)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ (Subtype.mk (p := D.P) j hj)
D₄' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₄ D φ;
  { toDiagram := __Diagram, top := m₁, isTerminal := hm₁, uniq_terminal := ⋯ }
⊢ Eq (α := j ⟶ Functor.obj (functor J κ) D₄') (f₁ ≫ Functor.map (functor J κ) (homOfLE ⋯))
    (f₂ ≫ Functor.map (functor J κ) (homOfLE ⋯))

Tactic:
simpa [functorMap, D₄', lift_eq _ D.isTerminal.prop, φ]

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.prop, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.isTerminal
-- 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)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → (↑x : J) ⟶ m₁ := fun (x : Subtype D.P) ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ (Subtype.mk (p := D.P) j hj)
D₄' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₄ D φ;
  { toDiagram := __Diagram, top := m₁, isTerminal := hm₁, uniq_terminal := ⋯ }
⊢ ∃ (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:
exact ⟨D₄', homOfLE ⟨le_sup_left.trans le_sup_left, le_sup_left⟩,
    by simpa [functorMap, D₄', lift_eq _ D.isTerminal.prop, φ]⟩
-- 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) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : α ⥤ J), F.Final

Tactic:
⟨DiagramWithUniqueTerminal J κ, _, isCardinalFiltered J κ hJ,
    functor J κ, final_functor J κ hJ⟩

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.final_functor, Exists.intro, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
⊢ IsFiltered.{w, w} κ.ord.ToType

Tactic:
have := isFiltered_of_isCardinalFiltered κ.ord.ToType κ
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
this : IsFiltered.{w, w} κ.ord.ToType
x_1 : J × κ.ord.ToType
j : J
x : κ.ord.ToType
x_2 : (j, Order.succ x) ⟶ (j, x)
fst : (j, Order.succ x).1 ⟶ (j, x).1
f : (j, Order.succ x).2 ⟶ (j, x).2
⊢ NoMaxOrder.{w} κ.ord.ToType

Tactic:
have : NoMaxOrder κ.ord.ToType :=
          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
this_1 : IsFiltered.{w, w} κ.ord.ToType
x_1 : J × κ.ord.ToType
j : J
x : κ.ord.ToType
x_2 : (j, Order.succ x) ⟶ (j, x)
fst : (j, Order.succ x).1 ⟶ (j, x).1
f : (j, Order.succ x).2 ⟶ (j, x).2
this : NoMaxOrder.{w} κ.ord.ToType
⊢ False

Tactic:
not_isMax _ (Order.max_of_succ_le (leOfHom f))

Premises used: not_isMax, Order.max_of_succ_le, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
this_1 : IsFiltered.{w, w} κ.ord.ToType
x_1 : J × κ.ord.ToType
j : J
x : κ.ord.ToType
x_2 : (j, Order.succ x) ⟶ (j, x)
fst : (j, Order.succ x).1 ⟶ (j, x).1
f : (j, Order.succ x).2 ⟶ (j, x).2
this : NoMaxOrder.{w} κ.ord.ToType
⊢ False

Tactic:
exact not_isMax _ (Order.max_of_succ_le (leOfHom f))

Premises used: not_isMax, Order.max_of_succ_le, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
this : IsFiltered.{w, w} κ.ord.ToType
obtain :
  ∀ (α : Type w) (w : PartialOrder α),
    IsCardinalFiltered α κ →
      ∀ (F : α ⥤ J × κ.ord.ToType),
        F.Final → ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : α ⥤ J), F.Final
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : α ⥤ J), F.Final

Tactic:
obtain ⟨α, _, _, F, _⟩ :=
    exists_cardinal_directed.aux (J × κ.ord.ToType) κ (fun ⟨j, x⟩ ↦
      ⟨⟨j, Order.succ x⟩, (𝟙 _, homOfLE (Order.le_succ x)), ⟨fun ⟨_, f⟩ ↦ by
        have : NoMaxOrder κ.ord.ToType :=
          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
        exact not_isMax _ (Order.max_of_succ_le (leOfHom f))⟩⟩)

Premises used: False, _private.0.CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.match_2, Order.succ, Quiver.Hom, Exists, CategoryTheory.CategoryStruct.id, Prod.mk, IsEmpty, IsEmpty.mk, Prod.fst, Cardinal.ord, CategoryTheory.homOfLE, _private.0.CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.match_1, Exists.intro, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.aux, Order.le_succ, Prod, Ordinal.ToType
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
this : IsFiltered.{w, w} κ.ord.ToType
α : Type w
w : PartialOrder α
w_1 : IsCardinalFiltered α κ
F : α ⥤ J × κ.ord.ToType
h : F.Final
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : α ⥤ J), F.Final

Tactic:
⟨_, _, inferInstance, F ⋙ Prod.fst _ _, inferInstance⟩

Premises used: CategoryTheory.Functor.comp, inferInstance, Exists.intro, CategoryTheory.Prod.fst
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
this : IsFiltered.{w, w} κ.ord.ToType
α : Type w
w : PartialOrder α
w_1 : IsCardinalFiltered α κ
F : α ⥤ J × κ.ord.ToType
h : F.Final
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : α ⥤ J), F.Final

Tactic:
exact ⟨_, _, inferInstance, F ⋙ Prod.fst _ _, inferInstance⟩