diff --git a/Mathlib/Data/Set/Pairwise/Basic.lean b/Mathlib/Data/Set/Pairwise/Basic.lean
index 7365c110ac476..ec5b714ca6538 100644
--- a/Mathlib/Data/Set/Pairwise/Basic.lean
+++ b/Mathlib/Data/Set/Pairwise/Basic.lean
@@ -296,12 +296,8 @@ lemma PairwiseDisjoint.eq_or_disjoint
   exact h.elim hi hj
 
 lemma pairwiseDisjoint_range_iff {α β : Type*} {f : α → (Set β)} :
-    (Set.range f).PairwiseDisjoint id ↔ ∀ x y, f x = f y ∨ Disjoint (f x) (f y) := by
-  constructor
-  · intro h x y
-    apply h.eq_or_disjoint (Set.mem_range_self x) (Set.mem_range_self y)
-  · rintro h _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy
-    exact (h x y).resolve_left hxy
+    (range f).PairwiseDisjoint id ↔ ∀ x y, f x ≠ f y → Disjoint (f x) (f y) := by
+  aesop (add simp [PairwiseDisjoint, Set.Pairwise])
 
 /-- If the range of `f` is pairwise disjoint, then the image of any set `s` under `f` is as well. -/
 lemma _root_.Pairwise.pairwiseDisjoint (h : Pairwise (Disjoint on f)) (s : Set ι) :
diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean
index 547d1fc8f93c9..e890d7dc7383d 100644
--- a/Mathlib/GroupTheory/GroupAction/Basic.lean
+++ b/Mathlib/GroupTheory/GroupAction/Basic.lean
@@ -296,6 +296,8 @@ variable {G α β : Type*} [Group G] [MulAction G α] [MulAction G β]
 
 section Orbit
 
+-- TODO: This proof is redoing a special case of `MulAction.IsInvariantBlock.isBlock`. Can we move
+-- this lemma earlier to golf?
 @[to_additive (attr := simp)]
 theorem smul_orbit (g : G) (a : α) : g • orbit G a = orbit G a :=
   (smul_orbit_subset g a).antisymm <|
diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean
index cc63c90b25d16..054bfb7524698 100644
--- a/Mathlib/GroupTheory/GroupAction/Blocks.lean
+++ b/Mathlib/GroupTheory/GroupAction/Blocks.lean
@@ -3,11 +3,7 @@ Copyright (c) 2024 Antoine Chambert-Loir. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir
 -/
-
-import Mathlib.Algebra.Group.Subgroup.Actions
-import Mathlib.Data.Set.Card
 import Mathlib.Data.Setoid.Partition
-import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.Pointwise
 import Mathlib.GroupTheory.GroupAction.SubMulAction
 import Mathlib.GroupTheory.Index
@@ -39,10 +35,10 @@ that contain a given point is a block
 
 ## References
 
-We follow [wielandt1964].
-
+We follow [Wielandt-1964].
 -/
 
+open Set
 open scoped Pointwise
 
 namespace MulAction
@@ -51,12 +47,14 @@ section orbits
 
 variable {G : Type*} [Group G] {X : Type*} [MulAction G X]
 
+@[to_additive]
 theorem orbit.eq_or_disjoint (a b : X) :
     orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b) := by
   apply (em (Disjoint (orbit G a) (orbit G b))).symm.imp _ id
   simp (config := { contextual := true })
     only [Set.not_disjoint_iff, ← orbit_eq_iff, forall_exists_index, and_imp, eq_comm, implies_true]
 
+@[to_additive]
 theorem orbit.pairwiseDisjoint :
     (Set.range fun x : X => orbit G x).PairwiseDisjoint id := by
   rintro s ⟨x, rfl⟩ t ⟨y, rfl⟩ h
@@ -64,6 +62,7 @@ theorem orbit.pairwiseDisjoint :
   exact (orbit.eq_or_disjoint x y).resolve_right h
 
 /-- Orbits of an element form a partition -/
+@[to_additive]
 theorem IsPartition.of_orbits :
     Setoid.IsPartition (Set.range fun a : X => orbit G a) := by
   apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty
@@ -76,246 +75,201 @@ end orbits
 
 section SMul
 
-variable (G : Type*) {X : Type*} [SMul G X]
+variable (G : Type*) {X : Type*} [SMul G X] {B : Set X} {a : X}
 
 -- Change terminology : is_fully_invariant ?
-/-- For `SMul G X`, a fixed block is a `Set X` which is fully invariant:
-  `g • B = B` for all `g : G` -/
+/-- A set `B` is a `G`-fixed block if `g • B = B` for all `g : G`. -/
+@[to_additive "A set `B` is a `G`-fixed block if `g +ᵥ B = B` for all `g : G`."]
 def IsFixedBlock (B : Set X) := ∀ g : G, g • B = B
 
