-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  {h : {n : ℕ} → Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Y.obj (Opposite.op { len := n + 1 }))}
  {h_zero_comp_δ_zero : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (h 0) (Y.δ 0) = g.app (Opposite.op { len := n })}
  {h_last_comp_δ_last :
    ∀ (n : ℕ),
      CategoryTheory.CategoryStruct.comp (h (Fin.last n)) (Y.δ (Fin.last (n + 1))) = f.app (Opposite.op { len := n })}
  {h_succ_comp_δ_castSucc_of_lt :
    ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
      i ≤ j.castSucc →
        CategoryTheory.CategoryStruct.comp (h j.succ) (Y.δ i.castSucc) =
          CategoryTheory.CategoryStruct.comp (X.δ i) (h j)}
  {h_succ_comp_δ_castSucc_succ :
    ∀ {n : ℕ} (j : Fin (n + 1)),
      CategoryTheory.CategoryStruct.comp (h j.succ) (Y.δ j.castSucc.succ) =
        CategoryTheory.CategoryStruct.comp (h j.castSucc) (Y.δ j.castSucc.succ)}
  {h_castSucc_comp_δ_succ_of_lt :
    ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
      j.castSucc < i →
        CategoryTheory.CategoryStruct.comp (h j.castSucc) (Y.δ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.δ i) (h j)}
  {h_comp_σ_castSucc_of_le :
    ∀ {n : ℕ} (i j : Fin (n + 1)),
      i ≤ j →
        CategoryTheory.CategoryStruct.comp (h j) (Y.σ i.castSucc) =
          CategoryTheory.CategoryStruct.comp (X.σ i) (h j.succ)}
  {h_comp_σ_succ_of_lt :
    ∀ {n : ℕ} (i j : Fin (n + 1)),
      j ≤ i →
        CategoryTheory.CategoryStruct.comp (h j) (Y.σ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.σ i) (h j.castSucc)}
  {h_1 : {n : ℕ} → Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Y.obj (Opposite.op { len := n + 1 }))}
  {h_zero_comp_δ_zero_1 :
    ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (h_1 0) (Y.δ 0) = g.app (Opposite.op { len := n })}
  {h_last_comp_δ_last_1 :
    ∀ (n : ℕ),
      CategoryTheory.CategoryStruct.comp (h_1 (Fin.last n)) (Y.δ (Fin.last (n + 1))) = f.app (Opposite.op { len := n })}
  {h_succ_comp_δ_castSucc_of_lt_1 :
    ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
      i ≤ j.castSucc →
        CategoryTheory.CategoryStruct.comp (h_1 j.succ) (Y.δ i.castSucc) =
          CategoryTheory.CategoryStruct.comp (X.δ i) (h_1 j)}
  {h_succ_comp_δ_castSucc_succ_1 :
    ∀ {n : ℕ} (j : Fin (n + 1)),
      CategoryTheory.CategoryStruct.comp (h_1 j.succ) (Y.δ j.castSucc.succ) =
        CategoryTheory.CategoryStruct.comp (h_1 j.castSucc) (Y.δ j.castSucc.succ)}
  {h_castSucc_comp_δ_succ_of_lt_1 :
    ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
      j.castSucc < i →
        CategoryTheory.CategoryStruct.comp (h_1 j.castSucc) (Y.δ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.δ i) (h_1 j)}
  {h_comp_σ_castSucc_of_le_1 :
    ∀ {n : ℕ} (i j : Fin (n + 1)),
      i ≤ j →
        CategoryTheory.CategoryStruct.comp (h_1 j) (Y.σ i.castSucc) =
          CategoryTheory.CategoryStruct.comp (X.σ i) (h_1 j.succ)}
  {h_comp_σ_succ_of_lt_1 :
    ∀ {n : ℕ} (i j : Fin (n + 1)),
      j ≤ i →
        CategoryTheory.CategoryStruct.comp (h_1 j) (Y.σ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.σ i) (h_1 j.castSucc)},
  { h := h, h_zero_comp_δ_zero := h_zero_comp_δ_zero, h_last_comp_δ_last := h_last_comp_δ_last,
        h_succ_comp_δ_castSucc_of_lt := h_succ_comp_δ_castSucc_of_lt,
        h_succ_comp_δ_castSucc_succ := h_succ_comp_δ_castSucc_succ,
        h_castSucc_comp_δ_succ_of_lt := h_castSucc_comp_δ_succ_of_lt,
        h_comp_σ_castSucc_of_le := h_comp_σ_castSucc_of_le, h_comp_σ_succ_of_lt := h_comp_σ_succ_of_lt } =
      { h := h_1, h_zero_comp_δ_zero := h_zero_comp_δ_zero_1, h_last_comp_δ_last := h_last_comp_δ_last_1,
        h_succ_comp_δ_castSucc_of_lt := h_succ_comp_δ_castSucc_of_lt_1,
        h_succ_comp_δ_castSucc_succ := h_succ_comp_δ_castSucc_succ_1,
        h_castSucc_comp_δ_succ_of_lt := h_castSucc_comp_δ_succ_of_lt_1,
        h_comp_σ_castSucc_of_le := h_comp_σ_castSucc_of_le_1, h_comp_σ_succ_of_lt := h_comp_σ_succ_of_lt_1 } →
    h = h_1