[Merged by Bors] - refactor: Remove leftCoset/rightCoset

Mathlib/Algebra/Category/GroupCat/EpiMono.lean

@@ -17,6 +17,8 @@ epimorphisms are surjective homomorphisms.
 
 noncomputable section
 
+open scoped Pointwise
+
 universe u v
 
 namespace MonoidHom
@@ -96,19 +98,18 @@ theorem mono_iff_injective : Mono f ↔ Function.Injective f :=
 
 namespace SurjectiveOfEpiAuxs
 
-local notation "X" => Set.range (Function.swap leftCoset f.range.carrier)
+set_option quotPrecheck false in
+local notation "X" => Set.range (· • (f.range : Set B) : B → Set B)
 
 /-- Define `X'` to be the set of all left cosets with an extra point at "infinity".
 -/
 inductive XWithInfinity
-  | fromCoset : Set.range (Function.swap leftCoset f.range.carrier) → XWithInfinity
+  | fromCoset : Set.range (· • (f.range : Set B) : B → Set B) → XWithInfinity
   | infinity : XWithInfinity
 #align Group.surjective_of_epi_auxs.X_with_infinity GroupCat.SurjectiveOfEpiAuxs.XWithInfinity
 
 open XWithInfinity Equiv.Perm
 
-open Coset
-
 local notation "X'" => XWithInfinity f
 
 local notation "∞" => XWithInfinity.infinity
@@ -118,7 +119,7 @@ local notation "SX'" => Equiv.Perm X'
 instance : SMul B X' where
   smul b x :=
     match x with
-    | fromCoset y => fromCoset ⟨b *l y, by
+    | fromCoset y => fromCoset ⟨b • y, by
           rw [← y.2.choose_spec, leftCoset_assoc]
           -- Porting note: should we make `Bundled.α` reducible?
           let b' : B := y.2.choose
