Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «0»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

pp: case «1»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

pp: case «2»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
· dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 2 3 (by simp)).hom,
          ← Category.assoc]
        convert! h₂₃ <;> decide

Goal state after:
case «1»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

case «2»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