Number of pairs on `Fin (n)`

Stream: Is there code for X?

[Shaopeng]

Been trying to prove something where one of the intermediate lemmas is

have h_card : ((Finset.univ.product Finset.univ).filter
        (fun (x, y) => (x : Fin (m + 1)) < y)).card = (m + 1).choose 2 := by
        sorry

Thought this simple fact has been stated and proved somewhere in mathlib4 but my codex failed after half an hour of high thinking. Any advice would be appreciated.

Thanks!

[Ruben Van de Velde]

Please share a #mwe

[Yury G. Kudryashov]

Aristotle solved it in less than 6 minutes (I forgot to time it, so I have only an upper estimate):

import Mathlib

open scoped BigOperators

theorem goal (m : ℕ) : ((Finset.univ.product Finset.univ).filter
    (fun (x, y) => (x : Fin (m + 1)) < y)).card = (m + 1).choose 2 := by
  erw [ Finset.card_filter ];
  erw [ Finset.sum_product ] ; aesop;
  -- The sum of the number of elements greater than $i$ for each $i$ in $Fin (m + 1)$ is equal to the sum of the first $m$ natural numbers.
  have h_sum : ∑ x : Fin (m + 1), (Finset.univ.filter (fun y => x < y)).card = ∑ i ∈ Finset.range (m + 1), (m - i) := by
    simp +decide [ Finset.card_univ, Finset.filter_lt_eq_Ioi ];
    rw [ Finset.sum_range ];
  rw [ h_sum, Nat.choose_two_right ];
  -- The sum of the first $m$ natural numbers is given by the formula $\frac{m(m+1)}{2}$.
  have h_sum_formula : ∑ i ∈ Finset.range (m + 1), (m - i) = ∑ i ∈ Finset.range (m + 1), i := by
    conv_rhs => rw [ ← Finset.sum_flip ] ;
  exact h_sum_formula.trans ( Finset.sum_range_id _ )

I forward-ported the proof to the current version of Lean/Mathlib by replacing the legacy notation ∑ i in Finset.range... with ∑ i ∈ Finset.range... before posting it here.

[Yury G. Kudryashov]

It also proved a more general fact in less than 3 minutes:

theorem goal {α : Type*} [LinearOrder α] [Fintype α] :
    Finset.card {(x, y) : α × α | x < y} = (Fintype.card α).choose 2 := by
  have h_card : Finset.card (Finset.filter (fun (x : α × α) => x.1 < x.2) (Finset.univ : Finset (α × α))) = Finset.card (Finset.powersetCard 2 (Finset.univ : Finset α)) := by
    refine' Finset.card_bij _ _ _ _;
    use fun p hp => { p.1, p.2 };
    · norm_num +zetaDelta at *;
      exact fun a b hab => Finset.card_pair hab.ne;
    · simp +contextual [ Finset.Subset.antisymm_iff, Finset.subset_iff ];
      aesop;
      · exact False.elim <| lt_asymm ha₂ ha₁;
      · exact False.elim <| lt_asymm ha₂ ha₁;
    · -- For any subset $b$ of size 2 in the powerset of the universal set, we can pick the two elements $x$ and $y$ from $b$, order them such that $x < y$, and then the pair $(x, y)$ will be in the set $\{x | x.1 < x.2\}$ and $\{x, y\}$ will equal $b$.
      intro b hb
      obtain ⟨x, y, hx, hy, hxy⟩ : ∃ x y : α, x ∈ b ∧ y ∈ b ∧ x ≠ y ∧ x < y := by
        obtain ⟨ x, y, hx, hy, hxy ⟩ := Finset.card_eq_two.mp ( Finset.mem_powersetCard.mp hb |>.2 ) ; cases lt_trichotomy x y <;> aesop;
      norm_num +zetaDelta at *;
      exact ⟨ x, y, hxy.2, by rw [ Finset.card_eq_two ] at hb; aesop ⟩;
  rw [ h_card, Finset.card_powersetCard, Finset.card_univ ]