-/-- For `SMul G X`, an invariant block is a `Set X` which is stable:
-  `g • B ⊆ B` for all `g : G` -/
+/-- A set `B` is a `G`-invariant block if `g • B ⊆ B` for all `g : G`.
+
+Note: It is not necessarily a block when the action is not by a group. -/
+@[to_additive
+"A set `B` is a `G`-invariant block if `g +ᵥ B ⊆ B` for all `g : G`.
+
+Note: It is not necessarily a block when the action is not by a group. "]
 def IsInvariantBlock (B : Set X) := ∀ g : G, g • B ⊆ B
 
-/-- A trivial block is a `Set X` which is either a subsingleton or ⊤
-  (it is not necessarily a block…) -/
-def IsTrivialBlock (B : Set X) := B.Subsingleton ∨ B = ⊤
+/-- A trivial block is a `Set X` which is either a subsingleton or `univ`.
 
-/-- `For SMul G X`, a block is a `Set X` whose translates are pairwise disjoint -/
-def IsBlock (B : Set X) := (Set.range fun g : G => g • B).PairwiseDisjoint id
+Note: It is not necessarily a block when the action is not by a group. -/
+@[to_additive
+"A trivial block is a `Set X` which is either a subsingleton or `univ`.
+
+Note: It is not necessarily a block when the action is not by a group."]
+def IsTrivialBlock (B : Set X) := B.Subsingleton ∨ B = univ
+
+/-- A set `B` is a `G`-block iff the sets of the form `g • B` are pairwise equal or disjoint. -/
+@[to_additive
+"A set `B` is a `G`-block iff the sets of the form `g +ᵥ B` are pairwise equal or disjoint. "]
+def IsBlock (B : Set X) := ∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
 
 variable {G}
 
-/-- A set B is a block iff for all g, g',
-the sets g • B and g' • B are either equal or disjoint -/
-theorem IsBlock.def {B : Set X} :
-    IsBlock G B ↔ ∀ g g' : G, g • B = g' • B ∨ Disjoint (g • B) (g' • B) := by
-  apply Set.pairwiseDisjoint_range_iff
+@[to_additive]
+lemma isBlock_iff_smul_eq_smul_of_nonempty :
+    IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B := by
+  simp_rw [IsBlock, ← not_disjoint_iff_nonempty_inter, not_imp_comm]
+
+@[to_additive]
+lemma isBlock_iff_pairwiseDisjoint_range_smul :
+    IsBlock G B ↔ (range fun g : G ↦ g • B).PairwiseDisjoint id := pairwiseDisjoint_range_iff.symm
 
-/-- Alternate definition of a block -/
-theorem IsBlock.mk_notempty {B : Set X} :
-    IsBlock G B ↔ ∀ g g' : G, g • B ∩ g' • B ≠ ∅ → g • B = g' • B := by
-  simp_rw [IsBlock.def, or_iff_not_imp_right, Set.disjoint_iff_inter_eq_empty]
+@[to_additive]
+lemma isBlock_iff_smul_eq_smul_or_disjoint :
+    IsBlock G B ↔ ∀ g₁ g₂ : G, g₁ • B = g₂ • B ∨ Disjoint (g₁ • B) (g₂ • B) :=
+  forall₂_congr fun _ _ ↦ or_iff_not_imp_left.symm
 
-/-- A fixed block is a block -/
-theorem IsFixedBlock.isBlock {B : Set X} (hfB : IsFixedBlock G B) :
-    IsBlock G B := by
-  simp [IsBlock.def, hfB _]
+alias ⟨IsBlock.smul_eq_smul_of_nonempty, _⟩ := isBlock_iff_smul_eq_smul_of_nonempty
+alias ⟨IsBlock.pairwiseDisjoint_range_smul, _⟩ := isBlock_iff_pairwiseDisjoint_range_smul
+alias ⟨IsBlock.smul_eq_smul_or_disjoint, _⟩ := isBlock_iff_smul_eq_smul_or_disjoint
 
-variable (X)
+/-- A fixed block is a block. -/
+@[to_additive "A fixed block is a block."]
+lemma IsFixedBlock.isBlock (hfB : IsFixedBlock G B) : IsBlock G B := by simp [IsBlock, hfB _]
 
-/-- The empty set is a block -/
-theorem isBlock_empty : IsBlock G (⊥ : Set X) := by
-  simp [IsBlock.def, Set.bot_eq_empty, Set.smul_set_empty]
+/-- The empty set is a block. -/
+@[to_additive (attr := simp) "The empty set is a block."]
+lemma IsBlock.empty : IsBlock G (∅ : Set X) := by simp [IsBlock]
 
-variable {X}
+/-- A singleton is a block. -/
+@[to_additive "A singleton is a block."]
+lemma IsBlock.singleton : IsBlock G ({a} : Set X) := by simp [IsBlock]
 
-theorem isBlock_singleton (a : X) : IsBlock G ({a} : Set X) := by
-  simp [IsBlock.def, Classical.or_iff_not_imp_left]
+/-- Subsingletons are (trivial) blocks. -/
+@[to_additive "Subsingletons are (trivial) blocks."]
+lemma IsBlock.of_subsingleton (hB : B.Subsingleton) : IsBlock G B :=
+  hB.induction_on .empty fun _ ↦ .singleton
 
-/-- Subsingletons are (trivial) blocks -/
-theorem isBlock_subsingleton {B : Set X} (hB : B.Subsingleton) :
-    IsBlock G B :=
-  hB.induction_on (isBlock_empty _) isBlock_singleton
+/-- A fixed block is an invariant block. -/
+@[to_additive "A fixed block is an invariant block."]
+lemma IsFixedBlock.isInvariantBlock (hB : IsFixedBlock G B) : IsInvariantBlock G B :=
+  fun _ ↦ (hB _).le
 
 end SMul
 
 section Group
 
-variable {G : Type*} [Group G] {X : Type*} [MulAction G X]
+variable {G : Type*} [Group G] {X : Type*} [MulAction G X] {B : Set X}
+
+@[to_additive]
+lemma isBlock_iff_disjoint_smul_of_ne :
+    IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B := by
+  refine ⟨fun hB g ↦ by simpa using hB (g₂ := 1), fun hB g₁ g₂ h ↦ ?_⟩
+  simp only [disjoint_smul_set_right, ne_eq, ← inv_smul_eq_iff, smul_smul] at h ⊢
+  exact hB h
+
+@[to_additive]
+lemma isBlock_iff_smul_eq_of_nonempty :
+    IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B := by
+  simp_rw [isBlock_iff_disjoint_smul_of_ne, ← not_disjoint_iff_nonempty_inter, not_imp_comm]
+
+@[to_additive]
+lemma isBlock_iff_smul_eq_or_disjoint :
+    IsBlock G B ↔ ∀ g : G, g • B = B ∨ Disjoint (g • B) B :=
+  isBlock_iff_disjoint_smul_of_ne.trans <| forall_congr' fun _ ↦ or_iff_not_imp_left.symm
+
+@[to_additive]
+lemma isBlock_iff_smul_eq_of_mem :
+    IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B := by
+  simp [isBlock_iff_smul_eq_of_nonempty, Set.Nonempty, mem_smul_set]
+
+@[to_additive] alias ⟨IsBlock.disjoint_smul_of_ne, _⟩ := isBlock_iff_disjoint_smul_of_ne
+@[to_additive] alias ⟨IsBlock.smul_eq_of_nonempty, _⟩ := isBlock_iff_smul_eq_of_nonempty
+@[to_additive] alias ⟨IsBlock.smul_eq_or_disjoint, _⟩ := isBlock_iff_smul_eq_or_disjoint
+@[to_additive] alias ⟨IsBlock.smul_eq_of_mem, _⟩ := isBlock_iff_smul_eq_of_mem
+
+-- TODO: Generalise to `SubgroupClass`
+/-- If `B` is a `G`-block, then it is also a `H`-block for any subgroup `H` of `G`. -/
+@[to_additive
+"If `B` is a `G`-block, then it is also a `H`-block for any subgroup `H` of `G`."]
+lemma IsBlock.subgroup {H : Subgroup G} (hB : IsBlock G B) : IsBlock H B := fun _ _ h ↦ hB h
+
+/-- A block of a group action is invariant iff it is fixed. -/
+@[to_additive "A block of a group action is invariant iff it is fixed."]
+lemma isInvariantBlock_iff_isFixedBlock : IsInvariantBlock G B ↔ IsFixedBlock G B :=
+  ⟨fun hB g ↦ (hB g).antisymm <| subset_set_smul_iff.2 <| hB _, IsFixedBlock.isInvariantBlock⟩
+
+/-- An invariant block of a group action is a fixed block. -/
+@[to_additive "An invariant block of a group action is a fixed block."]
+alias ⟨IsInvariantBlock.isFixedBlock, _⟩ := isInvariantBlock_iff_isFixedBlock
+
+/-- An invariant block  of a group action is a block. -/
+@[to_additive "An invariant block of a group action is a block."]
+lemma IsInvariantBlock.isBlock (hB : IsInvariantBlock G B) : IsBlock G B := hB.isFixedBlock.isBlock
+
+/-- The full set is a fixed block. -/
+@[to_additive "The full set is a fixed block."]
+lemma IsFixedBlock.univ : IsFixedBlock G (univ : Set X) := fun _ ↦ by simp
+
+/-- The full set is a block. -/
+@[to_additive (attr := simp) "The full set is a block."]
+lemma IsBlock.univ : IsBlock G (univ : Set X) := IsFixedBlock.univ.isBlock
+
+/-- The intersection of two blocks is a block. -/
+@[to_additive "The intersection of two blocks is a block."]
+lemma IsBlock.inter {B₁ B₂ : Set X} (h₁ : IsBlock G B₁) (h₂ : IsBlock G B₂) :
+    IsBlock G (B₁ ∩ B₂) := by
+  simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_inter] at h₁ h₂ ⊢
+  rintro g₁ g₂ ⟨a, ha₁, ha₂⟩
+  rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩]
 
-theorem IsBlock.smul_eq_or_disjoint {B : Set X} (hB : IsBlock G B) (g : G) :
-    g • B = B ∨ Disjoint (g • B) B := by
-  rw [IsBlock.def] at hB
-  simpa only [one_smul] using hB g 1
-
-theorem IsBlock.def_one {B : Set X} :
-    IsBlock G B ↔ ∀ g : G, g • B = B ∨ Disjoint (g • B) B := by
-  refine ⟨IsBlock.smul_eq_or_disjoint, ?_⟩
-  rw [IsBlock.def]
-  intro hB g g'
-  apply (hB (g'⁻¹ * g)).imp
-  · rw [← smul_smul, ← eq_inv_smul_iff, inv_inv]
-    exact id
-  · intro h
-    rw [Set.disjoint_iff] at h ⊢
-    rintro x hx
-    suffices g'⁻¹ • x ∈ (g'⁻¹ * g) • B ∩ B by apply h this
-    rw [Set.mem_inter_iff]
-    simp only [← smul_smul, ← Set.mem_smul_set_iff_inv_smul_mem, smul_inv_smul]
-    exact hx
-
-theorem IsBlock.mk_notempty_one {B : Set X} :
-    IsBlock G B ↔ ∀ g : G, g • B ∩ B ≠ ∅ → g • B = B := by
-  simp_rw [IsBlock.def_one, Set.disjoint_iff_inter_eq_empty, or_iff_not_imp_right]
-
-theorem IsBlock.mk_mem {B : Set X} :
-    IsBlock G B ↔ ∀ (g : G) (a : X) (_ : a ∈ B) (_ : g • a ∈ B), g • B = B := by
-  rw [IsBlock.mk_notempty_one]
-  simp only [← Set.nonempty_iff_ne_empty, Set.nonempty_def, Set.mem_inter_iff,
-    exists_imp, and_imp, Set.mem_smul_set_iff_inv_smul_mem]
-  constructor
-  · intro H g a ha hga
-    apply H g (g • a) _ hga
-    simpa only [inv_smul_smul] using ha
-  · intro H g a ha hga
-    rw [← eq_inv_smul_iff, eq_comm]
-    exact H g⁻¹ a hga ha
-
-theorem IsBlock.def_mem {B : Set X} (hB : IsBlock G B) {a : X} {g : G} :
-    a ∈ B → g • a ∈ B → g • B = B :=
-  IsBlock.mk_mem.mp hB g a
-
-theorem IsBlock.mk_subset {B : Set X} :
-    IsBlock G B ↔ ∀ {g : G} {b : X} (_ : b ∈ B) (_ : b ∈ g • B), g • B ⊆ B := by
-  simp_rw [IsBlock.mk_notempty_one, ← Set.nonempty_iff_ne_empty]
-  constructor
-  · intro hB g b hb hgb
-    exact (hB g ⟨b, hgb, hb⟩).le
-  · intro hB g ⟨b, hb', hb⟩
-    apply le_antisymm (hB hb hb')
-    suffices g⁻¹ • B ≤ B by
-      rw [Set.le_iff_subset] at this ⊢
-      rwa [← inv_inv g, ← Set.set_smul_subset_iff]
-    exact hB (Set.mem_smul_set_iff_inv_smul_mem.mp hb') (Set.smul_mem_smul_set_iff.mpr hb)
-
-/-- An invariant block is a fixed block -/
-theorem IsInvariantBlock.isFixedBlock {B : Set X} (hfB : IsInvariantBlock G B) :
-    IsFixedBlock G B := by
-  intro g
-  apply le_antisymm (hfB g)
-  intro x hx
-  rw [Set.mem_smul_set_iff_inv_smul_mem]
-  apply hfB g⁻¹
-  rwa [Set.smul_mem_smul_set_iff]
-
-/-- An invariant block is a block -/
-theorem IsInvariantBlock.isBlock {B : Set X} (hfB : IsInvariantBlock G B) :
-    IsBlock G B :=
-  hfB.isFixedBlock.isBlock
-
-/-- An orbit is a block -/
-theorem isFixedBlock_orbit (a : X) : IsFixedBlock G (orbit G a) :=
-  (smul_orbit · a)
-
-/-- An orbit is a block -/
-theorem isBlock_orbit (a : X) : IsBlock G (orbit G a) :=
-  (isFixedBlock_orbit a).isBlock
-
-variable (X)
-
-/-- The full set is a (trivial) block -/
-theorem isFixedBlock_univ : IsFixedBlock G (Set.univ : Set X) :=
-  fun _ ↦ by simp only [Set.smul_set_univ]
-@[deprecated (since := "2024-09-14")] alias isFixedBlock_top := isFixedBlock_univ
-
-/-- The full set is a (trivial) block -/
-theorem isBlock_univ : IsBlock G (Set.univ : Set X) :=
-  (isFixedBlock_univ _).isBlock
-
-variable {X}
-
-/-- Is `B` is a block for an action of `G`, it is a block for the action of any subgroup of `G` -/
-theorem IsBlock.subgroup {H : Subgroup G} {B : Set X} (hfB : IsBlock G B) :
-    IsBlock H B := by
-  rw [IsBlock.def_one]; rintro ⟨g, _⟩
-  simpa only using hfB.smul_eq_or_disjoint g
-
-theorem IsBlock.preimage {H Y : Type*} [Group H] [MulAction H Y]
-    {φ : H → G} (j : Y →ₑ[φ] X) {B : Set X} (hB : IsBlock G B) :
+/-- An intersection of blocks is a block. -/
+@[to_additive "An intersection of blocks is a block."]
+lemma IsBlock.iInter {ι : Sort*} {B : ι → Set X} (hB : ∀ i, IsBlock G (B i)) :
+    IsBlock G (⋂ i, B i) := by
+  simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_iInter] at hB ⊢
+  rintro g₁ g₂ ⟨a, ha₁, ha₂⟩
+  simp_rw [fun i ↦ hB i ⟨a, iInter_subset _ i ha₁, iInter_subset _ i ha₂⟩]
+
+/-- A trivial block is a block. -/
+@[to_additive "A trivial block is a block."]
+lemma IsTrivialBlock.isBlock (hB : IsTrivialBlock B) : IsBlock G B := by
+  obtain hB | rfl := hB
+  · exact .of_subsingleton hB
+  · exact .univ
+
+/-- An orbit is a fixed block. -/
+@[to_additive "An orbit is a fixed block."]
+protected lemma IsFixedBlock.orbit (a : X) : IsFixedBlock G (orbit G a) := (smul_orbit · a)
+
+/-- An orbit is a block. -/
+@[to_additive "An orbit is a block."]
+protected lemma IsBlock.orbit (a : X) : IsBlock G (orbit G a) := (IsFixedBlock.orbit a).isBlock
+
+@[to_additive]
+lemma isBlock_top : IsBlock (⊤ : Subgroup G) B ↔ IsBlock G B :=
+  Subgroup.topEquiv.toEquiv.forall_congr fun _ ↦ Subgroup.topEquiv.toEquiv.forall_congr_left
+
+lemma IsBlock.preimage {H Y : Type*} [Group H] [MulAction H Y]
+    {φ : H → G} (j : Y →ₑ[φ] X) (hB : IsBlock G B) :
     IsBlock H (j ⁻¹' B) := by
-  rw [IsBlock.def_one]
-  intro g
-  rw [← Group.preimage_smul_setₛₗ Y X φ j]
-  apply (hB.smul_eq_or_disjoint (φ g)).imp
-  · intro heq
-    rw [heq]
-  · exact Disjoint.preimage _
+  rintro g₁ g₂ hg
+  rw [← Group.preimage_smul_setₛₗ, ← Group.preimage_smul_setₛₗ] at hg ⊢
+  exact (hB <| ne_of_apply_ne _ hg).preimage _
 
 theorem IsBlock.image {H Y : Type*} [Group H] [MulAction H Y]
     {φ : G →* H} (j : X →ₑ[φ] Y)
     (hφ : Function.Surjective φ) (hj : Function.Injective j)
-    {B : Set X} (hB : IsBlock G B) :
+    (hB : IsBlock G B) :
     IsBlock H (j '' B) := by
-  rw [IsBlock.def]
-  intro h h'
-  obtain ⟨g, rfl⟩ := hφ h
-  obtain ⟨g', rfl⟩ := hφ h'
-  simp only [← image_smul_setₛₗ X Y φ j]
-  cases' IsBlock.def.mp hB g g' with h h
-  · left; rw [h]
-  · right; exact Set.disjoint_image_of_injective hj h
-
-theorem IsBlock.subtype_val_preimage {C : SubMulAction G X} {B : Set X} (hB : IsBlock G B) :
+  simp only [IsBlock, hφ.forall, ← image_smul_setₛₗ]
+  exact fun g₁ g₂ hg ↦ disjoint_image_of_injective hj <| hB <| ne_of_apply_ne _ hg
+
+theorem IsBlock.subtype_val_preimage {C : SubMulAction G X} (hB : IsBlock G B) :
     IsBlock G (Subtype.val ⁻¹' B : Set C) :=
   hB.preimage C.inclusion
 
-theorem IsBlock.iff_subtype_val {C : SubMulAction G X} {B : Set C} :
-    IsBlock G B ↔ IsBlock G (Subtype.val '' B : Set X) := by
-  simp only [IsBlock.def_one]
-  apply forall_congr'
-  intro g
-  rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set _ _ _ C.inclusion g B,
-    ← Set.image_eq_image Subtype.coe_injective]
-  apply or_congr Iff.rfl
-  simp only [Set.disjoint_iff, Set.subset_empty_iff, Set.image_eq_empty,
-    ← C.inclusion_injective.injOn.image_inter (Set.subset_univ _) (Set.subset_univ _)]
-
-theorem IsBlock.iff_top (B : Set X) :
-    IsBlock G B ↔ IsBlock (⊤ : Subgroup G) B := by
-  simp only [IsBlock.def_one]
-  constructor
-  · intro h g; exact h g
-  · intro h g; exact h ⟨g, Subgroup.mem_top g⟩
+theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} :
+    IsBlock G (Subtype.val '' B : Set X) ↔ IsBlock G B := by
+  refine forall₂_congr fun g₁ g₂ ↦ ?_
+  rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set, ← image_smul_set, ne_eq,
+    Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective]
 
-/-- The intersection of two blocks is a block -/
-theorem IsBlock.inter {B₁ B₂ : Set X} (h₁ : IsBlock G B₁) (h₂ : IsBlock G B₂) :
-    IsBlock G (B₁ ∩ B₂) := by
-  rw [IsBlock.def_one]
-  intro g
-  rw [Set.smul_set_inter]
-  cases' h₁.smul_eq_or_disjoint g with h₁ h₁
-  · cases' h₂.smul_eq_or_disjoint g with h₂ h₂
-    · left; rw [h₁, h₂]
-    right
-    apply Disjoint.inter_left'; apply Disjoint.inter_right'
-    exact h₂
-  · right
-    apply Disjoint.inter_left; apply Disjoint.inter_right
-    exact h₁
-
-/-- An intersection of blocks is a block -/
-theorem IsBlock.iInter {ι : Type*} {B : ι → Set X} (hB : ∀ i : ι, IsBlock G (B i)) :
-    IsBlock G (⋂ i, B i) := by
-  by_cases hι : (IsEmpty ι)
-  · -- ι = ∅, block = univ
-    suffices (⋂ i : ι, B i) = Set.univ by simpa only [this] using isBlock_univ X
-    simpa only [Set.iInter_eq_univ] using (hι.elim' ·)
-  rw [IsBlock.def_one]
-  intro g
-  rw [Set.smul_set_iInter]
-  by_cases h : ∃ i : ι, Disjoint (g • B i) (B i)
-  · right
-    obtain ⟨j, hj⟩ := h
-    refine Disjoint.mono ?_ ?_ hj <;> apply Set.iInter_subset
-  · left
-    simp only [not_exists] at h
-    have : ∀ i : ι, g • B i = B i := fun i => ((hB i).smul_eq_or_disjoint g).resolve_right (h i)
-    rw [Set.iInter_congr this]
-
-theorem IsBlock.of_subgroup_of_conjugate {B : Set X} {H : Subgroup G} (hB : IsBlock H B) (g : G) :
+theorem IsBlock.of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g : G) :
     IsBlock (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H) (g • B) := by
-  rw [IsBlock.def_one]
+  rw [isBlock_iff_smul_eq_or_disjoint]
   intro h'
   obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h')
   simp only [MulEquiv.coe_toMonoidHom, MulAut.conj_apply] at hh
@@ -329,9 +283,9 @@ theorem IsBlock.of_subgroup_of_conjugate {B : Set X} {H : Subgroup G} (hB : IsBl
   rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right]
 
 /-- A translate of a block is a block -/
-theorem IsBlock.translate {B : Set X} (g : G) (hB : IsBlock G B) :
+theorem IsBlock.translate (g : G) (hB : IsBlock G B) :
     IsBlock G (g • B) := by
-  rw [IsBlock.iff_top] at hB ⊢
+  rw [← isBlock_top] at hB ⊢
   rw [← Subgroup.map_comap_eq_self_of_surjective (f := MulAut.conj g) (MulAut.conj g).surjective ⊤]
   apply IsBlock.of_subgroup_of_conjugate
   rwa [Subgroup.comap_top]
@@ -339,12 +293,11 @@ theorem IsBlock.translate {B : Set X} (g : G) (hB : IsBlock G B) :
 variable (G) in
 /-- For `SMul G X`, a block system of `X` is a partition of `X` into blocks
   for the action of `G` -/
-def IsBlockSystem (B : Set (Set X)) :=
-  Setoid.IsPartition B ∧ ∀ b : Set X, b ∈ B → IsBlock G b
+def IsBlockSystem (ℬ : Set (Set X)) := Setoid.IsPartition ℬ ∧ ∀ ⦃B⦄, B ∈ ℬ → IsBlock G B
 
-/-- Translates of a block form a `block_system` -/
+/-- Translates of a block form a block system. -/
 theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X]
-    {B : Set X} (hB : IsBlock G B) (hBe : B.Nonempty) :
+    (hB : IsBlock G B) (hBe : B.Nonempty) :
     IsBlockSystem G (Set.range fun g : G => g • B) := by
   refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩
   case mem_blocks => rintro B' ⟨g, rfl⟩; exact hB.translate g
@@ -359,10 +312,7 @@ theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X]
     simp only [Set.smul_mem_smul_set_iff, hb, exists_unique_iff_exists, Set.mem_range,
       exists_apply_eq_apply, exists_const, exists_prop, and_imp, forall_exists_index,
       forall_apply_eq_imp_iff, true_and]
