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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
j : J
l₁ l₂ : j ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
hj : (∃ (a : ι), (D a).P j) ∨ m = j
⊢ l₁ = l₂
have refine_3 : ∀ (i : ι) (hj : (D i).P j), l₁ = l₂
Tactic: obtain (⟨i, hj⟩ | rfl) := hj
Cleared hypotheses: hj
-- 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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
j : J
l₁ l₂ : j ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
hj : (∃ (a : ι), (D a).P j) ∨ m = j
refine_3 : ∀ (i : ι) (hj : (D i).P j), l₁ = l₂
⊢ l₁ = l₂
have refine_3₁ : ∀ (l₁ l₂ : m ⟶ m) (hl₁ : (D₂ D hι u).W l₁) (hl₂ : (D₂ D hι u).W l₂), l₁ = l₂
Tactic: obtain (⟨i, hj⟩ | rfl) := hj
Cleared hypotheses: j, l₁, l₂, hl₁, hl₂, hj
-- 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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
j : J
l₁ l₂ : j ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
i : ι
hj : (D i).P j
⊢ l₁ = l₂
have refine_3 : ∀
  (hl₁ :
    (D₂ D hι u).W (X := j)
      (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj)) :
        (↑(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.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
j : J
l₂ : j ⟶ m
hl₂ : (D₂ D hι u).W l₂
i : ι
hj : (D i).P j
hl₁ :
  (D₂ D hι u).W (X := j)
    (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj)) :
      (↑(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.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj)) = l₂
have refine_3 : ∀
  (hl₂ :
    (D₂ D hι u).W (X := j)
      (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj)) :
        (↑(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)),
  Eq.{w + 1} (α := j ⟶ m)
    (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj)) :
      (↑(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.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
l₁ l₂ : m ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
⊢ l₁ = l₂
have refine_3 : 𝟙 m = l₂
Tactic: rw [eq_id_of_D₂_W D hι u hD hl₁, eq_id_of_D₂_W D hι u hD 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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
l₁ l₂ : m ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
refine_3 : 𝟙 m = l₂
⊢ l₁ = l₂
have refine_3₁ : Eq (α := m ⟶ m) (𝟙 m) (𝟙 m)
Tactic: rw [eq_id_of_D₂_W D hι u hD hl₁, eq_id_of_D₂_W D hι u hD 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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
j k : J
f : j ⟶ k
hf : Diagram.W (Diagram.iSup (fun (i : ι) ↦ (D i).toDiagram) hι) f
⊢ ∃ (li : j ⟶ m) (lj : k ⟶ m), (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li
have hf₁ : ∃ (i : ι), (D i).W f
Tactic: simp only [Diagram.iSup_W, MorphismProperty.iSup_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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J) ⟶ m :=
  fun (x : (i : ι) × Subtype (D i).P) ↦
    (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫ u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))
hD : ∀ {i : ι}, ¬(D i).P m
H :
  ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
j k : J
f : j ⟶ k
hf : ∃ (i : ι), (D i).W f
⊢ ∃ (li : j ⟶ m) (lj : k ⟶ m), (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li
have refine_4 : ∀ (i : ι) (hf : (D i).W f), ∃ (li : j ⟶ m) (lj : k ⟶ m), (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li
Tactic: obtain ⟨i, 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)
ι : 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
⊢ j = m
have this : (D₂ D hι u).P j
Tactic: have := hj.prop
-- 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)
ι : 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 : (D₂ D hι u).P j
⊢ j = m
have this₁ : (∃ (a : ι), (D a).P j) ∨ m = j
Tactic: simp only [D₂_P] at this
Cleared hypotheses: this
-- 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)
ι : 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
⊢ j = m
have inl : ∀ (i : ι) (hi : (D i).P j), j = m
Tactic: obtain (⟨i, hi⟩ | rfl) := this
Cleared hypotheses: this
-- 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)
ι : 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
⊢ j = m
have inr : ∀ (hj : (D₂ D hι u).IsTerminal m), m = m
Tactic: obtain (⟨i, hi⟩ | rfl) := this
Cleared hypotheses: j, hj, this
-- 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)
ι : 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
⊢ j = m
have inl : False
Tactic: exfalso
-- 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)
ι : 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
have refine_1 : ∀ (i : ι), (D i).W ≤ D₂'.W
Tactic: refine ⟨D₂', fun i ↦ ⟨?_, ?_⟩⟩
-- 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)
ι : 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
⊢ ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j
have refine_2 : ∀ (i : ι), (D i).P ≤ D₂'.P
Tactic: refine ⟨D₂', fun i ↦ ⟨?_, ?_⟩⟩
-- 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)
⊢ Functor.Final (C := DiagramWithUniqueTerminal J κ) (functor J κ)
have this : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
Tactic: have := isCardinalFiltered 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 κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
this : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
⊢ Functor.Final (C := DiagramWithUniqueTerminal J κ) (functor J κ)
have this₁ : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- 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 : IsFiltered J
⊢ Functor.Final (C := DiagramWithUniqueTerminal J κ) (functor J κ)
have this₁ : IsFiltered.{w, w} (DiagramWithUniqueTerminal J κ)
Tactic: have := isFiltered_of_isCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
-- 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 κ)
⊢ Functor.Final (C := DiagramWithUniqueTerminal J κ) (functor J κ)
have 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
Tactic: rw [Functor.final_iff_of_isFiltered]
-- 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 κ)
⊢ (∀ (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
have 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)
Tactic: refine ⟨fun j ↦ ⟨.single j, ⟨𝟙 _⟩⟩, fun {j D} (f₁ f₂ : j ⟶ D.top) ↦ ?_⟩