Fin.sum le

Stream: Is there code for X?

[Marcus Rossel]

Is there a simpler way to prove this (or a more general one for types with monotonic addition)?

import Batteries.Data.Fin.Basic

example {n : Nat} (f : Fin n → Nat) (i : Fin n) : f i ≤ Fin.sum f := by
  induction n
  case zero => exact i.elim0
  case succ m ih =>
    rw [Fin.sum, Fin.foldr_succ]
    cases i using Fin.cases
    case zero => simp
    case succ i =>
      specialize ih (f ·.succ) i
      grind [Fin.sum]

[Yaël Dillies]

docs#Finset.single_le_sum

[Etienne Marion]

See also https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/BigOperators/Group/Finset.html#Finset.single_le_sum_of_canonicallyOrdered

[Martin Dvořák]

Yaël Dillies said:

docs#Finset.single_le_sum

Should we provide lemmas for situations where hf is implicit?
By implicit, I mean where the assumption is not needed because nonnegativity comes from the type.

[Yaël Dillies]

That's exactly the lemma Etienne mentioned