-    intro g' ha
-    apply (IsBlock.def.mp hB g' g).resolve_right
-    rw [Set.not_disjoint_iff]
-    refine ⟨g • b, ha, ⟨b, hb, rfl⟩⟩
+    exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩
 
 section Normal
 
@@ -382,9 +332,9 @@ lemma smul_orbit_eq_orbit_smul (N : Subgroup G) [nN : N.Normal] (a : X) (g : G)
     simp only [← mul_assoc, ← smul_smul, smul_inv_smul, inv_inv]
 
 /-- An orbit of a normal subgroup is a block -/
-theorem orbit.isBlock_of_normal {N : Subgroup G} [N.Normal] (a : X) :
+theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) :
     IsBlock G (orbit N a) := by
-  rw [IsBlock.def_one]
+  rw [isBlock_iff_smul_eq_or_disjoint]
   intro g
   rw [smul_orbit_eq_orbit_smul]
   apply orbit.eq_or_disjoint
@@ -395,7 +345,48 @@ theorem IsBlockSystem.of_normal {N : Subgroup G} [N.Normal] :
   constructor
   · apply IsPartition.of_orbits
   · intro b; rintro ⟨a, rfl⟩
-    exact orbit.isBlock_of_normal a
+    exact .orbit_of_normal a
+
+section Group
+variable {S H : Type*} [Group H] [SetLike S H] [SubgroupClass S H] {s : S} {a b : G}
+
+/-!
+Annoyingly, it seems like the following two lemmas cannot be unified.
+-/
+
+section Left
+variable [MulAction G H] [IsScalarTower G H H]
+
+/-- See `MulAction.isBlock_subgroup'` for a version that works for the right action of a group on
+itself. -/
+@[to_additive "See `AddAction.isBlock_subgroup'` for a version that works for the right action
+of a group on itself."]
+lemma isBlock_subgroup : IsBlock G (s : Set H) := by
+  simp only [IsBlock, disjoint_left]
+  rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩
+  refine hab ?_
+  rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]
+
+end Left
+
+section Right
+variable [MulAction G H] [IsScalarTower G Hᵐᵒᵖ H]
+
+open MulOpposite
+
+/-- See `MulAction.isBlock_subgroup` for a version that works for the left action of a group on
+itself. -/
+@[to_additive "See `AddAction.isBlock_subgroup` for a version that works for the left action
+of a group on itself."]
+lemma isBlock_subgroup' : IsBlock G (s : Set H) := by
+  simp only [IsBlock, disjoint_left]
+  rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩
+  refine hab ?_
+  rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
+    op_smul_coe_set hd]
+
+end Right
+end Group
 
 end Normal
 
