feat(group_theory/sub{monoid,group}): Add closure_induction' for su…

…btypes (#4984)

src/group_theory/subgroup.lean

@@ -493,6 +493,36 @@ lemma closure_induction {p : G → Prop} {x} (h : x ∈ closure k)
 
 attribute [elab_as_eliminator] subgroup.closure_induction add_subgroup.closure_induction
 
+/-- An induction principle on elements of the subtype `subgroup.closure`.
+If `p` holds for `1` and all elements of `k`, and is preserved under multiplication and inverse,
+then `p` holds for all elements `x : closure k`.
+
+The difference with `subgroup.closure_induction` is that this acts on the subtype.
+-/
+@[to_additive "An induction principle on elements of the subtype `add_subgroup.closure`.
+If `p` holds for `0` and all elements of `k`, and is preserved under addition and negation,
+then `p` holds for all elements `x : closure k`.
+
+The difference with `add_subgroup.closure_induction` is that this acts on the subtype."]
+lemma closure_induction' (k : set G) {p : closure k → Prop}
+  (Hk : ∀ x (h : x ∈ k), p ⟨x, subset_closure h⟩)
+  (H1 : p 1)
+  (Hmul : ∀ x y, p x → p y → p (x * y))
+  (Hinv : ∀ x, p x → p x⁻¹)
+  (x : closure k) :
+  p x :=
+subtype.rec_on x $ λ x hx, begin
+  refine exists.elim _ (λ (hx : x ∈ closure k) (hc : p ⟨x, hx⟩), hc),
+  exact closure_induction hx
+    (λ x hx, ⟨subset_closure hx, Hk x hx⟩)
+    ⟨one_mem _, H1⟩
+    (λ x y hx hy, exists.elim hx $ λ hx' hx, exists.elim hy $ λ hy' hy,
+      ⟨mul_mem _ hx' hy', Hmul _ _ hx hy⟩)
+    (λ x hx, exists.elim hx $ λ hx' hx, ⟨inv_mem _ hx', Hinv _ hx⟩),
+end
+
+attribute [elab_as_eliminator] subgroup.closure_induction' add_subgroup.closure_induction'
+
 variable (G)
 
 /-- `closure` forms a Galois insertion with the coercion to set. -/

src/group_theory/submonoid/operations.lean

@@ -338,6 +338,34 @@ def subtype : S →* M := ⟨coe, rfl, λ _ _, rfl⟩
 
 @[simp, to_additive] theorem coe_subtype : ⇑S.subtype = coe := rfl
 
+/-- An induction principle on elements of the type `submonoid.closure s`.
+If `p` holds for `1` and all elements of `s`, and is preserved under multiplication, then `p`
+holds for all elements of the closure of `s`.
+
+The difference with `submonoid.closure_induction` is that this acts on the subtype.
+-/
+@[to_additive "An induction principle on elements of the type `add_submonoid.closure s`.
+If `p` holds for `0` and all elements of `s`, and is preserved under addition, then `p`
+holds for all elements of the closure of `s`.
+
+The difference with `add_submonoid.closure_induction` is that this acts on the subtype."]
+lemma closure_induction' (s : set M) {p : closure s → Prop}
+  (Hs : ∀ x (h : x ∈ s), p ⟨x, subset_closure h⟩)
+  (H1 : p 1)
+  (Hmul : ∀ x y, p x → p y → p (x * y))
+  (x : closure s) :
+  p x :=
+subtype.rec_on x $ λ x hx, begin
+  refine exists.elim _ (λ (hx : x ∈ closure s) (hc : p ⟨x, hx⟩), hc),
+  exact closure_induction hx
+    (λ x hx, ⟨subset_closure hx, Hs x hx⟩)
+    ⟨one_mem _, H1⟩
+    (λ x y hx hy, exists.elim hx $ λ hx' hx, exists.elim hy $ λ hy' hy,
+      ⟨mul_mem _ hx' hy', Hmul _ _ hx hy⟩),
+end
+
+attribute [elab_as_eliminator] submonoid.closure_induction' add_submonoid.closure_induction'
+
 /-- Given `submonoid`s `s`, `t` of monoids `M`, `N` respectively, `s × t` as a submonoid
 of `M × N`. -/
 @[to_additive prod "Given `add_submonoid`s `s`, `t` of `add_monoid`s `A`, `B` respectively, `s × t`