-- Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean
lemma fac_aux₂ {n : ℕ}
    (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
    (x : s.pt) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n) :
    X.map (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij).op (lift s x) =
      s.π.app (strArrowMk₂ (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij)) x

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₁ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₂ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) ⋯
β₀ : α ⟶ α₀ := homMk (mkOfSucc 1).op ⋯
β₁ : α ⟶ α₁ := homMk (δ 1).op ⋯
β₂ : α ⟶ α₂ := homMk (mkOfSucc 0).op ⋯
h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x
h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x
t : Fin (1 + 1)
this : α.hom ≫ (mkOfSucc 1).op = α₀.hom
⊢ X.map (α.hom ≫ (mkOfSucc 1).op) (lift s x) = X.map (mkOfSucc 1).op (s.π.app α x)

Tactic:
rw [this, h₀, ← congr_fun (s.w β₀) x]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₁ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
α₂ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) ⋯
β₀ : α ⟶ α₀ := homMk (mkOfSucc 1).op ⋯
β₁ : α ⟶ α₁ := homMk (δ 1).op ⋯
β₂ : α ⟶ α₂ := homMk (mkOfSucc 0).op ⋯
h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x
h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x
t : Fin (1 + 1)
this : α.hom ≫ (mkOfSucc 1).op = α₀.hom
⊢ (s.π.app α ≫ (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X).map β₀) x =
    X.map (mkOfSucc 1).op (s.π.app α x)

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
⊢ i + k ≤ j

Tactic:
omega

Result:
no goals

Proof state:
case intro
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
⊢ ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x

Tactic:
induction k with
| zero =>
    rintro i j hij hj hik
    obtain rfl : i = j := hik
    have : mkOfLe ⟨i, Nat.lt_add_one_of_le hj⟩ ⟨i, Nat.lt_add_one_of_le hj⟩ (by rfl) =
      ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩ := Hom.ext_one_left _ _
    rw [this]
    let α : (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩)) ⟶
      (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩)) :=
          StructuredArrow.homMk ((⦋1⦌.const ⦋0⦌ 0).op) (by simp; rfl)
    have nat := congr_fun (s.π.naturality α) x
    dsimp only [Fin.val_zero, Nat.add_zero, id_eq, Int.reduceNeg, Int.Nat.cast_ofNat_Int,
      Int.reduceAdd, Fin.eta, comp_obj, StructuredArrow.proj_obj, op_obj, const_obj_obj,
      const_obj_map, types_comp_apply, types_id_apply, Functor.comp_map, StructuredArrow.proj_map,
      op_map] at nat
    rw [nat, op_comp, Functor.map_comp]
    simp only [types_comp_apply]
    refine congrArg (X.map (⦋1⦌.const ⦋0⦌ 0).op) ?_
    unfold strArrowMk₂
    rw [lift, StrictSegal.spineToSimplex_vertex]
    congr
| succ k hk =>
    intro i j hij hj hik
    let α := strArrowMk₂ (mkOfLeComp (n := n) ⟨i, by omega⟩ ⟨i + k, by omega⟩
        ⟨j, by omega⟩ (by simp) (by simp only [Fin.mk_le_mk]; omega))
    let α₀ := strArrowMk₂ (mkOfLe (n := n) ⟨i + k, by omega⟩ ⟨j, by omega⟩
      (by simp only [Fin.mk_le_mk]; omega))
    let α₁ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨j, by omega⟩
      (by simp only [Fin.mk_le_mk]; omega))
    let α₂ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨i + k, by omega⟩ (by simp))
    let β₀ : α ⟶ α₀ := StructuredArrow.homMk ((mkOfSucc 1).op) (Quiver.Hom.unop_inj
      (by ext x; fin_cases x <;> rfl))
    let β₁ : α ⟶ α₁ := StructuredArrow.homMk ((δ 1).op) (Quiver.Hom.unop_inj
      (by ext x; fin_cases x <;> rfl))
    let β₂ : α ⟶ α₂ := StructuredArrow.homMk ((mkOfSucc 0).op) (Quiver.Hom.unop_inj
      (by ext x; fin_cases x <;> rfl))
    have h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x := by
      subst hik
      exact fac_aux₁ _ _ _ _ hj
    have h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x :=
      hk i (i + k) (by simp) (by omega) rfl
    change X.map α₁.hom (lift s x) = s.π.app α₁ x
    have : X.map α.hom (lift s x) = s.π.app α x := by
      apply StrictSegal.spineInjective
      apply Path.ext'
      intro t
      dsimp only [spineEquiv]
      rw [Equiv.coe_fn_mk, spine_arrow, spine_arrow,
          ← FunctorToTypes.map_comp_apply]
      match t with
      | 0 =>
          have : α.hom ≫ (mkOfSucc 0).op = α₂.hom :=
            Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl)
          rw [this, h₂, ← congr_fun (s.w β₂) x]
          rfl
      | 1 =>
          have : α.hom ≫ (mkOfSucc 1).op = α₀.hom :=
            Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl)
          rw [this, h₀, ← congr_fun (s.w β₀) x]
          rfl
    rw [← StructuredArrow.w β₁, FunctorToTypes.map_comp_apply, this, ← s.w β₁]
    dsimp

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
⊢ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op ≫ ((Truncated.inclusion 2).map (⦋1⦌.const ⦋0⦌ 0).op.unop).op =
    (⦋1⦌.const ⦋n⦌ ((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩)) 0)).op

Tactic:
rfl

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) ⋯
α₀ : StructuredArrow (op ⦋n⦌) (Truncated.inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) ⋯
⊢ j < n + 1

Tactic:
omega

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j → X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
⊢ i < n + 1

Tactic:
omega

Result:
no goals