feat(group_theory/submonoid/membership): +2 induction principles (#17160

)

src/group_theory/submonoid/membership.lean

@@ -319,13 +319,23 @@ begin
   { simpa only [map_mul, free_monoid.lift_eval_of] using Hmul _ x.prop _ ih }
 end
 
+@[elab_as_eliminator, to_additive]
+lemma induction_of_closure_eq_top_left {s : set M} {p : M → Prop} (hs : closure s = ⊤) (x : M)
+  (H1 : p 1) (Hmul : ∀ (x ∈ s) y, p y → p (x * y)) : p x :=
+closure_induction_left (by { rw [hs], exact mem_top _ }) H1 Hmul
+
 @[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)
 
+@[elab_as_eliminator, to_additive]
+lemma induction_of_closure_eq_top_right {s : set M} {p : M → Prop} (hs : closure s = ⊤) (x : M)
+  (H1 : p 1) (Hmul : ∀ x (y ∈ s), p x → p (x * y)) : p x :=
+closure_induction_right (by { rw [hs], exact mem_top _ }) H1 Hmul
+
 /-- The submonoid generated by an element. -/
 def powers (n : M) : submonoid M :=
 submonoid.copy (powers_hom M n).mrange (set.range ((^) n : ℕ → M)) $
@@ -404,8 +414,7 @@ end submonoid
   (hs : ∀ (x ∈ s) (y : N) (z : α), (x • y) • z = x • (y • z)) :
   is_scalar_tower M N α :=
 begin
-  refine ⟨λ x, submonoid.closure_induction_left
-    (show x ∈ submonoid.closure s, by { rw [htop], apply submonoid.mem_top }) _ _⟩,
+  refine ⟨λ x, submonoid.induction_of_closure_eq_top_left htop x _ _⟩,
   { intros y z, rw [one_smul, one_smul] },
   { clear x, intros x hx x' hx' y z, rw [mul_smul, mul_smul, hs x hx, hx'] }
 end
@@ -415,8 +424,7 @@ end
   (hs : ∀ (x ∈ s) (y : N) (z : α), x • y • z = y • x • z) :
   smul_comm_class M N α :=
 begin
-  refine ⟨λ x, submonoid.closure_induction_left
-    (show x ∈ submonoid.closure s, by { rw [htop], apply submonoid.mem_top }) _ _⟩,
+  refine ⟨λ x, submonoid.induction_of_closure_eq_top_left htop x _ _⟩,
   { intros y z, rw [one_smul, one_smul] },
   { clear x, intros x hx x' hx' y z, rw [mul_smul, mul_smul, hx', hs x hx] }
 end