chore: Golf BoundedGENhdsClass (α × β) instance (#8085)

and the correspond pi instance.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

@@ -82,14 +82,14 @@ theorem Filter.Tendsto.isCoboundedUnder_ge [NeBot f] (h : Tendsto u f (𝓝 a))
 
 instance : BoundedGENhdsClass αᵒᵈ := ⟨@isBounded_le_nhds α _ _ _⟩
 
-instance : BoundedLENhdsClass (α × β) := by
+instance Prod.instBoundedLENhdsClass : BoundedLENhdsClass (α × β) := by
   refine ⟨fun x ↦ ?_⟩
   obtain ⟨a, ha⟩ := isBounded_le_nhds x.1
   obtain ⟨b, hb⟩ := isBounded_le_nhds x.2
   rw [← @Prod.mk.eta _ _ x, nhds_prod_eq]
   exact ⟨(a, b), ha.prod_mk hb⟩
 
-instance [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
+instance Pi.instBoundedLENhdsClass [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
     [∀ i, BoundedLENhdsClass (π i)] : BoundedLENhdsClass (∀ i, π i) := by
   refine' ⟨fun x ↦ _⟩
   rw [nhds_pi]
@@ -130,19 +130,12 @@ theorem Filter.Tendsto.isCoboundedUnder_le [NeBot f] (h : Tendsto u f (𝓝 a))
 
 instance : BoundedLENhdsClass αᵒᵈ := ⟨@isBounded_ge_nhds α _ _ _⟩
 
-instance : BoundedGENhdsClass (α × β) := by
-  refine ⟨fun x ↦ ?_⟩
-  obtain ⟨a, ha⟩ := isBounded_ge_nhds x.1
-  obtain ⟨b, hb⟩ := isBounded_ge_nhds x.2
-  rw [← @Prod.mk.eta _ _ x, nhds_prod_eq]
-  exact ⟨(a, b), ha.prod_mk hb⟩
+instance Prod.instBoundedGENhdsClass : BoundedGENhdsClass (α × β) :=
+  ⟨(Prod.instBoundedLENhdsClass (α := αᵒᵈ) (β := βᵒᵈ)).isBounded_le_nhds⟩
 
-instance [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
-    [∀ i, BoundedGENhdsClass (π i)] : BoundedGENhdsClass (∀ i, π i) := by
-  refine' ⟨fun x ↦ _⟩
-  rw [nhds_pi]
-  choose f hf using fun i ↦ isBounded_ge_nhds (x i)
-  exact ⟨f, eventually_pi hf⟩
+instance Pi.instBoundedGENhdsClass [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
+    [∀ i, BoundedGENhdsClass (π i)] : BoundedGENhdsClass (∀ i, π i) :=
+  ⟨(Pi.instBoundedLENhdsClass (π := fun i ↦ (π i)ᵒᵈ)).isBounded_le_nhds⟩
 
 end BoundedGENhdsClass