-- 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)
refine_3 :
  ∀ (g : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) (property_2 : 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 ⦋m⦌)
          (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) g
            property_2)))
    (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 ⦋m⦌)
            (Subtype.mk (p := fun (α : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) ↦ Epi α) g
              property_2))
          y)),
    Eq (α := SimplicialObject.Splitting.IndexSet (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))
      (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 α) g
          property_2))
⊢ Eq (α := SimplicialObject.Splitting.IndexSet (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))
    (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))

Tactic:
obtain rfl : m = p := unique_nonDegenerate_dim _ _ _ _ rfl _ _ h

Premises used: SSet.unique_nonDegenerate_dim, rfl