fix(ErdosProblems): 274 (#2390)

Use existential quantifier instead of universal. This is false if `G`
has prime order, since the only exact coverings of size `> 1` are
`p`-copies of `{1}`, which all have the same size.

---------

Co-authored-by: Paul Lezeau <lezeau@google.com>

Author: smmercuri

FormalConjectures/ErdosProblems/274.lean

@@ -47,12 +47,13 @@ structure Group.ExactCovering (G : Type*) [Group G] (ι : Type*) [Fintype ι] wh
 
 /--
 If `G` is a group then can there exist an exact covering of `G` by more than one cosets of
+Does there exist a group `G` with an exact covering by more than one cosets of
 different sizes? (i.e. each element is contained in exactly one of the cosets.)
 -/
 @[category research open, AMS 20]
-theorem erdos_274 : answer(sorry) ↔ ∀ᵉ (G : Type*) (h : Group G) (hG : 1 < ENat.card G),
-    (∃ (ι : Type*) (_ : Fintype ι) (P : Group.ExactCovering G ι),
-      1 < Fintype.card ι ∧ (Set.range P.parts).Pairwise fun A B ↦ #A ≠ #B) := by
+theorem erdos_274 : answer(sorry) ↔ ∃ (G : Type*) (h : Group G) (hG : 1 < ENat.card G)
+    (ι : Type*) (_ : Fintype ι) (P : Group.ExactCovering G ι),
+      1 < Fintype.card ι ∧ (Set.range P.parts).Pairwise fun A B ↦ #A ≠ #B := by
   sorry
 
 /--