awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨m₀, t, hm₀⟩ := hJ D.top
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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)
⊢ ∃ (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)
have obtain : ∀ (m₁ : J) (u : m₀ ⟶ m₁) (hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u),
  ∃ (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₁, u, hu⟩ : ∃ (m₁ : J) (u : m₀ ⟶ m₁), f₁ ≫ t ≫ u = f₂ ≫ t ≫ u :=
    ⟨_, IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t),
      by simpa using IsFiltered.coeq_condition (f₁ ≫ t) (f₂ ≫ t)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
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
⊢ ∃ (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)
have h₁ : ¬D.P m₁
Tactic: have h₁ : ¬ (D.P m₁) := fun h₁ ↦ hm₀.false (u ≫ D.isTerminal.lift h₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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
j : J
hj : D.P j
f : j ⟶ m₁
hf : (D₄ D φ).W f
⊢ f = φ (Subtype.mk (p := D.P) j hj)
have inl : ∀ (hf : D.W f), f = φ (Subtype.mk (p := D.P) j hj)
Tactic: obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨⟩⟩) := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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
j : J
hj : D.P j
f : j ⟶ m₁
hf : (D₄ D φ).W f
inl : ∀ (hf : D.W f), f = φ (Subtype.mk (p := D.P) j hj)
⊢ f = φ (Subtype.mk (p := D.P) j hj)
have inl₁ : ∀ ⦃X Y : J⦄ (i : Unit) (hj : D.P m₁), Eq (α := m₁ ⟶ m₁) (𝟙 m₁) (φ (Subtype.mk (p := D.P) m₁ hj))
Tactic: obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨⟩⟩) := hf
Cleared hypotheses: j, hj, f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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
j : J
hj : D.P j
f : j ⟶ m₁
hf : (D₄ D φ).W f
inl : ∀ (hf : D.W f), f = φ (Subtype.mk (p := D.P) j hj)
inl₁ : ∀ ⦃X Y : J⦄ (i : Unit) (hj : D.P m₁), Eq (α := m₁ ⟶ m₁) (𝟙 m₁) (φ (Subtype.mk (p := D.P) m₁ hj))
⊢ f = φ (Subtype.mk (p := D.P) j hj)
have inr : ∀ ⦃X Y : J⦄ (i : Subtype D.P) (hj : D.P (↑i : J)), φ i = φ (Subtype.mk (p := D.P) (↑i : J) hj)
Tactic: obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨⟩⟩) := hf
Cleared hypotheses: j, hj, f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
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
⊢ ∃ (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)
have h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f), f = φ (Subtype.mk (p := D.P) j hj)
Tactic: have h₂ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f) :
      f = φ ⟨_, hj⟩ := by
    obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨⟩⟩) := hf
    · exact (h₁ (D.tgt hf)).elim
    · exact (h₁ hj).elim
    · rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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)
f : m₁ ⟶ m₁
hf : (D₄ D φ).W f
⊢ f = 𝟙 m₁
have inl : ∀ (hf : D.W f), f = 𝟙 m₁
Tactic: obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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)
f : m₁ ⟶ m₁
hf : (D₄ D φ).W f
inl : ∀ (hf : D.W f), f = 𝟙 m₁
⊢ f = 𝟙 m₁
have inl₁ : ∀ ⦃X Y : J⦄ (i : Unit), Eq (α := m₁ ⟶ m₁) (𝟙 m₁) (𝟙 m₁)
Tactic: obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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)
f : m₁ ⟶ m₁
hf : (D₄ D φ).W f
inl : ∀ (hf : D.W f), f = 𝟙 m₁
inl₁ : ∀ ⦃X Y : J⦄ (i : Unit), Eq (α := m₁ ⟶ m₁) (𝟙 m₁) (𝟙 m₁)
⊢ f = 𝟙 m₁
have inr : ∀ (hf : MorphismProperty.ofHoms φ f), f = 𝟙 m₁
Tactic: obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
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)
f : m₁ ⟶ m₁
hf : MorphismProperty.ofHoms φ f
⊢ f = 𝟙 m₁
have hf₁ : ∃ (i : Subtype D.P), Arrow.mk f = Arrow.mk (φ i)
Tactic: rw [MorphismProperty.ofHoms_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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)
f : m₁ ⟶ m₁
hf : ∃ (i : Subtype D.P), Arrow.mk f = Arrow.mk (φ i)
⊢ f = 𝟙 m₁
have inr : ∀ (j : J) (hj : D.P j)
  (hf : Arrow.mk f = Arrow.mk (X := (↑(Subtype.mk (p := D.P) j hj) : J)) (φ (Subtype.mk (p := D.P) j hj))), f = 𝟙 m₁
