awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
i : Unit
⊢ ∃ (a : Unit),
    Eq (α := Subtype (Diagram.P (κ := κ) (Diagram.single j)))
      ((fun (x : Unit) ↦
          (Subtype.mk (p := Diagram.P (κ := κ) (Diagram.single j)) j ⋯ :
            Subtype (Diagram.P (κ := κ) (Diagram.single j))))
        a)
      (Subtype.mk (p := Diagram.P (κ := κ) (Diagram.single j)) j ⋯)

Tactic:
⟨⟨⟩, rfl⟩

Premises used: Exists.intro, PUnit.unit, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
i : Unit
⊢ ∃ (a : Unit),
    Eq (α := Subtype (Diagram.P (κ := κ) (Diagram.single j)))
      ((fun (x : Unit) ↦
          (Subtype.mk (p := Diagram.P (κ := κ) (Diagram.single j)) j ⋯ :
            Subtype (Diagram.P (κ := κ) (Diagram.single j))))
        a)
      (Subtype.mk (p := Diagram.P (κ := κ) (Diagram.single j)) j ⋯)

Tactic:
exact ⟨⟨⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
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
⊢ __Diagram.IsTerminal j

Tactic:
refine .ofExistsUnique ⟨⟨⟩⟩ (fun _ h ↦ ?_) (fun _ h₁ _ _ h₂ h₃ ↦ ?_) (fun _ _ _ h ↦ ?_)
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j x : J
h : __Diagram.P x
⊢ j = x

Tactic:
simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h

Premises used: CategoryTheory.ObjectProperty.singleton_iff, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single_P
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j x : J
h : j = x
refine_1 : ∃ (lift : j ⟶ j), __Diagram.W lift
⊢ ∃ (lift : x ⟶ j), __Diagram.W lift

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
⊢ ∃ (lift : j ⟶ j), __Diagram.W lift

Tactic:
⟨𝟙 _, ⟨⟨⟩⟩⟩

Premises used: CategoryTheory.CategoryStruct.id, Exists.intro, CategoryTheory.MorphismProperty.ofHoms.mk
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j : J
⊢ ∃ (lift : j ⟶ j), __Diagram.W lift

Tactic:
exact ⟨𝟙 _, ⟨⟨⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
⊢ j = x

Tactic:
simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h₁

Premises used: CategoryTheory.ObjectProperty.singleton_iff, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single_P
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
refine_2 : ∀ (x x_3 : j ⟶ j) (h₂ : __Diagram.W x) (h₃ : __Diagram.W x_3), x = x_3
⊢ x_1 = x_2

Tactic:
subst h₁
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
refine_2 : ∀ ⦃X Y : J⦄, 𝟙 j = x_1
⊢ x = x_1

Tactic:
obtain ⟨⟨⟩⟩ := h₂
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
refine_2 : ∀ ⦃X Y : J⦄, Eq (α := j ⟶ j) (𝟙 j) (𝟙 j)
⊢ 𝟙 j = x

