-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
refine_1 :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op ≫ X.map f.op) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₁ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((section_ f).op ≫ f.op)) : (a : X _⦋n⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₂ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op ≫ X.map ((section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₃ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f.op ≫ (section_ f).op ≫ f.op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₄ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f.op ≫ (f ≫ section_ f).op)) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₅ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map ((f ≫ section_ f) ≫ f).op) : (a : X _⦋m⦌) → X _⦋n⦌)
        (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
refine_1₆ :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f ≫ section_ f ≫ f).op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
⊢ Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
          X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
have refine_1₇ : Eq (α := X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f ≫ 𝟙 ⦋m⦌).op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]