feat: Subgroup.mem_sup for arbitrary groups when one of the subgroups is normal (#31458)

We prove Subgroup.mem_sup for arbitrary (not necessarily commutative) groups when one of the subgroups is normal.

Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>

Author: bwangpj

Mathlib/Algebra/Group/Subgroup/Lattice.lean

@@ -603,6 +603,32 @@ theorem mem_sup : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x :=
 theorem mem_sup' : x ∈ s ⊔ t ↔ ∃ (y : s) (z : t), (y : C) * z = x :=
   mem_sup.trans <| by simp only [SetLike.exists, exists_prop]
 
+@[to_additive]
+theorem mem_sup_of_normal_right {s t : Subgroup G} [ht : t.Normal] {x : G} :
+    x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x := by
+  constructor
+  · intro hx; rw [sup_eq_closure] at hx
+    refine closure_induction ?_ ?_ ?_ ?_ hx
+    · rintro x (hx | hx)
+      · exact ⟨x, hx, 1, t.one_mem, by simp⟩
+      · exact ⟨1, s.one_mem, x, hx, by simp⟩
+    · exact ⟨1, s.one_mem, 1, t.one_mem, by simp⟩
+    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
+      exact ⟨y₁ * y₂, s.mul_mem hy₁ hy₂,
+            (y₂⁻¹ * z₁ * y₂) * z₂, t.mul_mem (ht.conj_mem' z₁ hz₁ y₂) hz₂, by simp [mul_assoc]⟩
+    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
+      exact ⟨y⁻¹, s.inv_mem hy,
+            y * z⁻¹ * y⁻¹, ht.conj_mem z⁻¹ (t.inv_mem hz) y, by simp [mul_assoc]⟩
+  · rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz
+
+@[to_additive]
+theorem mem_sup_of_normal_left {s t : Subgroup G} [hs : s.Normal] {x : G} :
+    x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x := by
+  have h := (sup_comm t s) ▸ mem_sup_of_normal_right (s := t) (t := s) (x := x)
+  exact h.trans
+    ⟨fun ⟨y, hy, z, hz, hp⟩ ↦ ⟨y * z * y⁻¹, hs.conj_mem z hz y, y, hy, by simp [hp]⟩,
+    fun ⟨y, hy, z, hz, hp⟩ ↦ ⟨z, hz, z⁻¹ * y * z, hs.conj_mem' y hy z, by simp [mul_assoc, hp]⟩⟩
+
 @[to_additive]
 theorem mem_closure_pair {x y z : C} :
     z ∈ closure ({x, y} : Set C) ↔ ∃ m n : ℤ, x ^ m * y ^ n = z := by