feat(group_theory/subgroup/basic): One-sided closure induction lemmas (…

…#12725)

This PR adds one-sided closure induction lemmas, which I will need for Schreier's lemma.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/group_theory/subgroup/basic.lean

@@ -834,6 +834,18 @@ begin
   { simp only [true_and, coe_to_submonoid, union_subset_iff, subset_closure, inv_subset_closure] }
 end
 
+@[to_additive] lemma closure_induction_left {p : G → Prop} {x : G}
+  (h : x ∈ closure k) (H1 : p 1) (Hmul : ∀ (x ∈ k) y, p y → p (x * y))
+  (Hinv : ∀ (x ∈ k) y, p y → p (x⁻¹ * y)) : p x :=
+let key := le_of_eq (closure_to_submonoid k) in submonoid.closure_induction_left (key h) H1
+  (λ x hx, hx.elim (Hmul x) (λ hx y hy, (congr_arg _ (inv_inv x)).mp (Hinv x⁻¹ hx y hy)))
+
+@[to_additive] lemma closure_induction_right {p : G → Prop} {x : G}
+  (h : x ∈ closure k) (H1 : p 1) (Hmul : ∀ x (y ∈ k), p x → p (x * y))
+  (Hinv : ∀ x (y ∈ k), p x → p (x * y⁻¹)) : p x :=
+let key := le_of_eq (closure_to_submonoid k) in submonoid.closure_induction_right (key h) H1
+  (λ x y hy, hy.elim (Hmul x y) (λ hy hx, (congr_arg _ (inv_inv y)).mp (Hinv x y⁻¹ hy hx)))
+
 /-- An induction principle for closure membership. If `p` holds for `1` and all elements of
 `k` and their inverse, and is preserved under multiplication, then `p` holds for all elements of
 the closure of `k`. -/
@@ -843,15 +855,8 @@ elements of the additive closure of `k`."]
 lemma closure_induction'' {p : G → Prop} {x} (h : x ∈ closure k)
   (Hk : ∀ x ∈ k, p x) (Hk_inv : ∀ x ∈ k, p x⁻¹) (H1 : p 1)
   (Hmul : ∀ x y, p x → p y → p (x * y)) : p x :=
-begin
-  rw [← mem_to_submonoid, closure_to_submonoid k] at h,
-  refine submonoid.closure_induction h (λ x hx, _) H1 (λ x y hx hy, Hmul x y hx hy),
-  { rw [mem_union, mem_inv] at hx,
-    cases hx with mem invmem,
-    { exact Hk x mem },
-    { rw [← inv_inv x],
-      exact Hk_inv _ invmem } },
-end
+closure_induction_left h H1 (λ x hx y hy, Hmul x y (Hk x hx) hy)
+  (λ x hx y hy, Hmul x⁻¹ y (Hk_inv x hx) hy)
 
 /-- An induction principle for elements of `⨆ i, S i`.
 If `C` holds for `1` and all elements of `S i` for all `i`, and is preserved under multiplication,

src/group_theory/submonoid/membership.lean

@@ -253,6 +253,24 @@ begin
   exact ⟨l, h1, (multiset.coe_prod l).trans h2⟩,
 end
 
+@[to_additive]
+lemma closure_induction_left {s : set M} {p : M → Prop} {x : M} (h : x ∈ closure s) (H1 : p 1)
+  (Hmul : ∀ (x ∈ s) y, p y → p (x * y)) : p x :=
+begin
+  rw closure_eq_mrange at h,
+  obtain ⟨l, rfl⟩ := h,
+  induction l using free_monoid.rec_on with x y ih,
+  { exact H1 },
+  { simpa only [map_mul, free_monoid.lift_eval_of] using Hmul _ x.prop _ ih }
+end
+
+@[to_additive]
+lemma closure_induction_right {s : set M} {p : M → Prop} {x : M} (h : x ∈ closure s) (H1 : p 1)
+  (Hmul : ∀ x (y ∈ s), p x → p (x * y)) : p x :=
+@closure_induction_left _ _ (mul_opposite.unop ⁻¹' s) (p ∘ mul_opposite.unop) (mul_opposite.op x)
+  (closure_induction h (λ x hx, subset_closure hx) (one_mem _) (λ x y hx hy, mul_mem _ hy hx))
+  H1 (λ x hx y, Hmul _ _ hx)
+
 /-- The submonoid generated by an element. -/
 def powers (n : M) : submonoid M :=
 submonoid.copy (powers_hom M n).mrange (set.range ((^) n : ℕ → M)) $