English
For i : Fin(n+2) and x : Fin(n+3), the map' applied to the succAbove order-embedding yields the predAbove action: map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x.
Русский
Для i ∈ Fin(n+2) и x ∈ Fin(n+3) отображение map' от отображения i.succAboveOrderEmb.toOrderHom отправляет действие predAbove: map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x.
LaTeX
$$$map'\\,i\\!\\.succAboveOrderEmb.toOrderHom\\,x = i.predAbove\\,x$$$
Lean4
@[simp]
theorem map'_succAboveOrderEmb {n : ℕ} (i : Fin (n + 2)) (x : Fin (n + 3)) :
map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x :=
by
obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
· by_cases hx : x ≤ i
· rw [Fin.predAbove_of_le_castSucc _ _ (by simpa), Fin.castPred_castSucc]
obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
· simp only [map'_eq_castSucc_iff, OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
constructor
· obtain hx | rfl := hx.lt_or_eq
· rwa [Fin.succAbove_of_castSucc_lt]
· simpa only [Fin.succAbove_castSucc_self] using Fin.castSucc_le_succ x
· intro j hj
rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx), Fin.castSucc_lt_castSucc_iff]
· obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx
simp [map'_eq_last_iff]
· simp only [not_le] at hx
obtain ⟨x, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hx)
rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.le_castSucc_iff]), Fin.pred_castSucc_succ,
map'_eq_castSucc_iff]
simp only [Fin.succAbove_of_lt_succ _ _ hx, OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply, le_refl,
Fin.castSucc_lt_castSucc_iff, true_and]
intro j hj
by_cases h : j.castSucc < i
· simpa [Fin.succAbove_of_castSucc_lt _ _ h] using hj.le
· simp only [not_lt] at h
rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]
· simp
