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}
D₂ : DiagramWithUniqueTerminal J κ
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
hW : { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W = D₂.W
hP : { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P = D₂.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } = D₂
have obtain : ∀ (D₂ : Diagram J κ) (top' : J) (h₂ : D₂.IsTerminal top') (h₂' : ∀ (j : J) (hj : D₂.IsTerminal j), j = top')
  (hW :
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
      { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W)
  (hP :
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
      { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P),
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }
Tactic: obtain ⟨D₂, top', h₂, h₂'⟩ := D₂
Cleared hypotheses: D₂, hW, hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
D₂ : Diagram J κ
top' : J
h₂ : D₂.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₂.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }
have obtain : ∀ (h₂ : D₁.IsTerminal top') (h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top')
  (hW :
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
      { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W)
  (hP :
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
      { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P),
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }
Tactic: obtain rfl : D₁ = D₂ := by aesop
Cleared hypotheses: D₂, h₂, h₂', hW, hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
top' : J
h₂ : D₁.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }
have obtain : ∀ (h₂ : D₁.IsTerminal top) (h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top)
  (hW :
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
      { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W)
  (hP :
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
      { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P),
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' }
Tactic: obtain rfl : top = top' := h₂' _ h₁
Cleared hypotheses: top', h₂, h₂', hW, hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
h₂ : D₁.IsTerminal top
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' }
have obtain : ∀
  (hW :
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.W =
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.W)
  (hP :
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ }.P =
      { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' : DiagramWithUniqueTerminal J κ }.P),
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' : DiagramWithUniqueTerminal J κ } =
    { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₂' }
Tactic: obtain rfl : h₁ = h₂ := by subsingleton
Cleared hypotheses: h₂, hW, hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x x_1 : DiagramWithUniqueTerminal J κ
h₁ : x.W ≤ x_1.W ∧ x.P ≤ x_1.P
h₂ : x_1.W ≤ x.W ∧ x_1.P ≤ x.P
⊢ x = x_1
have hW : x.W = x_1.W
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
x x_1 : DiagramWithUniqueTerminal J κ
h₁ : x.W ≤ x_1.W ∧ x.P ≤ x_1.P
h₂ : x_1.W ≤ x.W ∧ x_1.P ≤ x.P
hW : x.W = x_1.W
⊢ x = x_1
have hP : x.P = x_1.P
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
f : Arrow J
hf :
  Membership.mem (γ := Set (Arrow J))
    (MorphismProperty.toSet
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
    f
⊢ ∃ (a : Unit),
    (fun (x : Unit) ↦
          (Subtype.mk (p := fun (x : Arrow J) ↦
              Membership.mem (γ := Set (Arrow J))
                (MorphismProperty.toSet
                  (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                x)
              (Arrow.mk (𝟙 j)) ⋯ :
            { x : Arrow J //
              Membership.mem (γ := Set (Arrow J))
                (MorphismProperty.toSet
                  (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                x }))
        a =
      Subtype.mk (p := fun (x : Arrow J) ↦
        Membership.mem (γ := Set (Arrow J))
          (MorphismProperty.toSet
            (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
          x)
        f hf
have refine : (fun (x : Unit) ↦
      (Subtype.mk (p := fun (x : Arrow J) ↦
          Membership.mem (γ := Set (Arrow J))
            (MorphismProperty.toSet
              (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
            x)
          (Arrow.mk (𝟙 j)) sorry :
        { x : Arrow J //
          Membership.mem (γ := Set (Arrow J))
            (MorphismProperty.toSet
              (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
            x }))
    PUnit.unit =
  Subtype.mk (p := fun (x : Arrow J) ↦
    Membership.mem (γ := Set (Arrow J))
      (MorphismProperty.toSet
        (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
      x)
    f hf
Tactic: refine ⟨⟨⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
f : Arrow J
hf :
  Membership.mem (γ := Set (Arrow J))
    (MorphismProperty.toSet
      (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
    f
⊢ (fun (x : Unit) ↦
        (Subtype.mk (p := fun (x : Arrow J) ↦
            Membership.mem (γ := Set (Arrow J))
              (MorphismProperty.toSet
                (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
              x)
            (Arrow.mk (𝟙 j)) ⋯ :
          { x : Arrow J //
            Membership.mem (γ := Set (Arrow J))
              (MorphismProperty.toSet
                (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
              x }))
      PUnit.unit =
    Subtype.mk (p := fun (x : Arrow J) ↦
      Membership.mem (γ := Set (Arrow J))
        (MorphismProperty.toSet
          (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
        x)
      f hf
have a : (↑((fun (x : Unit) ↦
          (Subtype.mk (p := fun (x : Arrow J) ↦
              Membership.mem (γ := Set (Arrow J))
                (MorphismProperty.toSet
                  (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                x)
              (Arrow.mk (𝟙 j)) sorry :
            { x : Arrow J //
              Membership.mem (γ := Set (Arrow J))
                (MorphismProperty.toSet
                  (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
                x }))
        PUnit.unit) :
    Arrow J) =
  (↑(Subtype.mk (p := fun (x : Arrow J) ↦
        Membership.mem (γ := Set (Arrow J))
          (MorphismProperty.toSet
            (MorphismProperty.ofHoms (X := fun (x : Unit) ↦ j) (Y := fun (x : Unit) ↦ j) fun (x : Unit) ↦ 𝟙 j))
          x)
        f hf) :
    Arrow J)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
⊢ __Diagram.IsTerminal j
have refine_1 : ∀ (x : J) (h : __Diagram.P x), ∃ (lift : x ⟶ j), __Diagram.W lift
Tactic: refine .ofExistsUnique ⟨⟨⟩⟩ (fun _ h ↦ ?_) (fun _ h₁ _ _ h₂ h₃ ↦ ?_) (fun _ _ _ h ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
refine_1 : ∀ (x : J) (h : __Diagram.P x), ∃ (lift : x ⟶ j), __Diagram.W lift
⊢ __Diagram.IsTerminal j
have refine_2 : ∀ (x : J) (h₁ : __Diagram.P x) (x_1 x_2 : x ⟶ j) (h₂ : __Diagram.W x_1) (h₃ : __Diagram.W x_2), x_1 = x_2
Tactic: refine .ofExistsUnique ⟨⟨⟩⟩ (fun _ h ↦ ?_) (fun _ h₁ _ _ h₂ h₃ ↦ ?_) (fun _ _ _ h ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
refine_1 : ∀ (x : J) (h : __Diagram.P x), ∃ (lift : x ⟶ j), __Diagram.W lift
refine_2 : ∀ (x : J) (h₁ : __Diagram.P x) (x_1 x_2 : x ⟶ j) (h₂ : __Diagram.W x_1) (h₃ : __Diagram.W x_2), x_1 = x_2
⊢ __Diagram.IsTerminal j
have refine_3 : ∀ (x x_1 : J) (x_2 : x ⟶ x_1) (h : __Diagram.W x_2),
  ∃ (li : x ⟶ j) (lj : x_1 ⟶ j), __Diagram.W li ∧ __Diagram.W lj ∧ x_2 ≫ lj = li
Tactic: refine .ofExistsUnique ⟨⟨⟩⟩ (fun _ h ↦ ?_) (fun _ h₁ _ _ h₂ h₃ ↦ ?_) (fun _ _ _ h ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j x : J
h : __Diagram.P x
⊢ ∃ (lift : x ⟶ j), __Diagram.W lift
have h₁ : j = x
Tactic: simp only [Diagram.single_P, ObjectProperty.singleton_iff] 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
j x : J
h : j = x
⊢ ∃ (lift : x ⟶ j), __Diagram.W lift
have refine_1 : ∃ (lift : j ⟶ j), __Diagram.W lift
Tactic: subst h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j x : J
h₁ : __Diagram.P x
x_1 x_2 : x ⟶ j
h₂ : __Diagram.W x_1
h₃ : __Diagram.W x_2
⊢ x_1 = x_2
have h₄ : j = x
Tactic: simp only [Diagram.single_P, ObjectProperty.singleton_iff] 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
j x : J
x_1 x_2 : x ⟶ j
h₂ : __Diagram.W x_1
h₃ : __Diagram.W x_2
h₁ : j = x
⊢ x_1 = x_2
have refine_2 : ∀ (x x_3 : j ⟶ j) (h₂ : __Diagram.W x) (h₃ : __Diagram.W x_3), x = x_3
Tactic: subst h₁
Cleared hypotheses: x, x_1, x_2, h₂, h₃, h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
x x_1 : j ⟶ j
h₂ : __Diagram.W x
h₃ : __Diagram.W x_1
⊢ x = x_1
have refine_2 : ∀ ⦃X Y : J⦄, 𝟙 j = x_1
Tactic: obtain ⟨⟨⟩⟩ := h₂
Cleared hypotheses: x, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
x : j ⟶ j
h₃ : __Diagram.W x
X Y : J
⊢ 𝟙 j = x
have refine_2 : ∀ ⦃X Y : J⦄, Eq (α := j ⟶ j) (𝟙 j) (𝟙 j)
Tactic: obtain ⟨⟨⟩⟩ := h₃
Cleared hypotheses: x, h₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j x x_1 : J
x_2 : x ⟶ x_1
h : __Diagram.W x_2
⊢ ∃ (li : x ⟶ j) (lj : x_1 ⟶ j), __Diagram.W li ∧ __Diagram.W lj ∧ x_2 ≫ lj = li
have refine_3 : ∀ ⦃X Y : J⦄, ∃ (li : j ⟶ j) (lj : j ⟶ j), __Diagram.W li ∧ __Diagram.W lj ∧ 𝟙 j ≫ lj = li
Tactic: obtain ⟨⟨⟩⟩ := h
Cleared hypotheses: x, x_1, x_2, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i j : J
f : i ⟶ j
hf : (⨆ (i : ι), (D i).W) f
⊢ (⨆ (i : ι), (D i).P) i
have simp : ∀ (hf : ∃ (i_1 : ι), (D i_1).W f), ∃ (i_1 : ι), (D i_1).P i
Tactic: simp only [MorphismProperty.iSup_iff, iSup_apply, iSup_Prop_eq] 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 u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i j : J
f : i ⟶ j
hf : ∃ (i_1 : ι), (D i_1).W f
⊢ ∃ (i_1 : ι), (D i_1).P i
have obtain : ∀ (i_1 : ι) (hi : (D i_1).W f), ∃ (i_2 : ι), (D i_2).P i
Tactic: obtain ⟨i, hi⟩ := 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 u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i j : J
f : i ⟶ j
hf : (⨆ (i : ι), (D i).W) f
⊢ (⨆ (i : ι), (D i).P) j
have simp : ∀ (hf : ∃ (i_1 : ι), (D i_1).W f), ∃ (i : ι), (D i).P j
Tactic: simp only [MorphismProperty.iSup_iff, iSup_apply, iSup_Prop_eq] 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 u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i j : J
f : i ⟶ j
hf : ∃ (i_1 : ι), (D i_1).W f
⊢ ∃ (i : ι), (D i).P j
have obtain : ∀ (i_1 : ι) (hi : (D i_1).W f), ∃ (i : ι), (D i).P j
Tactic: obtain ⟨i, hi⟩ := 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),
    (∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)) ∧
      ∀ (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₂
have choose : ∀ (m₀ : (i : ι) → J) (t₀ : (i : ι) → (D i).top ⟶ m₀ i) (hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m₀ i ⟶ (D i).top)),
  ∃ (m : J) (u : (i : ι) → (D i).top ⟶ m),
    (∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)) ∧
      ∀ (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₂
Tactic: choose m₀ t₀ hm₀ using fun i ↦ hJ (D i).top
-- 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₀ : (i : ι) → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun (i : ι) ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun (i : ι) ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1},
    fst := fun (x : { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }) ↦ PUnit.unit,
    snd := fun (x : { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }) ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun (x : shape.L) ↦ (↑x : ι × ι × J).2.2, right := fun (x : shape.R) ↦ m₁,
    fst := fun (x : shape.L) ↦ (D (↑x : ι × ι × J).1).isTerminal.lift ⋯ ≫ u (↑x : ι × ι × J).1,
    snd := fun (x : shape.L) ↦ (D (↑x : ι × ι × J).2.1).isTerminal.lift ⋯ ≫ u (↑x : ι × ι × J).2.1 }
⊢ ∃ (m : J) (u : (i : ι) → (D i).top ⟶ m),
    (∀ (i : ι), IsEmpty.{w + 1} (m ⟶ (D i).top)) ∧
      ∀ (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₂
have hκ : Cardinal.aleph0 ≤ κ
Tactic: have hκ : Cardinal.aleph0 ≤ κ := Cardinal.IsRegular.aleph0_le Fact.out
-- 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₀ : (i : ι) → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun (i : ι) ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun (i : ι) ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1},
    fst := fun (x : { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }) ↦ PUnit.unit,
    snd := fun (x : { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }) ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun (x : shape.L) ↦ (↑x : ι × ι × J).2.2, right := fun (x : shape.R) ↦ m₁,
    fst := fun (x : shape.L) ↦ (D (↑x : ι × ι × J).1).isTerminal.lift ⋯ ≫ u (↑x : ι × ι × J).1,
    snd := fun (x : shape.L) ↦ (D (↑x : ι × ι × J).2.1).isTerminal.lift ⋯ ≫ u (↑x : ι × ι × J).2.1 }
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT shape.L κ
have this : HasCardinalLT (ι × (i : ι) × Subtype (D i).P) κ
Tactic: have : HasCardinalLT (ι × (Σ (i : ι), Subtype (D i).P)) κ :=
      hasCardinalLT_prod hκ hι (hasCardinalLT_sigma _ _ hι (fun i ↦ (D i).hP))
-- 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₀ : (i : ι) → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty.{w + 1} (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun (i : ι) ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun (i : ι) ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1},
    fst := fun (x : { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }) ↦ PUnit.unit,
    snd := fun (x : { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }) ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun (x : shape.L) ↦ (↑x : ι × ι × J).2.2, right := fun (x : shape.R) ↦ m₁,
    fst := fun (x : shape.L) ↦ (D (↑x : ι × ι × J).1).isTerminal.lift ⋯ ≫ u (↑x : ι × ι × J).1,
    snd := fun (x : shape.L) ↦ (D (↑x : ι × ι × J).2.1).isTerminal.lift ⋯ ≫ u (↑x : ι × ι × J).2.1 }
hκ : Cardinal.aleph0 ≤ κ
this : HasCardinalLT (ι × (i : ι) × Subtype (D i).P) κ
⊢ HasCardinalLT shape.L κ
have refine : Function.Injective (β := ι × (i : ι) × Subtype (D i).P) fun (x : shape.L) ↦
  match (motive := shape.L → ι × (i : ι) × Subtype (D i).P) x with
  | ⟨(i₁, i₂, j), sorry⟩ => (i₁, Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i₂ (Subtype.mk (p := (D i₂).P) j h₂))
Tactic: refine this.of_injective (fun ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩ ↦ ⟨i₁, i₂, ⟨j, h₂⟩⟩) ?_