Module: Mathlib.AlgebraicTopology.SimplicialSet.Splitting

Goal state before:
pp: case refine_1
X : SSet
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
        (Opposite.op ⦋n⦌)).cofanTypes.pt
⊢ ∃ i y,
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
              (Opposite.op ⦋n⦌)).cofanTypes.inj
        i y =
      x

pp: case refine_2
X : SSet
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
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)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩ y
⊢ x = y

pp: case refine_3
X : SSet
x✝² : SimplexCategoryᵒᵖ
n : ℕ
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)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩
p : ℕ
g : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋p⦌)
property✝ : Epi g
y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩ y
⊢ ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ = ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩

Tactic:
· obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x
      exact ⟨.mk f, y, rfl⟩

Goal state after:
case refine_2
X : SSet
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
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)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩ y
⊢ x = y

case refine_3
X : SSet
x✝² : SimplexCategoryᵒᵖ
n : ℕ
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)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩
p : ℕ
g : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋p⦌)
property✝ : Epi g
y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩ y
⊢ ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ = ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