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
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₂' : ι
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.2.1

Premises used: And.right, 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₂' : ι
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.2.1

Premises used: And.right, And.left, rfl
-- 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
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
⊢ j = j'

Tactic:
simpa using h
-- 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
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 : j = j' := by simpa using h

Premises used: rfl
-- 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
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
⊢ 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:
rfl
-- 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 shape.L κ

Tactic:
have hL : HasCardinalLT shape.L κ := by
    have : HasCardinalLT (ι × (Σ (i : ι), Subtype (D i).P)) κ :=
      hasCardinalLT_prod hκ hι (hasCardinalLT_sigma _ _ hι (fun i ↦ (D i).hP))
    refine this.of_injective (fun ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩ ↦ ⟨i₁, i₂, ⟨j, h₂⟩⟩) ?_
    rintro ⟨⟨i₁, i₂, j⟩, _, _⟩ ⟨⟨i₁', i₂', j'⟩, _, _⟩ h
    rw [Prod.ext_iff, Sigma.ext_iff] at h
    dsimp at h
    obtain rfl : i₁ = i₁' := h.1
    obtain rfl : i₂ = i₂' := h.2.1
    obtain rfl : j = j' := by simpa using h
    rfl
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
⊢ HasCardinalLT shape.R κ

Tactic:
have hR : HasCardinalLT shape.R κ := hasCardinalLT_of_finite _ _ hκ
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
rw : (HasCardinalLT shape.L κ ∧ HasCardinalLT shape.R κ) ∧ HasCardinalLT shape.L κ ∧ HasCardinalLT shape.L κ
⊢ HasCardinalLT (Arrow (WalkingMultispan shape)) κ

Tactic:
rw [hasCardinalLT_iff_of_equiv (WalkingMultispan.arrowEquiv shape),
      hasCardinalLT_sum_iff _ _ _ hκ, hasCardinalLT_sum_iff _ _ _ hκ,
      hasCardinalLT_iff_of_equiv (WalkingMultispan.equiv shape),
      hasCardinalLT_sum_iff _ _ _ hκ]

Premises used: CategoryTheory.Limits.WalkingMultispan.equiv, hasCardinalLT_iff_of_equiv, hasCardinalLT_sum_iff, CategoryTheory.Limits.WalkingMultispan.arrowEquiv
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
⊢ (HasCardinalLT shape.L κ ∧ HasCardinalLT shape.R κ) ∧ HasCardinalLT shape.L κ ∧ HasCardinalLT shape.L κ

Tactic:
⟨⟨?_, ?_⟩, ?_, ?_⟩

Premises used: And.intro
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
refine_1 : HasCardinalLT shape.L κ
refine_2 : HasCardinalLT shape.R κ
refine_3 refine_4 : HasCardinalLT shape.L κ
⊢ (HasCardinalLT shape.L κ ∧ HasCardinalLT shape.R κ) ∧ HasCardinalLT shape.L κ ∧ HasCardinalLT shape.L κ

Tactic:
refine ⟨⟨?_, ?_⟩, ?_, ?_⟩
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
⊢ HasCardinalLT shape.L κ

Tactic:
assumption
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
⊢ HasCardinalLT shape.R κ

Tactic:
assumption
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
⊢ HasCardinalLT (Arrow (WalkingMultispan shape)) κ

Tactic:
have hshape : HasCardinalLT (Arrow (WalkingMultispan shape)) κ := by
    rw [hasCardinalLT_iff_of_equiv (WalkingMultispan.arrowEquiv shape),
      hasCardinalLT_sum_iff _ _ _ hκ, hasCardinalLT_sum_iff _ _ _ hκ,
      hasCardinalLT_iff_of_equiv (WalkingMultispan.equiv shape),
      hasCardinalLT_sum_iff _ _ _ hκ]
    refine ⟨⟨?_, ?_⟩, ?_, ?_⟩ <;> assumption
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
hshape : HasCardinalLT (Arrow (WalkingMultispan shape)) κ
c : Multicofork index := cocone index.multispan hshape
i₁ i₂ : ι
j : J
h₁ : (D i₁).P j
h₂ : (D i₂).P j
⊢ Eq (α := j ⟶ c.pt) ((D i₁).isTerminal.lift h₁ ≫ (fun (i : ι) ↦ u i ≫ c.π PUnit.unit) i₁)
    ((D i₂).isTerminal.lift h₂ ≫ (fun (i : ι) ↦ u i ≫ c.π PUnit.unit) i₂)

Tactic:
simpa [index, shape] using c.condition ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩

Premises used: Prod.mk, Subtype.mk, And.intro, CategoryTheory.Limits.Multicofork.condition