-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Splitting
Goal:
X : SSet
x_1 : SimplexCategoryᵒᵖ
n : ℕ
x_2 x_3 : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property : Epi f
x :
  SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α })
      (Opposite.op ⦋m⦌)
      (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) f
        property))
p : ℕ
g : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋p⦌)
property_1 : Epi g
y :
  SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α })
      (Opposite.op ⦋p⦌)
      (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋p⦌)) ↦ Epi α) g
        property_1))
h :
  Eq (α :=
    Functor.CoconeTypes.pt (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
      Discrete.functor
        (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌))))
    (CofanTypes.inj (F :=
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
        { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α }) (Opposite.op ⦋m⦌)
        (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) f
          property))
      x)
    (CofanTypes.inj (F :=
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
        { α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop Δ' // Epi α }) (Opposite.op ⦋p⦌)
        (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋p⦌)) ↦ Epi α) g
          property_1))
      y)
⊢ m = p

Tactic:
unique_nonDegenerate_dim _ _ _ _ rfl _ _ h

Premises used: SSet.unique_nonDegenerate_dim, rfl