@@ -411,28 +402,21 @@ section Stabilizer
 /-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block -/
 theorem IsBlock.of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ H) :
     IsBlock G (MulAction.orbit H a) := by
-  simp_rw [IsBlock.def_one, or_iff_not_imp_right, Set.not_disjoint_iff]
-  rintro g ⟨-, ⟨-, ⟨h₁, rfl⟩, h⟩, ⟨h₂, rfl⟩⟩
+  rw [isBlock_iff_smul_eq_of_nonempty]
+  rintro g ⟨-, ⟨-, ⟨h₁, rfl⟩, h⟩, h₂, rfl⟩
   suffices g ∈ H by
     rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]
   rw [← mul_mem_cancel_left h₂⁻¹.2, ← mul_mem_cancel_right h₁.2]
   apply hH
-  simp only [mem_stabilizer_iff, InvMemClass.coe_inv, mul_smul, inv_smul_eq_iff]
-  exact h
+  simpa only [mem_stabilizer_iff, InvMemClass.coe_inv, mul_smul, inv_smul_eq_iff]
 
 /-- If `B` is a block containing `a`, then the stabilizer of `B` contains the stabilizer of `a` -/
-theorem IsBlock.stabilizer_le {B : Set X} (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
-    stabilizer G a ≤ stabilizer G B := by
-  intro g hg
-  apply Or.resolve_right (hB.smul_eq_or_disjoint g)
-  rw [Set.not_disjoint_iff]
-  refine ⟨a, ?_, ha⟩
-  rw [← hg, Set.smul_mem_smul_set_iff]
-  exact ha
+theorem IsBlock.stabilizer_le (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
+    stabilizer G a ≤ stabilizer G B :=
+  fun g hg ↦ hB.smul_eq_of_nonempty ⟨a, by rwa [← hg, smul_mem_smul_set_iff], ha⟩
 
 /-- A block containing `a` is the orbit of `a` under its stabilizer -/
-theorem IsBlock.orbit_stabilizer_eq
-    [htGX : IsPretransitive G X] {B : Set X} (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
+theorem IsBlock.orbit_stabilizer_eq [IsPretransitive G X] (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
     MulAction.orbit (stabilizer G B) a = B := by
   ext x
   constructor
@@ -442,7 +426,7 @@ theorem IsBlock.orbit_stabilizer_eq
     exact ha
   · intro hx
     obtain ⟨k, rfl⟩ := exists_smul_eq G a x
-    exact ⟨⟨k, hB.def_mem ha hx⟩, rfl⟩
+    exact ⟨⟨k, hB.smul_eq_of_mem ha hx⟩, rfl⟩
 
 /-- A subgroup containing the stabilizer of `a`
   is the stabilizer of the orbit of `a` under that subgroup -/
@@ -479,9 +463,9 @@ def block_stabilizerOrderIso [htGX : IsPretransitive G X] (a : X) :
       obtain ⟨k, rfl⟩ := htGX.exists_smul_eq a b
       suffices k ∈ stabilizer G B' by
         exact this.symm ▸ (Set.smul_mem_smul_set ha')
-      exact hBB' (hB.def_mem ha hb)
+      exact hBB' (hB.smul_eq_of_mem ha hb)
     · intro hBB' g hgB
-      apply IsBlock.def_mem hB' ha'
+      apply hB'.smul_eq_of_mem ha'
       exact hBB' <| hgB.symm ▸ (Set.smul_mem_smul_set ha)
 
 end Stabilizer
@@ -552,7 +536,7 @@ theorem of_subset {B : Set X} (a : X) (hfB : B.Finite) :
     IsBlock G (⋂ (k : G) (_ : a ∈ k • B), k • B) := by
   let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B
   cases' Set.eq_empty_or_nonempty B with hfB_e hfB_ne
-  · simp [hfB_e, isBlock_univ]
+  · simp [hfB_e]
   have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by
     intro k hk
     exact Set.biInter_subset_of_mem hk
@@ -569,10 +553,8 @@ theorem of_subset {B : Set X} (a : X) (hfB : B.Finite) :
   have hag' (g : G) (hg : a ∈ g • B') : B' = g • B' := by
     rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_of_finite_iff_le_smul _ hfB']
     exact hag g hg
-  rw [mk_notempty_one]
-  intro g hg
-  rw [← Set.nonempty_iff_ne_empty] at hg
-  obtain ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩ := Set.nonempty_def.mp hg
+  rw [isBlock_iff_smul_eq_of_nonempty]
+  rintro g ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩
   obtain ⟨k : G, hk : k • a = b⟩ := exists_smul_eq G a b
   have hak : a ∈ k⁻¹ • B' := by
     refine ⟨b, hb, ?_⟩