refactor(GroupAction/Blocks): additivise, fix names, golf API (#17578)

Most of the API can be additivised smoothly. The lemma names didn't match the naming convention. Some proofs were harder than necessary because of the suboptimal definition of `IsBlock` as `∀ _, _ ∨ _` rather than `∀ _, _ → _`.

From LeanCamCombi

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 ι) :

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 <|