Finset sum lt iff sum of coerced

Stream: Is there code for X?

[Malvin Gattinger]

Is there a theorem like this already in mathlib that I did not find? Or other theorems to for Finset.sum and ofNat?

import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.BigOperators.Order

theorem extracted {X Y : Finset α} {f : α → Nat} :
    Finset.sum X f < Finset.sum Y f
  ↔ (Finset.sum X fun x => (↑(f x) : Int)) < Finset.sum Y fun x => ↑(f x) :=
  by
  sorry

[Kevin Buzzard]

import Mathlib.Tactic

variable (α : Type 32)

theorem extracted {X Y : Finset α} {f : α → Nat} :
    Finset.sum X f < Finset.sum Y f
  ↔ (Finset.sum X fun x => (↑(f x) : Int)) < Finset.sum Y fun x => ↑(f x) :=
  by zify

[Malvin Gattinger]

Thank you!