English
If f is monotone, then for each a and each j, j < card { i : f(i) ≤ a } iff f(j) ≤ a.
Русский
Если f монотонна, то для любого a и любого j выполняется: j <card{ i : f(i) ≤ a } эквивалентно f(j) ≤ a.
LaTeX
$$$\\forall m\\, (f : \\mathrm{Fin}\,m \\to \\alpha)\\, (a \\in \\alpha),\\; \\mathrm{Monotone}(f) \\Rightarrow\\; j < \\mathrm{card}\\{ i : f(i) \\le a \\} \\iff f(j) \\le a.$$$
Lean4
/-- If `f₀ ≤ f₁ ≤ f₂ ≤ ⋯` is a sorted `m`-tuple of elements of `α`, then for any `j : Fin m` and
`a : α` we have `j < #{i | fᵢ ≤ a}` iff `fⱼ ≤ a`. -/
theorem lt_card_le_iff_apply_le_of_monotone [Preorder α] [DecidableLE α] {m : ℕ} (f : Fin m → α) (a : α)
(h_sorted : Monotone f) (j : Fin m) : j < Fintype.card { i // f i ≤ a } ↔ f j ≤ a :=
by
suffices h1 : ∀ k : Fin m, (k < Fintype.card { i // f i ≤ a }) → f k ≤ a
by
refine ⟨h1 j, fun h ↦ ?_⟩
by_contra! hc
let p : Fin m → Prop := fun x ↦ f x ≤ a
let q : Fin m → Prop := fun x ↦ x < Fintype.card { i // f i ≤ a }
let q' : { i // f i ≤ a } → Prop := fun x ↦ q x
have hw : 0 < Fintype.card { j : { x : Fin m // f x ≤ a } // ¬q' j } :=
Fintype.card_pos_iff.2 ⟨⟨⟨j, h⟩, not_lt.2 hc⟩⟩
apply hw.ne'
have he := Fintype.card_congr <| Equiv.sumCompl <| q'
have h4 := (Fintype.card_congr (@Equiv.subtypeSubtypeEquivSubtype _ p q (h1 _)))
have h_le : Fintype.card { i // f i ≤ a } ≤ m := by omega
rwa [Fintype.card_sum, h4, Fintype.card_fin_lt_of_le h_le, add_eq_left] at he
intro _ h
contrapose! h
rw [← Fin.card_Iio, Fintype.card_subtype]
refine Finset.card_mono (fun i => Function.mtr ?_)
rw [Finset.mem_filter_univ, Finset.mem_Iio]
exact fun hij hia ↦ h ((h_sorted (le_of_not_gt hij)).trans hia)
