English
For i : Fin(n+1) and x : Fin(n+2), the map' built from i.predAbove with the monotone data yields i.succ.castSucc.succAbove x.
Русский
Для i : Fin(n+1) и x : Fin(n+2) отображение map' построено как i.predAbove даёт i.succ.castSucc.succAbove x.
LaTeX
$$$map'\\{ toFun := i.predAbove, monotone' := Fin.predAbove_right_monotone i \\} x = i.succ.castSucc.succAbove x$$$
Lean4
@[simp]
theorem map'_predAbove {n : ℕ} (i : Fin (n + 1)) (x : Fin (n + 2)) :
map' { toFun := i.predAbove, monotone' := Fin.predAbove_right_monotone i } x = i.succ.castSucc.succAbove x :=
by
obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
· by_cases hi : i.succ ≤ x.castSucc
· rw [Fin.succAbove_of_le_castSucc _ _ (by simpa), Fin.succ_castSucc, map'_eq_castSucc_iff]
simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
constructor
· rw [Fin.succ_le_castSucc_iff] at hi
rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa only [Fin.castSucc_lt_succ_iff] using hi.le), Fin.pred_succ]
· intro j hj
by_cases h : i.castSucc < j
· rwa [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
· simp only [not_lt] at h
rw [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff, Fin.castSucc_castPred]
exact lt_of_le_of_lt h hi
· simp only [Fin.succ_le_castSucc_iff, not_lt] at hi
rw [Fin.succAbove_of_castSucc_lt _ _ (by simpa), map'_eq_castSucc_iff]
simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
constructor
· simp only [i.predAbove_of_le_castSucc x.castSucc (by simpa), Fin.castPred_castSucc, le_refl]
· intro j hj
by_cases h : i.castSucc < j
· rw [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
exact hj.trans x.castSucc_lt_succ
· simp only [not_lt] at h
rwa [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff, Fin.castSucc_castPred]
· simp [map'_last]
