feat(GroupTheory/GroupAction/Basic): orbit lemmas for product (#13580)

Add a few basic lemmas about orbits in relation to the action of a monoid or group on `α × β` induced by its actions on `α` and `β`.

From AperiodicMonotilesLean.

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -38,7 +38,7 @@ open Function
 
 namespace MulAction
 
-variable (M : Type u) [Monoid M] (α : Type v) [MulAction M α]
+variable (M : Type u) [Monoid M] (α : Type v) [MulAction M α] {β : Type*} [MulAction M β]
 
 section Orbit
 
@@ -117,6 +117,18 @@ lemma mem_orbit_of_mem_orbit_submonoid {S : Submonoid M} {a b : α} (h : a ∈ o
     a ∈ orbit M b :=
   orbit_submonoid_subset S _ h
 
+@[to_additive]
+lemma fst_mem_orbit_of_mem_orbit {x y : α × β} (h : x ∈ MulAction.orbit M y) :
+    x.1 ∈ MulAction.orbit M y.1 := by
+  rcases h with ⟨g, rfl⟩
+  exact mem_orbit _ _
+
+@[to_additive]
+lemma snd_mem_orbit_of_mem_orbit {x y : α × β} (h : x ∈ MulAction.orbit M y) :
+    x.2 ∈ MulAction.orbit M y.2 := by
+  rcases h with ⟨g, rfl⟩
+  exact mem_orbit _ _
+
 variable (M)
 
 @[to_additive]
@@ -668,6 +680,18 @@ def selfEquivSigmaOrbits : α ≃ Σω : Ω, orbit G ω.out' :=
 #align mul_action.self_equiv_sigma_orbits MulAction.selfEquivSigmaOrbits
 #align add_action.self_equiv_sigma_orbits AddAction.selfEquivSigmaOrbits
 
+variable (β)
+
+@[to_additive]
+lemma orbitRel_le_fst :
+    orbitRel G (α × β) ≤ (orbitRel G α).comap Prod.fst :=
+  Setoid.le_def.2 fst_mem_orbit_of_mem_orbit
+
+@[to_additive]
+lemma orbitRel_le_snd :
+    orbitRel G (α × β) ≤ (orbitRel G β).comap Prod.snd :=
+  Setoid.le_def.2 snd_mem_orbit_of_mem_orbit
+
 end Orbit
 
 section Stabilizer