Tactic:
obtain ⟨⟨⟩⟩ := h₃
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j X_1 Y_1 X Y : J
⊢ Eq (α := j ⟶ j) (𝟙 j) (𝟙 j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
refine_3 : ∀ ⦃X Y : J⦄, ∃ (li : j ⟶ j) (lj : j ⟶ j), __Diagram.W li ∧ __Diagram.W lj ∧ 𝟙 j ≫ lj = li
⊢ ∃ (li : x ⟶ j) (lj : x_1 ⟶ j), __Diagram.W li ∧ __Diagram.W lj ∧ x_2 ≫ lj = li

Tactic:
obtain ⟨⟨⟩⟩ := h
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j X Y : J
⊢ Eq (α := j ⟶ j) (𝟙 j ≫ 𝟙 j) (𝟙 j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j X Y : J
⊢ ∃ (li : j ⟶ j) (lj : j ⟶ j), __Diagram.W li ∧ __Diagram.W lj ∧ 𝟙 j ≫ lj = li

Tactic:
exact ⟨𝟙 _, 𝟙 _, ⟨⟨⟩⟩, ⟨⟨⟩⟩, by simp⟩
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
j X Y : J
i : Unit
lift : {j_1 : J} → (hj : Diagram.P (κ := κ) (Diagram.single j) j_1) → j_1 ⟶ j
hlift : ∀ {j_1 : J} (hj : Diagram.P (κ := κ) (Diagram.single j) j_1), Diagram.W (κ := κ) (Diagram.single j) (lift hj)
uniq :
  ∀ {j_1 : J} (hj : Diagram.P (κ := κ) (Diagram.single j) j_1) {φ : j_1 ⟶ j}
    (hφ : Diagram.W (κ := κ) (Diagram.single j) φ), lift hj = φ
comm : ∀ {i j_1 : J} (f : i ⟶ j_1) (hf : Diagram.W (κ := κ) (Diagram.single j) f), f ≫ lift ⋯ = lift ⋯
⊢ j = j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
simp : ∀ (hf : ∃ (i_1 : ι), (D i_1).W f), ∃ (i_1 : ι), (D i_1).P i
⊢ (⨆ (i : ι), (D i).P) i

Tactic:
simp only [MorphismProperty.iSup_iff, iSup_apply, iSup_Prop_eq] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.iSup_iff, iSup_Prop_eq, iSup_apply
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
obtain : ∀ (i_1 : ι) (hi : (D i_1).W f), ∃ (i_2 : ι), (D i_2).P i
⊢ ∃ (i_1 : ι), (D i_1).P i

Tactic:
obtain ⟨i, hi⟩ := hf
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i_1 j : J
f : i_1 ⟶ j
i : ι
hi : (D i).W f
⊢ ∃ (i : ι), (D i).P i_1

Tactic:
⟨i, (D i).src hi⟩

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i_1 j : J
f : i_1 ⟶ j
i : ι
hi : (D i).W f
⊢ ∃ (i : ι), (D i).P i_1

Tactic:
exact ⟨i, (D i).src hi⟩
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
simp : ∀ (hf : ∃ (i_1 : ι), (D i_1).W f), ∃ (i : ι), (D i).P j
⊢ (⨆ (i : ι), (D i).P) j

Tactic:
simp only [MorphismProperty.iSup_iff, iSup_apply, iSup_Prop_eq] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.iSup_iff, iSup_Prop_eq, iSup_apply
-- Module: Mathlib.CategoryTheory.Presentable.Directed
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
obtain : ∀ (i_1 : ι) (hi : (D i_1).W f), ∃ (i : ι), (D i).P j
⊢ ∃ (i : ι), (D i).P j

Tactic:
obtain ⟨i, hi⟩ := hf
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i_1 j : J
f : i_1 ⟶ j
i : ι
hi : (D i).W f
⊢ ∃ (i : ι), (D i).P j

Tactic:
⟨i, (D i).tgt hi⟩

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i_1 j : J
f : i_1 ⟶ j
i : ι
hi : (D i).W f
⊢ ∃ (i : ι), (D i).P j

Tactic:
exact ⟨i, (D i).tgt hi⟩
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i j : J
f : i ⟶ j
h : D₁.W f
⊢ (D₁.P ⊔ D₂.P) i

Tactic:
Or.inl (D₁.src h)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, Or.inl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i j : J
f : i ⟶ j
h : D₁.W f
⊢ (D₁.P ⊔ D₂.P) i

Tactic:
exact Or.inl (D₁.src h)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, Or.inl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i j : J
f : i ⟶ j
h : D₂.W f
⊢ (D₁.P ⊔ D₂.P) i

Tactic:
Or.inr (D₂.src h)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, Or.inr
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i j : J
f : i ⟶ j
h : D₂.W f
⊢ (D₁.P ⊔ D₂.P) i

Tactic:
exact Or.inr (D₂.src h)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, Or.inr
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i j : J
f : i ⟶ j
h : D₁.W f
⊢ (D₁.P ⊔ D₂.P) j

Tactic:
Or.inl (D₁.tgt h)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, Or.inl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i j : J
f : i ⟶ j
h : D₁.W f
⊢ (D₁.P ⊔ D₂.P) j

Tactic:
exact Or.inl (D₁.tgt h)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, Or.inl
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i j : J
f : i ⟶ j
h : D₂.W f
⊢ (D₁.P ⊔ D₂.P) j

Tactic:
Or.inr (D₂.tgt h)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, Or.inr
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i j : J
f : i ⟶ j
h : D₂.W f
⊢ (D₁.P ⊔ D₂.P) j

Tactic:
exact Or.inr (D₂.tgt h)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.tgt, Or.inr
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
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₂
⊢ ∃ (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

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.top
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
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 }
⊢ Cardinal.aleph0 ≤ κ

Tactic:
have hκ : Cardinal.aleph0 ≤ κ := Cardinal.IsRegular.aleph0_le Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
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 (ι × (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))
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
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 κ

Tactic:
this.of_injective (fun ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩ ↦ ⟨i₁, i₂, ⟨j, h₂⟩⟩) ?_

Premises used: HasCardinalLT.of_injective, Subtype, Prod.mk, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.P, Subtype.mk, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.toDiagram, Sigma.mk, Prod, Sigma, _private.0.CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered_aux.match_1
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
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) κ
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), ⋯⟩ => (i₁, Sigma.mk (β := fun (i : ι) ↦ Subtype (D i).P) i₂ (Subtype.mk (p := (D i₂).P) j h₂))
⊢ HasCardinalLT shape.L κ

