chore(Topology/../Nonarchimedean): minor golf (#9209)

leanprover-community · Dec 22, 2023 · 038fe40 · 038fe40
1 parent 503aade
commit 038fe40
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 10 deletions.
diff --git a/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean b/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
@@ -59,11 +59,7 @@ theorem of_comm {A ι : Type*} [CommRing A] (B : ι → AddSubgroup A)
   { inter
     mul
     leftMul
-    rightMul := by
-      intro x i
-      cases' leftMul x i with j hj
-      use j
-      simpa [mul_comm] using hj }
+    rightMul := fun x i ↦ (leftMul x i).imp fun j hj ↦ by simpa only [mul_comm] using hj }
 #align ring_subgroups_basis.of_comm RingSubgroupsBasis.of_comm
 
 /-- Every subgroups basis on a ring leads to a ring filter basis. -/

diff --git a/Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean b/Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean
@@ -142,11 +142,8 @@ theorem left_mul_subset (U : OpenAddSubgroup R) (r : R) :
 
 /-- An open subgroup of a nonarchimedean ring contains the square of another one. -/
 theorem mul_subset (U : OpenAddSubgroup R) : ∃ V : OpenAddSubgroup R, (V : Set R) * V ⊆ U := by
-  let ⟨V, H⟩ :=
-    prod_self_subset
-      (IsOpen.mem_nhds (IsOpen.preimage continuous_mul U.isOpen)
-        (by simpa only [Set.mem_preimage, SetLike.mem_coe, Prod.snd_zero,
-            mul_zero] using U.zero_mem))
+  let ⟨V, H⟩ := prod_self_subset <| (U.isOpen.preimage continuous_mul).mem_nhds <| by
+    simpa only [Set.mem_preimage, Prod.snd_zero, mul_zero] using U.zero_mem
   use V
   rintro v ⟨a, b, ha, hb, hv⟩
   have hy := H (Set.mk_mem_prod ha hb)