Tactic: obtain ⟨⟨j, hj⟩, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
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)
f : m₁ ⟶ m₁
j : J
hj : D.P j
hf : Arrow.mk f = Arrow.mk (X := (↑(Subtype.mk (p := D.P) j hj) : J)) (φ (Subtype.mk (p := D.P) j hj))
⊢ f = 𝟙 m₁
have hj₁ : D.P m₁
Tactic: obtain rfl : m₁ = j := congr_arg Arrow.leftFunc.obj hf
Cleared hypotheses: j, hj, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
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)
f : m₁ ⟶ m₁
j : J
hj : D.P j
hf : Arrow.mk f = Arrow.mk (X := (↑(Subtype.mk (p := D.P) j hj) : J)) (φ (Subtype.mk (p := D.P) j hj))
hj₁ : D.P m₁
⊢ f = 𝟙 m₁
have hf₁ : Arrow.mk f = Arrow.mk (X := (↑(Subtype.mk (p := D.P) m₁ hj₁) : J)) (φ (Subtype.mk (p := D.P) m₁ hj₁))
Tactic: obtain rfl : m₁ = j := congr_arg Arrow.leftFunc.obj hf
Cleared hypotheses: j, hj, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
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)
⊢ ∃ (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)
have h₃ : ∀ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f), f = 𝟙 m₁
Tactic: have h₃ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f) : f = 𝟙 _ := by
    obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
    · exact (h₁ (D.src hf)).elim
    · rfl
    · rw [MorphismProperty.ofHoms_iff] at hf
      obtain ⟨⟨j, hj⟩, hf⟩ := hf
      obtain rfl : m₁ = j := congr_arg Arrow.leftFunc.obj hf
      exact (h₁ hj).elim
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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₂
⊢ l₁ = l₂
have 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₂
Tactic: obtain rfl := h₂ hj hl₁
Cleared hypotheses: l₁, hl₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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₁)
⊢ φ (Subtype.mk (p := D.P) j hj) = l₂
have 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))
Tactic: obtain rfl := h₂ hj hl₂
Cleared hypotheses: l₂, hl₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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₂
⊢ l₁ = l₂
have inr : 𝟙 m₁ = l₂
Tactic: rw [h₃ hl₁, h₃ hl₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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₂
⊢ l₁ = l₂
have inr₁ : Eq (α := m₁ ⟶ m₁) (𝟙 m₁) (𝟙 m₁)
Tactic: rw [h₃ hl₁, h₃ hl₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
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 ⋯ ⋯ ⋯ ⋯
⊢ ∃ (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)
have lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift sorry = φ (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 ⟨_⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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
⊢ j = m₁
have inl : ∀ (hj' : D.P j), j = m₁
Tactic: obtain (hj' | ⟨⟨⟩⟩) := hj.prop
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
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₁
⊢ j = m₁
have inr : ∀ (i : Unit) (hj : (D₄ D φ).IsTerminal m₁), m₁ = m₁
Tactic: obtain (hj' | ⟨⟨⟩⟩) := hj.prop
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : α ⥤ J), F.Final
have this : IsFiltered.{w, w} κ.ord.ToType
Tactic: have := isFiltered_of_isCardinalFiltered κ.ord.ToType κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
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
⊢ False
have this₁ : NoMaxOrder.{w} κ.ord.ToType
Tactic: have : NoMaxOrder κ.ord.ToType :=
          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)