chore(AlgebraicTopology): autoParam for strArrowMk₂ (#21562)

We make the proof in `SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂` an autoParam and remove the explicit proof term from most uses of `strArrowMk₂`. Additionally, we replace one instance of `erw` in the same file (`Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean`).

Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

@@ -56,9 +56,9 @@ namespace isPointwiseRightKanExtensionAt
 
 /-- A morphism in `SimplexCategory` with domain `[0]`, `[1]`, or `[2]` defines an object in the
 comma category `StructuredArrow (op [n]) (Truncated.inclusion (n := 2)).op`.-/
-abbrev strArrowMk₂ {i : ℕ} {n : ℕ} (φ : [i] ⟶ [n]) (hi : i ≤ 2) :
-    StructuredArrow (op [n]) (Truncated.inclusion (n := 2)).op :=
-  StructuredArrow.mk (Y := op ⟨[i], hi⟩) (by exact φ.op)
+abbrev strArrowMk₂ {i : ℕ} {n : ℕ} (φ : [i] ⟶ [n]) (hi : i ≤ 2 := by omega) :
+    StructuredArrow (op [n]) (Truncated.inclusion 2).op :=
+  StructuredArrow.mk (Y := op [i]₂) φ.op
 
 /-- Given a term in the cone over the diagram
 `(proj (op [n]) ((Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)` where `X` is
@@ -71,15 +71,15 @@ noncomputable def lift {X : SSet.{u}} [StrictSegal X] {n}
     vertex := fun i ↦ s.π.app (.mk (Y := op [0]₂) (.op (SimplexCategory.const _ _ i))) x
     arrow := fun i ↦ s.π.app (.mk (Y := op [1]₂) (.op (mkOfLe _ _ (Fin.castSucc_le_succ i)))) x
     arrow_src := fun i ↦ by
-      let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) (by simp) ⟶
-        strArrowMk₂ ([0].const _ i.castSucc) (by simp) :=
+      let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶
+        strArrowMk₂ ([0].const _ i.castSucc) :=
           StructuredArrow.homMk (δ 1).op
           (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))
       exact congr_fun (s.w φ) x
     arrow_tgt := fun i ↦ by
       dsimp
-      let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) (by simp) ⟶
-          strArrowMk₂ ([0].const _ i.succ) (by simp) :=
+      let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶
+          strArrowMk₂ ([0].const _ i.succ) :=
         StructuredArrow.homMk (δ 0).op
           (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))
       exact congr_fun (s.w φ) x }
@@ -88,7 +88,7 @@ lemma fac_aux₁ {n : ℕ}
     (s : Cone (proj (op [n]) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
     (x : s.pt) (i : ℕ) (hi : i < n) :
     X.map (mkOfSucc ⟨i, hi⟩).op (lift s x) =
-      s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) (by omega)) x := by
+      s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩)) x := by
   dsimp [lift]
   rw [spineToSimplex_arrow]
   rfl
@@ -97,18 +97,18 @@ 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) (by omega)) x := by
+      s.π.app (strArrowMk₂ (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij)) x := by
   obtain ⟨k, hk⟩ := Nat.le.dest hij
   revert i j
   induction k with
   | zero =>
       rintro i j hij hj hik
-      obtain rfl : i = j := by omega
-      have : mkOfLe ⟨i, Nat.lt_add_one_of_le hj⟩ ⟨i, Nat.lt_add_one_of_le hj⟩ (by omega) =
+      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⟩) (by omega)) ⟶
-        (strArrowMk₂ ([1].const [0] 0 ≫ [0].const [n] ⟨i, Nat.lt_add_one_of_le hj⟩) (by omega)) :=
+      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,
@@ -124,22 +124,21 @@ lemma fac_aux₂ {n : ℕ}
   | 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)) (by rfl)
+          ⟨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)) (by simp)
+        (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)) (by simp)
-      let α₂ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨i + k, by omega⟩ (by simp)) (by simp)
+        (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
-        obtain rfl : j = (i + k) + 1 := by omega
-        exact fac_aux₁ _ _ _ _ (by omega)
+        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
@@ -167,9 +166,9 @@ lemma fac_aux₂ {n : ℕ}
 lemma fac_aux₃ {n : ℕ}
     (s : Cone (proj (op [n]) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
     (x : s.pt) (φ : [1] ⟶ [n]) :
-    X.map φ.op (lift s x) = s.π.app (strArrowMk₂ φ (by omega)) x := by
+    X.map φ.op (lift s x) = s.π.app (strArrowMk₂ φ) x := by
   obtain ⟨i, j, hij, rfl⟩ : ∃ i j hij, φ = mkOfLe i j hij :=
-    ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by simp),
+    ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by decide),
       Hom.ext_one_left _ _ rfl rfl⟩
   exact fac_aux₂ _ _ _ _ _ _ (by omega)
 
@@ -191,14 +190,14 @@ noncomputable def isPointwiseRightKanExtensionAt (n : ℕ) :
     dsimp
     ext k
     · dsimp only [spineEquiv, Equiv.coe_fn_mk]
-      erw [spine_map_vertex]
-      rw [spine_spineToSimplex, spine_vertex]
-      let α : strArrowMk₂ f hi ⟶ strArrowMk₂ ([0].const [n] (f.toOrderHom k)) (by omega) :=
+      rw [show op f = f.op from rfl]
+      rw [spine_map_vertex, spine_spineToSimplex, spine_vertex]
+      let α : strArrowMk₂ f hi ⟶ strArrowMk₂ ([0].const [n] (f.toOrderHom k)) :=
         StructuredArrow.homMk (([0].const _ (by exact k)).op) (by simp; rfl)
       exact congr_fun (s.w α).symm x
     · dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
       rw [← FunctorToTypes.map_comp_apply]
-      let α : strArrowMk₂ f hi ⟶ strArrowMk₂ (mkOfSucc k ≫ f) (by omega) :=
+      let α : strArrowMk₂ f ⟶ strArrowMk₂ (mkOfSucc k ≫ f) :=
         StructuredArrow.homMk (mkOfSucc k).op (by simp; rfl)
       exact (isPointwiseRightKanExtensionAt.fac_aux₃ _ _ _ _).trans (congr_fun (s.w α).symm x)
   uniq s m hm := by