English
For any i ∈ Fin n, the element i.castSucc in Fin (n+1) is not the last element of Fin (n+1).
Русский
Для любого i ∈ Fin n элемент i.castSucc в Fin(n+1) не является последним элементом Fin(n+1).
LaTeX
$$$\\text{castSucc\\_ne\\_last} : \\forall i \\ (i : Fin n), i.castSucc \\ne \\mathrm{last}\\, n$$$
Lean4
/-- Induct on two ereals by performing case splits on the sign of one whenever the other is
infinite. This version eliminates some cases by assuming that `P` is symmetric and `P x y` implies
`P (-x) y` for all `x`, `y`. -/
@[elab_as_elim]
theorem induction₂_symm_neg {P : EReal → EReal → Prop} (symm : ∀ {x y}, P x y → P y x)
(neg_left : ∀ {x y}, P x y → P (-x) y) (top_top : P ⊤ ⊤) (top_pos : ∀ x : ℝ, 0 < x → P ⊤ x) (top_zero : P ⊤ 0)
(coe_coe : ∀ x y : ℝ, P x y) : ∀ x y, P x y :=
have neg_right : ∀ {x y}, P x y → P x (-y) := fun h => symm <| neg_left <| symm h
have : ∀ x, (∀ y : ℝ, 0 < y → P x y) → ∀ y : ℝ, y < 0 → P x y := fun _ h y hy =>
neg_neg (y : EReal) ▸ neg_right (h _ (neg_pos_of_neg hy))
@induction₂_neg_left P neg_left top_top top_pos top_zero (this _ top_pos) (neg_right top_top) (symm top_zero)
(symm <| neg_left top_zero) (fun x hx => symm <| top_pos x hx) (fun x hx => symm <| neg_left <| top_pos x hx)
coe_coe