@@ -142,27 +143,25 @@ theorem one_smul (x : X') : (1 : B) • x = x :=
 #align Group.surjective_of_epi_auxs.one_smul GroupCat.SurjectiveOfEpiAuxs.one_smul
 
 theorem fromCoset_eq_of_mem_range {b : B} (hb : b ∈ f.range) :
-    fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩ =
-      fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩ := by
+    fromCoset ⟨b • ↑f.range, b, rfl⟩ = fromCoset ⟨f.range, 1, one_leftCoset _⟩ := by
   congr
   let b : B.α := b
-  change b *l f.range = f.range
-  nth_rw 2 [show (f.range : Set B.α) = 1 *l f.range from (one_leftCoset _).symm]
+  change b • (f.range : Set B) = f.range
+  nth_rw 2 [show (f.range : Set B.α) = (1 : B) • f.range from (one_leftCoset _).symm]
   rw [leftCoset_eq_iff, mul_one]
   exact Subgroup.inv_mem _ hb
 #align Group.surjective_of_epi_auxs.from_coset_eq_of_mem_range GroupCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range
 
 example (G : Type) [Group G] (S : Subgroup G) : Set G := S
 
 theorem fromCoset_ne_of_nin_range {b : B} (hb : b ∉ f.range) :
-    fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩ ≠
-      fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩ := by
+    fromCoset ⟨b • ↑f.range, b, rfl⟩ ≠ fromCoset ⟨f.range, 1, one_leftCoset _⟩ := by
   intro r
   simp only [fromCoset.injEq, Subtype.mk.injEq] at r
   -- Porting note: annoying dance between types CoeSort.coe B, B.α, and B
   let b' : B.α := b
-  change b' *l f.range = f.range at r
-  nth_rw 2 [show (f.range : Set B.α) = 1 *l f.range from (one_leftCoset _).symm] at r
+  change b' • (f.range : Set B) = f.range at r
+  nth_rw 2 [show (f.range : Set B.α) = (1 : B) • f.range from (one_leftCoset _).symm] at r
   rw [leftCoset_eq_iff, mul_one] at r
   exact hb (inv_inv b ▸ Subgroup.inv_mem _ r)
 #align Group.surjective_of_epi_auxs.from_coset_ne_of_nin_range GroupCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range
@@ -173,36 +172,35 @@ instance : DecidableEq X' :=
 /-- Let `τ` be the permutation on `X'` exchanging `f.range` and the point at infinity.
 -/
 noncomputable def tau : SX' :=
-  Equiv.swap (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) ∞
+  Equiv.swap (fromCoset ⟨↑f.range, ⟨1, one_leftCoset _⟩⟩) ∞
 #align Group.surjective_of_epi_auxs.tau GroupCat.SurjectiveOfEpiAuxs.tau
 
 local notation "τ" => tau f
 
-theorem τ_apply_infinity : τ ∞ = fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩ :=
+theorem τ_apply_infinity : τ ∞ = fromCoset ⟨f.range, 1, one_leftCoset _⟩ :=
   Equiv.swap_apply_right _ _
 #align Group.surjective_of_epi_auxs.τ_apply_infinity GroupCat.SurjectiveOfEpiAuxs.τ_apply_infinity
 
-theorem τ_apply_fromCoset : τ (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) = ∞ :=
+theorem τ_apply_fromCoset : τ (fromCoset ⟨f.range, 1, one_leftCoset _⟩) = ∞ :=
   Equiv.swap_apply_left _ _
 #align Group.surjective_of_epi_auxs.τ_apply_fromCoset GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset
 
 theorem τ_apply_fromCoset' (x : B) (hx : x ∈ f.range) :
-    τ (fromCoset ⟨x *l f.range.carrier, ⟨x, rfl⟩⟩) = ∞ :=
+    τ (fromCoset ⟨x • ↑f.range, ⟨x, rfl⟩⟩) = ∞ :=
   (fromCoset_eq_of_mem_range _ hx).symm ▸ τ_apply_fromCoset _
 #align Group.surjective_of_epi_auxs.τ_apply_fromCoset' GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset'
 
-theorem τ_symm_apply_fromCoset :
-    (Equiv.symm τ) (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) = ∞ := by
+theorem τ_symm_apply_fromCoset : Equiv.symm τ (fromCoset ⟨f.range, 1, one_leftCoset _⟩) = ∞ := by
   rw [tau, Equiv.symm_swap, Equiv.swap_apply_left]
 #align Group.surjective_of_epi_auxs.τ_symm_apply_fromCoset GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset
 
 theorem τ_symm_apply_infinity :
-    (Equiv.symm τ) ∞ = fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩ := by
+    Equiv.symm τ ∞ = fromCoset ⟨f.range, 1, one_leftCoset _⟩ := by
   rw [tau, Equiv.symm_swap, Equiv.swap_apply_right]
 #align Group.surjective_of_epi_auxs.τ_symm_apply_infinity GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity
 
 /-- Let `g : B ⟶ S(X')` be defined as such that, for any `β : B`, `g(β)` is the function sending
-point at infinity to point at infinity and sending coset `y` to `β *l y`.
+point at infinity to point at infinity and sending coset `y` to `β • y`.
 -/
 def g : B →* SX' where
   toFun β :=
@@ -247,8 +245,8 @@ The strategy is the following: assuming `epi f`
 -/
 
 
-theorem g_apply_fromCoset (x : B) (y : X) : (g x) (fromCoset y)
-    = fromCoset ⟨x *l y, by aesop_cat⟩ := rfl
+theorem g_apply_fromCoset (x : B) (y : Set.range (· • (f.range : Set B) : B → Set B)) :
+    g x (fromCoset y) = fromCoset ⟨x • ↑y, by aesop_cat⟩ := rfl
 #align Group.surjective_of_epi_auxs.g_apply_fromCoset GroupCat.SurjectiveOfEpiAuxs.g_apply_fromCoset
 
 theorem g_apply_infinity (x : B) : (g x) ∞ = ∞ := rfl
@@ -262,55 +260,50 @@ theorem h_apply_infinity (x : B) (hx : x ∈ f.range) : (h x) ∞ = ∞ := by
 #align Group.surjective_of_epi_auxs.h_apply_infinity GroupCat.SurjectiveOfEpiAuxs.h_apply_infinity
 
 theorem h_apply_fromCoset (x : B) :
-    (h x) (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) =
-      fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩ := by
+    (h x) (fromCoset ⟨f.range, 1, one_leftCoset _⟩) =
+      fromCoset ⟨f.range, 1, one_leftCoset _⟩ := by
     change ((τ).symm.trans (g x)).trans τ _ = _
-    simp [τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]
+    simp [-MonoidHom.coe_range, τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]
 #align Group.surjective_of_epi_auxs.h_apply_fromCoset GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset
 
 theorem h_apply_fromCoset' (x : B) (b : B) (hb : b ∈ f.range) :
-    (h x) (fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩) =
-      fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩ :=
+    h x (fromCoset ⟨b • f.range, b, rfl⟩) = fromCoset ⟨b • ↑f.range, b, rfl⟩ :=
   (fromCoset_eq_of_mem_range _ hb).symm ▸ h_apply_fromCoset f x
 #align Group.surjective_of_epi_auxs.h_apply_fromCoset' GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset'
 
 theorem h_apply_fromCoset_nin_range (x : B) (hx : x ∈ f.range) (b : B) (hb : b ∉ f.range) :
-    (h x) (fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩) =
-      fromCoset ⟨x * b *l f.range.carrier, ⟨x * b, rfl⟩⟩ := by
+    h x (fromCoset ⟨b • f.range, b, rfl⟩) = fromCoset ⟨(x * b) • ↑f.range, x * b, rfl⟩ := by
   change ((τ).symm.trans (g x)).trans τ _ = _
   simp only [tau, MonoidHom.coe_mk, Equiv.toFun_as_coe, Equiv.coe_trans, Function.comp_apply]
   rw [Equiv.symm_swap,
-    @Equiv.swap_apply_of_ne_of_ne X' _ (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) ∞
-      (fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)]
+    @Equiv.swap_apply_of_ne_of_ne X' _ (fromCoset ⟨f.range, 1, one_leftCoset _⟩) ∞
+      (fromCoset ⟨b • ↑f.range, b, rfl⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)]
   simp only [g_apply_fromCoset, leftCoset_assoc]
   refine' Equiv.swap_apply_of_ne_of_ne (fromCoset_ne_of_nin_range _ fun r => hb _) (by simp)
   convert Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r
   rw [← mul_assoc, mul_left_inv, one_mul]
 #align Group.surjective_of_epi_auxs.h_apply_fromCoset_nin_range GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range
 