Tactic:
refine this.of_injective (fun ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩ ↦ ⟨i₁, i₂, ⟨j, h₂⟩⟩) ?_

Premises used: HasCardinalLT.of_injective
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
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) κ
i₁ i₂ : ι
j : J
left : (D (i₁, i₂, j).1).P (i₁, i₂, j).2.2
right : (D (i₁, i₂, j).2.1).P (i₁, i₂, j).2.2
i₁' i₂' : ι
j' : J
left_1 : (D (i₁', i₂', j').1).P (i₁', i₂', j').2.2
right_1 : (D (i₁', i₂', j').2.1).P (i₁', i₂', j').2.2
h : i₁ = i₁' ∧ i₂ = i₂' ∧ Subtype.mk (p := (D i₂).P) j right ≍ Subtype.mk (p := (D i₂').P) j' right_1
⊢ i₁ = i₁'

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
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) κ
i₁ i₂ : ι
j : J
left : (D (i₁, i₂, j).1).P (i₁, i₂, j).2.2
right : (D (i₁, i₂, j).2.1).P (i₁, i₂, j).2.2
i₁' i₂' : ι
j' : J
left_1 : (D (i₁', i₂', j').1).P (i₁', i₂', j').2.2
right_1 : (D (i₁', i₂', j').2.1).P (i₁', i₂', j').2.2
h : i₁ = i₁' ∧ i₂ = i₂' ∧ Subtype.mk (p := (D i₂).P) j right ≍ Subtype.mk (p := (D i₂').P) j' right_1
obtain :
  ∀ (left_2 : (D (i₁, i₂', j').1).P (i₁, i₂', j').2.2) (right_2 : (D (i₁, i₂', j').2.1).P (i₁, i₂', j').2.2)
    (h : i₁ = i₁ ∧ i₂ = i₂' ∧ Subtype.mk (p := (D i₂).P) j right ≍ Subtype.mk (p := (D i₂').P) j' right_2),
    Eq (α := shape.L) (Subtype.mk (p := fun (x : ι × ι × J) ↦ (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2) (i₁, i₂, j) ⋯)
      (Subtype.mk (p := fun (x : ι × ι × J) ↦ (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2) (i₁, i₂', j') ⋯)
⊢ Eq (α := shape.L) (Subtype.mk (p := fun (x : ι × ι × J) ↦ (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2) (i₁, i₂, j) ⋯)
    (Subtype.mk (p := fun (x : ι × ι × J) ↦ (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2) (i₁', i₂', j') ⋯)

Tactic:
obtain rfl : i₁ = i₁' := h.1

Premises used: And.left, rfl