feat: interaction of Finset.sup and Nat.cast (#19245)

Co-authored-by: Andrew Yang

Author: YaelDillies

Mathlib.lean

@@ -743,6 +743,7 @@ import Mathlib.Algebra.Order.Ring.Canonical
 import Mathlib.Algebra.Order.Ring.Cast
 import Mathlib.Algebra.Order.Ring.Cone
 import Mathlib.Algebra.Order.Ring.Defs
+import Mathlib.Algebra.Order.Ring.Finset
 import Mathlib.Algebra.Order.Ring.InjSurj
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.Algebra.Order.Ring.Nat

Mathlib/Algebra/Order/Ring/Finset.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2022 Eric Wieser, Yaël Dillies, Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser, Yaël Dillies, Andrew Yang
+-/
+import Mathlib.Algebra.Order.Field.Canonical.Defs
+import Mathlib.Data.Finset.Lattice.Fold
+import Mathlib.Data.Nat.Cast.Order.Ring
+
+/-!
+# `Finset.sup` of `Nat.cast`
+-/
+
+open Finset
+
+namespace Nat
+variable {ι R : Type*}
+
+section LinearOrderedSemiring
+variable [LinearOrderedSemiring R] {s : Finset ι}
+
+set_option linter.docPrime false in
+@[simp, norm_cast]
+lemma cast_finsetSup' (f : ι → ℕ) (hs) : ((s.sup' hs f : ℕ) : R) = s.sup' hs fun i ↦ (f i : R) :=
+  comp_sup'_eq_sup'_comp _ _ cast_max
+
+set_option linter.docPrime false in
+@[simp, norm_cast]
+lemma cast_finsetInf' (f : ι → ℕ) (hs) : (↑(s.inf' hs f) : R) = s.inf' hs fun i ↦ (f i : R) :=
+  comp_inf'_eq_inf'_comp _ _ cast_min
+
+end LinearOrderedSemiring
+
+@[simp, norm_cast]
+lemma cast_finsetSup [CanonicallyLinearOrderedSemifield R] (s : Finset ι) (f : ι → ℕ) :
+    (↑(s.sup f) : R) = s.sup fun i ↦ (f i : R) :=
+  comp_sup_eq_sup_comp _ cast_max (by simp)
+
+end Nat

Mathlib/Data/Nat/Cast/Order/Ring.lean

@@ -37,11 +37,11 @@ theorem ofNat_nonneg {α} [OrderedSemiring α] (n : ℕ) [n.AtLeastTwo] :
   ofNat_nonneg' n
 
 @[simp, norm_cast]
-theorem cast_min {α} [LinearOrderedSemiring α] {a b : ℕ} : ((min a b : ℕ) : α) = min (a : α) b :=
+theorem cast_min {α} [LinearOrderedSemiring α] (m n : ℕ) : (↑(min m n : ℕ) : α) = min (m : α) n :=
   (@mono_cast α _).map_min
 
 @[simp, norm_cast]
-theorem cast_max {α} [LinearOrderedSemiring α] {a b : ℕ} : ((max a b : ℕ) : α) = max (a : α) b :=
+theorem cast_max {α} [LinearOrderedSemiring α] (m n : ℕ) : (↑(max m n : ℕ) : α) = max (m : α) n :=
   (@mono_cast α _).map_max
 
 section Nontrivial