chore(algebra/big_operators/part_enat): drop file (#17934)

The only lemma in this file is a version of `nat.cast_sum`. Also fix an instance on `part_enat` so that `nat.cast_sum` works for this type.

archive/imo/imo2019_q4.lean

@@ -5,7 +5,6 @@ Authors: Floris van Doorn
 -/
 import tactic.interval_cases
 import algebra.big_operators.order
-import algebra.big_operators.part_enat
 import data.nat.multiplicity
 
 /-!
@@ -36,7 +35,7 @@ begin
   { suffices : multiplicity 2 (k! : ℤ) = (n * (n - 1) / 2 : ℕ),
     { rw [← part_enat.coe_lt_coe, ← this], change multiplicity ((2 : ℕ) : ℤ) _ < _,
       simp_rw [int.coe_nat_multiplicity, multiplicity_two_factorial_lt hk.lt.ne.symm] },
-    rw [h, multiplicity.finset.prod prime_2, ← sum_range_id, ← sum_nat_coe_enat],
+    rw [h, multiplicity.finset.prod prime_2, ← sum_range_id, nat.cast_sum],
     apply sum_congr rfl, intros i hi,
     rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime prime_2],
     rwa [multiplicity_pow_self_of_prime prime_2, multiplicity_pow_self_of_prime prime_2,

src/algebra/big_operators/default.lean

@@ -6,4 +6,3 @@ import algebra.big_operators.ring
 import algebra.big_operators.pi
 import algebra.big_operators.finsupp
 import algebra.big_operators.nat_antidiagonal
-import algebra.big_operators.part_enat

src/data/nat/part_enat.lean

@@ -78,7 +78,7 @@ instance : add_comm_monoid part_enat :=
   add_zero  := λ x, part.ext' (and_true _) (λ _ _, add_zero _),
   add_assoc := λ x y z, part.ext' and.assoc (λ _ _, add_assoc _ _ _) }
 
-instance : add_monoid_with_one part_enat :=
+instance : add_comm_monoid_with_one part_enat :=
 { one := 1,
   nat_cast := some,
   nat_cast_zero := rfl,