English
If L is m-admissible, j ∈ L, then j < m + |L| and simplicialEvalσ L j = simplicialEvalσ L (j+1).
Русский
Если L — m-допустимый и j ∈ L, то j < m+|L| и simplicialEvalσ L j = simplicialEvalσ L (j+1).
LaTeX
$$$\\\\text{If } L \\\\text{ is } m\\text{-admissible and } j \\\\in L, \\\\text{ then } j < m + |L| \\\\land \\\\ simplicialEvalσ L j = simplicialEvalσ L (j+1).$$$
Lean4
theorem mem_isAdmissible_of_lt_and_eval_eq_eval_add_one (hL : IsAdmissible m L) (j : ℕ) (hj₁ : j < m + L.length)
(hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)) : j ∈ L := by
induction L generalizing m with
| nil => grind [simplicialEvalσ]
| cons a L h_rec =>
have := h_rec hL.tail (by grind)
suffices ¬j = a → (simplicialEvalσ L j = simplicialEvalσ L (j + 1)) by grind
intro hja
simp only [simplicialEvalσ] at hj₂
have : simplicialEvalσ L j ≤ simplicialEvalσ L (j + 1) := simplicialEvalσ_monotone L (by grind)
suffices
¬a < simplicialEvalσ L j →
a < simplicialEvalσ L (j + 1) →
simplicialEvalσ L j = simplicialEvalσ L (j + 1) - 1 → simplicialEvalσ L j = simplicialEvalσ L (j + 1)
by grind
intro h₁ h₂ hj₂
simp only [IsAdmissible, List.sorted_cons, List.length_cons] at hL
obtain h | rfl | h := Nat.lt_trichotomy j a
· grind [simplicialEvalσ_monotone, Monotone, simplicialEvalσ_of_lt_mem]
· grind
· have := simplicialEvalσ_of_lt_mem L (a + 1) <| fun x h ↦ hL.1.1 x h
grind [simplicialEvalσ_monotone, Monotone]
