awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ (m : J) (x : e ⟶ m), IsEmpty.{w + 1} (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : (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
⊢ 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') ⋯)
have 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) sorry)
    (Subtype.mk (p := fun (x : ι × ι × J) ↦ (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2) (i₁, i₂', j') sorry)
Tactic: obtain rfl : i₁ = i₁' := h.1
Cleared hypotheses: i₁', left_1, right_1, 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 ι κ
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
⊢ 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') ⋯)
have 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) sorry)
    (Subtype.mk (p := fun (x : ι × ι × J) ↦ (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2) (i₁, i₂, j') sorry)
Tactic: obtain rfl : i₂ = i₂' := h.2.1
Cleared hypotheses: i₂', left_1, right_1, 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 ι κ
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
⊢ 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') ⋯)
have 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) sorry)
    (Subtype.mk (p := fun (x : ι × ι × J) ↦ (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2) (i₁, i₂, j) sorry)
Tactic: obtain rfl : j = j' := by simpa using h
Cleared hypotheses: j', left_1, right_1, 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₀ : (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 ≤ κ
⊢ ∃ (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 hL : 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
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
⊢ ∃ (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 hR : HasCardinalLT shape.R κ
Tactic: have hR : HasCardinalLT shape.R κ := hasCardinalLT_of_finite _ _ 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 ι κ
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)) κ
have rw : (HasCardinalLT shape.L κ ∧ HasCardinalLT shape.R κ) ∧ HasCardinalLT shape.L κ ∧ HasCardinalLT shape.L κ
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κ]
-- 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 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
⊢ ∃ (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 hshape : 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
-- 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 j : J} {f : i ⟶ j},
    ((D₁ D hι m).W ⊔
          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 →
      (D₁ D hι m).P i
have simp : ∀ {i j : J} {f : i ⟶ j},
  (((⨆ (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)))
      f →
    (∃ (a : ι), (D a).P i) ∨ m = i
Tactic: simp only [D₁_W, D₁_P]
-- 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
i j : J
f : i ⟶ j
hf : (⨆ (i : ι), (D i).W) f
⊢ (∃ (a : ι), (D a).P i) ∨ m = i
have hf₁ : ∃ (i_1 : ι), (D i_1).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
i j : J
f : i ⟶ j
hf : ∃ (i_1 : ι), (D i_1).W f
⊢ (∃ (a : ι), (D a).P i) ∨ m = i
have inl : ∀ (i_1 : ι) (hf : (D i_1).W f), (∃ (a : ι), (D a).P i) ∨ m = i
Tactic: obtain ⟨i, hf⟩ := 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 j : J} {f : i ⟶ j},
    ((D₁ D hι m).W ⊔
          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 →
      (D₁ D hι m).P j
have simp : ∀ {i j : J} {f : i ⟶ j},
  (((⨆ (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)))
      f →
    (∃ (a : ι), (D a).P j) ∨ m = j
Tactic: simp only [D₁_W, D₁_P]
-- 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
i j : J
f : i ⟶ j
hf : (⨆ (i : ι), (D i).W) f
⊢ (∃ (a : ι), (D a).P j) ∨ m = j
have hf₁ : ∃ (i_1 : ι), (D i_1).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
i j : J
f : i ⟶ j
hf : ∃ (i_1 : ι), (D i_1).W f
⊢ (∃ (a : ι), (D a).P j) ∨ m = j
have inl : ∀ (i_1 : ι) (hf : (D i_1).W f), (∃ (a : ι), (D a).P j) ∨ m = j
Tactic: obtain ⟨i, hf⟩ := 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 : ι), (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 = 𝟙 m
have inl : ∀ (hf : (⨆ (i : ι), (D i).W) f), f = 𝟙 m
Tactic: obtain ((hf | ⟨⟨⟩⟩) | hf) := 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 : ι), (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 = 𝟙 m
⊢ f = 𝟙 m
have inl₁ : ∀ ⦃X Y : J⦄ (i : Unit), Eq (α := m ⟶ m) (𝟙 m) (𝟙 m)
Tactic: obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
Cleared hypotheses: 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
ι : 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 : ι), (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 = 𝟙 m
inl₁ : ∀ ⦃X Y : J⦄ (i : Unit), Eq (α := m ⟶ m) (𝟙 m) (𝟙 m)
⊢ f = 𝟙 m
have inr : ∀
  (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 sorry ≫
          u (x.fst (β := fun (i : ι) ↦ Subtype (D i).P)))
      f),
  f = 𝟙 m
Tactic: obtain ((hf | ⟨⟨⟩⟩) | 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
ι : 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 : ι), (D i).W) f
⊢ f = 𝟙 m
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
ι : 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 : ι), (D i).W f
⊢ f = 𝟙 m
have inl : ∀ (i : ι) (hi : (D i).W f), f = 𝟙 m
Tactic: obtain ⟨i, hi⟩ := hf
Cleared hypotheses: hf