[Yury G. Kudryashov]

Clearly, the proofs can be further simplified/golfed etc.

[Shaopeng]

Ruben Van de Velde said:

#mwe

Thank you. Will do for future questions. Thanks!

[Shaopeng]

Yury G. Kudryashov said:

Aristotle solved it in less than 6 minutes (I forgot to time it, so I have only an upper estimate):

import Mathlib

open scoped BigOperators

theorem goal (m : ℕ) : ((Finset.univ.product Finset.univ).filter
    (fun (x, y) => (x : Fin (m + 1)) < y)).card = (m + 1).choose 2 := by
  erw [ Finset.card_filter ];
  erw [ Finset.sum_product ] ; aesop;
  -- The sum of the number of elements greater than $i$ for each $i$ in $Fin (m + 1)$ is equal to the sum of the first $m$ natural numbers.
  have h_sum : ∑ x : Fin (m + 1), (Finset.univ.filter (fun y => x < y)).card = ∑ i ∈ Finset.range (m + 1), (m - i) := by
    simp +decide [ Finset.card_univ, Finset.filter_lt_eq_Ioi ];
    rw [ Finset.sum_range ];
  rw [ h_sum, Nat.choose_two_right ];
  -- The sum of the first $m$ natural numbers is given by the formula $\frac{m(m+1)}{2}$.
  have h_sum_formula : ∑ i ∈ Finset.range (m + 1), (m - i) = ∑ i ∈ Finset.range (m + 1), i := by
    conv_rhs => rw [ ← Finset.sum_flip ] ;
  exact h_sum_formula.trans ( Finset.sum_range_id _ )

I forward-ported the proof to the current version of Lean/Mathlib by replacing the legacy notation ∑ i in Finset.range... with ∑ i ∈ Finset.range... before posting it here.

Thank you so much!

[Shaopeng]

Yury G. Kudryashov said:

Aristotle solved it in less than 6 minutes (I forgot to time it, so I have only an upper estimate):

import Mathlib

open scoped BigOperators

theorem goal (m : ℕ) : ((Finset.univ.product Finset.univ).filter
    (fun (x, y) => (x : Fin (m + 1)) < y)).card = (m + 1).choose 2 := by
  erw [ Finset.card_filter ];
  erw [ Finset.sum_product ] ; aesop;
  -- The sum of the number of elements greater than $i$ for each $i$ in $Fin (m + 1)$ is equal to the sum of the first $m$ natural numbers.
  have h_sum : ∑ x : Fin (m + 1), (Finset.univ.filter (fun y => x < y)).card = ∑ i ∈ Finset.range (m + 1), (m - i) := by
    simp +decide [ Finset.card_univ, Finset.filter_lt_eq_Ioi ];
    rw [ Finset.sum_range ];
  rw [ h_sum, Nat.choose_two_right ];
  -- The sum of the first $m$ natural numbers is given by the formula $\frac{m(m+1)}{2}$.
  have h_sum_formula : ∑ i ∈ Finset.range (m + 1), (m - i) = ∑ i ∈ Finset.range (m + 1), i := by
    conv_rhs => rw [ ← Finset.sum_flip ] ;
  exact h_sum_formula.trans ( Finset.sum_range_id _ )

I forward-ported the proof to the current version of Lean/Mathlib by replacing the legacy notation ∑ i in Finset.range... with ∑ i ∈ Finset.range... before posting it here.

Sorry, do you mind sharing the name of the forward-ported lemma/theorem so I can just apply? I Loogled and couldn't locate it. Thanks!

[Jeremy Tan]

There is no forward-ported lemma, only the notation changed between Aristotle's version and the present version

[Yury G. Kudryashov]

Aristotle uses Mathlib version from May 2025 at the moment. At that time, we used a different notation for sums. I've run a search&replace on Aristotle's output to get a proof that work with today's Mathlib.

[Shaopeng]

Thanks for clarifying!