-- 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
⊢ 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_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
Tactic: refine CofanTypes.isColimit_mk _ (fun x ↦ ?_) (fun ⟨⟨⟨m⟩⟩, f, _⟩ x y h ↦ ?_)
      (fun ⟨⟨⟨m⟩⟩, f, _⟩ ⟨⟨⟨p⟩⟩, g, _⟩ x y h ↦ ?_)