Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (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 // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).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✝ : (D (i₁', i₂', j').1).P (i₁', i₂', j').2.2
right✝ : (D (i₁', i₂', j').2.1).P (i₁', i₂', j').2.2
h :
  ((fun x ↦
            match x with
            | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
          ⟨(i₁, i₂, j), ⋯⟩).1 =
      ((fun x ↦
            match x with
            | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
          ⟨(i₁', i₂', j'), ⋯⟩).1 ∧
    ((fun x ↦
            match x with
            | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
          ⟨(i₁, i₂, j), ⋯⟩).2 =
      ((fun x ↦
            match x with
            | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
          ⟨(i₁', i₂', j'), ⋯⟩).2
⊢ ⟨(i₁, i₂, j), ⋯⟩ = ⟨(i₁', i₂', j'), ⋯⟩

Tactic:
Sigma.ext_iff

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (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 // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).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✝ : (D (i₁', i₂', j').1).P (i₁', i₂', j').2.2
right✝ : (D (i₁', i₂', j').2.1).P (i₁', i₂', j').2.2
h :
  ((fun x ↦
            match x with
            | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
          ⟨(i₁, i₂, j), ⋯⟩).1 =
      ((fun x ↦
            match x with
            | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
          ⟨(i₁', i₂', j'), ⋯⟩).1 ∧
    ((fun x ↦
                match x with
                | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
              ⟨(i₁, i₂, j), ⋯⟩).2.fst =
        ((fun x ↦
                match x with
                | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
              ⟨(i₁', i₂', j'), ⋯⟩).2.fst ∧
      ((fun x ↦
                match x with
                | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
              ⟨(i₁, i₂, j), ⋯⟩).2.snd ≍
        ((fun x ↦
                match x with
                | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
              ⟨(i₁', i₂', j'), ⋯⟩).2.snd
⊢ ⟨(i₁, i₂, j), ⋯⟩ = ⟨(i₁', i₂', j'), ⋯⟩