-theorem agree : f.range.carrier = { x | h x = g x } := by
+theorem agree : f.range = { x | h x = g x } := by
   refine' Set.ext fun b => ⟨_, fun hb : h b = g b => by_contradiction fun r => _⟩
   · rintro ⟨a, rfl⟩
     change h (f a) = g (f a)
     ext ⟨⟨_, ⟨y, rfl⟩⟩⟩
     · rw [g_apply_fromCoset]
       by_cases m : y ∈ f.range
       · rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
-        change fromCoset _ = fromCoset ⟨f a *l (y *l _), _⟩
-        simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m)]
-        congr
-        rw [leftCoset_assoc _ (f a) y]
+        change fromCoset _ = fromCoset ⟨f a • (y • _), _⟩
+        simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m), smul_smul]
       · rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
         simp only [leftCoset_assoc]
     · rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
-  · have eq1 : (h b) (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) =
-        fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩ := by
+  · have eq1 : (h b) (fromCoset ⟨f.range, 1, one_leftCoset _⟩) =
+        fromCoset ⟨f.range, 1, one_leftCoset _⟩ := by
       change ((τ).symm.trans (g b)).trans τ _ = _
       dsimp [tau]
       simp [g_apply_infinity f]
     have eq2 :
-      (g b) (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) =
-        fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩ := rfl
+      g b (fromCoset ⟨f.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.range, b, rfl⟩ := rfl
     exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, FunLike.congr_fun hb])
 #align Group.surjective_of_epi_auxs.agree GroupCat.SurjectiveOfEpiAuxs.agree
 

Mathlib/FieldTheory/KrullTopology.lean

@@ -236,7 +236,7 @@
       have h_nhd := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
       rw [mem_nhds_iff] at h_nhd
       rcases h_nhd with ⟨W, hWH, hW_open, hW_1⟩
-      refine' ⟨leftCoset f W, leftCoset g W,
+      refine' ⟨f • W, g • W,
         ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, _⟩⟩
       rw [Set.disjoint_left]
       rintro σ ⟨w1, hw1, h⟩ ⟨w2, hw2, rfl⟩
@@ -266,10 +266,10 @@
   rcases FunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩
   let E := IntermediateField.adjoin K ({x} : Set L)
   haveI := IntermediateField.adjoin.finiteDimensional (h_int x)
-  refine' ⟨leftCoset σ E.fixingSubgroup,
+  refine' ⟨σ • E.fixingSubgroup,
     ⟨E.fixingSubgroup_isOpen.leftCoset σ, E.fixingSubgroup_isClosed.leftCoset σ⟩,
     ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, _⟩
   simp only [mem_leftCoset_iff, SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff,
     not_forall]
   exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩
 #align krull_topology_totally_disconnected krullTopology_totallyDisconnected