-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Splitting (goal)
Goal:
X : SSet
x : SimplexCategoryᵒᵖ
n : ℕ
refine_1 :
  ∀
    (x :
      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⦌)))),
    ∃ (i : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)) (y :
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌) i),
      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⦌)))
          i y =
        x
refine_2 :
  ∀ (x : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)) (m : ℕ)
    (f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)) (property : Epi f)
    (x 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 α) f
            property)))
    (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 α) f
              property))
          y)),
    x = y
⊢ Functor.CoconeTypes.IsColimit (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⦌)))
have refine_3 : ∀ (x x : 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)),
  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: refine CofanTypes.isColimit_mk _ (fun x ↦ ?_) (fun ⟨⟨⟨m⟩⟩, f, _⟩ x y h ↦ ?_)
      (fun ⟨⟨⟨m⟩⟩, f, _⟩ ⟨⟨⟨p⟩⟩, g, _⟩ x y h ↦ ?_)