add comments and cleanup

TestingLowerBounds/ForMathlib/CountableOrCountablyGenerated.lean

@@ -4,12 +4,12 @@ namespace MeasurableSpace
 
 variable {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
 
-
+-- PRed, see #15418
 lemma countable_left_of_prod_of_nonempty [Nonempty β] (h : Countable (α × β)) : Countable α := by
   contrapose h
   rw [not_countable_iff] at *
   infer_instance
-
+-- PRed, see #15418
 lemma countable_right_of_prod_of_nonempty [Nonempty α] (h : Countable (α × β)) : Countable β := by
   contrapose h
   rw [not_countable_iff] at *
@@ -26,7 +26,7 @@ lemma countableOrCountablyGenerated_left_of_prod_left_of_nonempty [Nonempty β]
   · have := countable_left_of_prod_of_nonempty h
     infer_instance
   · infer_instance
-
+-- PRed, see #15418
 lemma countableOrCountablyGenerated_right_of_prod_left_of_nonempty [Nonempty α]
     [h : CountableOrCountablyGenerated (α × β) γ] :
     CountableOrCountablyGenerated β γ := by
@@ -64,10 +64,9 @@ lemma countableOrCountablyGenerated_left_of_prod_right_of_nonempty [Nonempty γ]
   · infer_instance
   · have := countablyGenerated_left_of_prod_of_nonempty h
     infer_instance
-
-instance [Countable (α × β)] : Countable (β × α) :=
-  Countable.of_equiv _ (Equiv.prodComm α β)
-
+-- PRed, see #15418
+instance [Countable (α × β)] : Countable (β × α) := Countable.of_equiv _ (Equiv.prodComm α β)
+-- PRed, see #15418
 instance [h : CountableOrCountablyGenerated (α × β) γ] :
     CountableOrCountablyGenerated (β × α) γ := by
   rcases h with (h | h)
@@ -78,10 +77,4 @@ instance [h : CountableOrCountablyGenerated (α × β) γ] :
 instance [CountablyGenerated (α × β)] : CountablyGenerated (β × α) := by
   sorry
 
-instance [h : CountableOrCountablyGenerated (α × β) γ] :
-    CountableOrCountablyGenerated (β × α) γ := by
-  rcases h with (h | h)
-  · exact ⟨Or.inl inferInstance⟩
-  · exact ⟨Or.inr h⟩
-
 end MeasurableSpace