Delete now upstreamed lemmas

Author: YaelDillies

LeanCamCombi.lean

@@ -16,7 +16,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYM
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 import LeanCamCombi.Mathlib.Data.Fintype.Card
-import LeanCamCombi.Mathlib.Data.Nat.Choose.Cast
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.PlainCombi.KatonaCircle
 import LeanCamCombi.PlainCombi.LittlewoodOfford

LeanCamCombi/Mathlib/Data/Nat/Choose/Cast.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou, Chris Wong
 -/
 import LeanCamCombi.Mathlib.Data.Fintype.Card
-import LeanCamCombi.Mathlib.Data.Nat.Choose.Cast
 import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Perm
+import Mathlib.Data.Nat.Choose.Cast
 
 /-!
 # The Katona circle method
@@ -107,7 +107,7 @@ lemma card_prefixed (s : Finset α) : #(prefixed s) = (#s)! * (card α - #s)! :=
 
 @[simp]
 lemma dens_prefixed (s : Finset α) : (prefixed s).dens = ((card α).choose #s : ℚ≥0)⁻¹ := by
-  simp [dens, card_prefixed, Nat.cast_choose' _ s.card_le_univ]
+  simp [dens, card_prefixed, Nat.cast_choose _ s.card_le_univ]
 
 -- TODO: This can be strengthened to an iff
 lemma disjoint_prefixed_prefixed (hst : ¬ s ⊆ t) (hts : ¬ t ⊆ s) :