awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf :
  MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
    (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
    (fun (x : (i : ι) × Subtype (D i).P) ↦
      (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
        u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
    f
⊢ f = 𝟙 m
have hf₁ : ∃ (i : (i : ι) × Subtype (D i).P),
  Arrow.mk f =
    Arrow.mk
      ((D (i.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift sorry ≫
        u (i.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
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
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf :
  ∃ (i : (i : ι) × Subtype (D i).P),
    Arrow.mk f =
      Arrow.mk
        ((D (i.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
          u (i.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
⊢ f = 𝟙 m
have inr : ∀ (i : ι) (j : J) (hj : (D i).P j)
  (hi :
    Arrow.mk f =
      Arrow.mk
        ((D
                  (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                    (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj)))).isTerminal.lift
            sorry ≫
          u
            (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
              (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))))),
  f = 𝟙 m
Tactic: obtain ⟨⟨i, j, hj⟩, hi⟩ := 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
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
j : J
hj : (D i).P j
hi :
  Arrow.mk f =
    Arrow.mk
      ((D
                (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                  (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj)))).isTerminal.lift
          ⋯ ≫
        u
          (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
            (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))))
⊢ f = 𝟙 m
have hj₁ : (D i).P m
Tactic: obtain rfl : m = j := congr_arg Arrow.leftFunc.obj hi
Cleared hypotheses: j, hj, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
j : J
hj : (D i).P j
hi :
  Arrow.mk f =
    Arrow.mk
      ((D
                (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                  (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj)))).isTerminal.lift
          ⋯ ≫
        u
          (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
            (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))))
hj₁ : (D i).P m
⊢ f = 𝟙 m
have hi₁ : Arrow.mk f =
  Arrow.mk
    ((D
              (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m hj₁)))).isTerminal.lift
        sorry ≫
      u
        (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
          (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m hj₁))))
Tactic: obtain rfl : m = j := congr_arg Arrow.leftFunc.obj hi
Cleared hypotheses: j, hj, hi
-- 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ι : Cardinal.mk ι < κ
⊢ ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j
have hι₁ : HasCardinalLT ι κ
Tactic: rw [← hasCardinalLT_iff_cardinal_mk_lt] at hι
Cleared hypotheses: 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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
⊢ ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j
have obtain : ∀ (m : J) (u : (i : ι) → (D i).top ⟶ m) (hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top))
  (hm :
    ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
      (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂),
  ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j
Tactic: obtain ⟨m, u, hm₀, hm⟩ := isCardinalFiltered_aux J κ hJ D hι
-- 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))
⊢ ∃ (j : DiagramWithUniqueTerminal J κ), ∀ (k : ι), D k ≤ j
have hD : ∀ {i : ι}, ¬(D i).P m
Tactic: have hD {i : ι} : ¬ (D i).P m := fun hi ↦ (hm₀ i).false ((D i).isTerminal.lift hi)
-- 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
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf :
  (((⨆ (i : ι), (D i).W) ⊔
        MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
      MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
        (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
        fun (x : (i : ι) × Subtype (D i).P) ↦
        (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
          u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
    f
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
have inl : ∀ (hf : (⨆ (i : ι), (D i).W) f),
  f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
Tactic: obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨i', j, hj'⟩⟩) := 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
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf :
  (((⨆ (i : ι), (D i).W) ⊔
        MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
      MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
        (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
        fun (x : (i : ι) × Subtype (D i).P) ↦
        (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
          u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
    f
inl :
  ∀ (hf : (⨆ (i : ι), (D i).W) f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
have inl₁ : ∀ ⦃X Y : J⦄ (i_1 : Unit) (hj : (D i).P m),
  Eq (α := m ⟶ m) (𝟙 m) (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m hj)))
Tactic: obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨i', j, hj'⟩⟩) := 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)
ι : 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
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf :
  (((⨆ (i : ι), (D i).W) ⊔
        MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
      MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
        (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
        fun (x : (i : ι) × Subtype (D i).P) ↦
        (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift ⋯ ≫
          u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
    f
inl :
  ∀ (hf : (⨆ (i : ι), (D i).W) f),
    f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
inl₁ :
  ∀ ⦃X Y : J⦄ (i_1 : Unit) (hj : (D i).P m),
    Eq (α := m ⟶ m) (𝟙 m) (φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) m hj)))
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
have inr : ∀ ⦃X Y : J⦄ (i' : ι) (j : J) (hj' : (D i').P j)
  (hj :
    (D i).P
      (↑(Sigma.snd (β := fun (i : ι) ↦ Subtype (D i).P)
            (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) :
        J)),
  (D
              (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
                (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj')))).isTerminal.lift
        sorry ≫
      u
        (Sigma.fst (β := fun (i : ι) ↦ Subtype (D i).P)
          (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) =
    φ
      (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i
        (Subtype.mk (p := (D i).P)
          (↑(Sigma.snd (β := fun (i : ι) ↦ Subtype (D i).P)
                (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i' (Subtype.mk (p := (D i').P) j hj'))) :
            J)
          hj))
Tactic: obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨i', j, hj'⟩⟩) := 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)
ι : 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
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf : (⨆ (i : ι), (D i).W) f
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
have hf₁ : ∃ (i : ι), (D i).W f
Tactic: simp only [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
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf : ∃ (i : ι), (D i).W f
⊢ f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
have inl : ∀ (i_1 : ι) (hf : (D i_1).W f), f = φ (Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i (Subtype.mk (p := (D i).P) j hj))
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
⊢ (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))
Tactic: have H {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : (D₂ D hι u).W f) :
          f = φ ⟨i, ⟨_, hj⟩⟩ := by
        simp only [D₂_W] at hf
        obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨i', j, hj'⟩⟩) := hf
        · simp only [MorphismProperty.iSup_iff] at hf
          obtain ⟨i, hf⟩ := hf
          exact (hD ((D i).tgt hf)).elim
        · exact (hD hj).elim
        · apply hm
-- 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))
⊢ (D₂ D hι u).IsTerminal m
have refine_1 : (D₂ D hι u).W (𝟙 m)
Tactic: refine .ofExistsUnique ?_ ?_ ?_ ?_
-- 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))
refine_1 : (D₂ D hι u).W (𝟙 m)
⊢ (D₂ D hι u).IsTerminal m
have refine_2 : ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∃ (lift : j ⟶ m), (D₂ D hι u).W lift
Tactic: refine .ofExistsUnique ?_ ?_ ?_ ?_
-- 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))
refine_1 : (D₂ D hι u).W (𝟙 m)
refine_2 : ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∃ (lift : j ⟶ m), (D₂ D hι u).W lift
⊢ (D₂ D hι u).IsTerminal m
have refine_3 : ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∀ (l₁ l₂ : j ⟶ m), (D₂ D hι u).W l₁ → (D₂ D hι u).W l₂ → l₁ = l₂
Tactic: refine .ofExistsUnique ?_ ?_ ?_ ?_
-- 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))
refine_1 : (D₂ D hι u).W (𝟙 m)
refine_2 : ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∃ (lift : j ⟶ m), (D₂ D hι u).W lift
refine_3 : ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∀ (l₁ l₂ : j ⟶ m), (D₂ D hι u).W l₁ → (D₂ D hι u).W l₂ → l₁ = l₂
⊢ (D₂ D hι u).IsTerminal m
have refine_4 : ∀ ⦃i j : J⦄ (f : i ⟶ j),
  (D₂ D hι u).W f → ∃ (li : i ⟶ m) (lj : j ⟶ m), (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li
Tactic: refine .ofExistsUnique ?_ ?_ ?_ ?_
-- 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⦄, (D₂ D hι u).P j → ∃ (lift : j ⟶ m), (D₂ D hι u).W lift
have refine_2 : ∀ ⦃j : J⦄,
  (∃ (a : ι), (D a).P j) ∨ m = j →
    ∃ (lift : j ⟶ m),
      (((⨆ (i : ι), (D i).W) ⊔
            MorphismProperty.ofHoms (X := fun (x : Unit) ↦ m) (Y := fun (x : Unit) ↦ m) fun (x : Unit) ↦ 𝟙 m) ⊔
          MorphismProperty.ofHoms (X := fun (x : (i : ι) × Subtype (D i).P) ↦
            (↑(x.snd (β := fun (i : ι) ↦ Subtype (D i).P)) : J)) (Y := fun (x : (i : ι) × Subtype (D i).P) ↦ m)
            fun (x : (i : ι) × Subtype (D i).P) ↦
            (D (x.fst (β := fun (i : ι) ↦ Subtype (D i).P))).isTerminal.lift sorry ≫
              u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
        lift
Tactic: simp only [D₂_P, D₂_W]
-- 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 : J
hj : (D₂ D hι u).P j
l₁ l₂ : j ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
⊢ l₁ = l₂
have hj₁ : (∃ (a : ι), (D a).P j) ∨ m = j
Tactic: simp only [D₂_P] at hj
Cleared hypotheses: hj