chore(GroupTheory): rename induction arguments for `Sub{semigroup,mon…

…oid,group}` (#11461)

The additive version are still incorrectly named, but these can easily be tracked down later (#11462) by searching for `to_additive (attr := elab_as_elim)`.

Mathlib/Algebra/Order/Ring/Star.lean

@@ -36,12 +36,12 @@ private lemma mul_le_mul_of_nonneg_left {R : Type*} [CommSemiring R] [PartialOrd
     [StarOrderedRing R] {a b c : R} (hab : a ≤ b) (hc : 0 ≤ c) : c * a ≤ c * b := by
   rw [StarOrderedRing.nonneg_iff] at hc
   induction hc using AddSubmonoid.closure_induction' with
-  | Hs _ h =>
+  | mem _ h =>
     obtain ⟨x, rfl⟩ := h
     simp_rw [mul_assoc, mul_comm x, ← mul_assoc]
     exact conjugate_le_conjugate hab x
-  | H1 => simp
-  | Hmul x hx y hy =>
+  | one => simp
+  | mul x hx y hy =>
     simp only [← nonneg_iff, add_mul] at hx hy ⊢
     apply add_le_add <;> aesop
 

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

@@ -257,13 +257,13 @@ lemma nonneg_iff_isSelfAdjoint_and_spectrumRestricts {a : A} :
   refine ⟨fun ha ↦ ?_, ?_⟩
   · rw [StarOrderedRing.nonneg_iff] at ha
     induction ha using AddSubmonoid.closure_induction' with
-    | Hs x hx =>
+    | mem x hx =>
       obtain ⟨b, rfl⟩ := hx
       exact ⟨IsSelfAdjoint.star_mul_self b, spectrum_star_mul_self_nonneg⟩
-    | H1 =>
+    | one =>
       nontriviality A
       simp
-    | Hmul x _ y _ hx hy =>
+    | mul x _ y _ hx hy =>
       rw [← SpectrumRestricts.nnreal_iff] at hx hy ⊢
       exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩
   · rintro ⟨ha₁, ha₂⟩

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -1118,22 +1118,22 @@ of `k`. -/
       "An induction principle for additive closure membership. If `p`
       holds for `0` and all elements of `k`, and is preserved under addition and inverses, then `p`
       holds for all elements of the additive closure of `k`."]
-theorem closure_induction {p : G → Prop} {x} (h : x ∈ closure k) (Hk : ∀ x ∈ k, p x) (H1 : p 1)
-    (Hmul : ∀ x y, p x → p y → p (x * y)) (Hinv : ∀ x, p x → p x⁻¹) : p x :=
-  (@closure_le _ _ ⟨⟨⟨setOf p, fun {x y} ↦ Hmul x y⟩, H1⟩, fun {x} ↦ Hinv x⟩ k).2 Hk h
+theorem closure_induction {p : G → Prop} {x} (h : x ∈ closure k) (mem : ∀ x ∈ k, p x) (one : p 1)
+    (mul : ∀ x y, p x → p y → p (x * y)) (inv : ∀ x, p x → p x⁻¹) : p x :=
+  (@closure_le _ _ ⟨⟨⟨setOf p, fun {x y} ↦ mul x y⟩, one⟩, fun {x} ↦ inv x⟩ k).2 mem h
 #align subgroup.closure_induction Subgroup.closure_induction
 #align add_subgroup.closure_induction AddSubgroup.closure_induction
 
 /-- A dependent version of `Subgroup.closure_induction`.  -/
 @[to_additive (attr := elab_as_elim) "A dependent version of `AddSubgroup.closure_induction`. "]
 theorem closure_induction' {p : ∀ x, x ∈ closure k → Prop}
-    (Hs : ∀ (x) (h : x ∈ k), p x (subset_closure h)) (H1 : p 1 (one_mem _))
-    (Hmul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
-    (Hinv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx)) {x} (hx : x ∈ closure k) : p x hx := by
+    (mem : ∀ (x) (h : x ∈ k), p x (subset_closure h)) (one : p 1 (one_mem _))
+    (mul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
+    (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx)) {x} (hx : x ∈ closure k) : p x hx := by
   refine' Exists.elim _ fun (hx : x ∈ closure k) (hc : p x hx) => hc
   exact
-    closure_induction hx (fun x hx => ⟨_, Hs x hx⟩) ⟨_, H1⟩
-      (fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ => ⟨_, Hmul _ _ _ _ hx hy⟩) fun x ⟨hx', hx⟩ => ⟨_, Hinv _ _ hx⟩
+    closure_induction hx (fun x hx => ⟨_, mem x hx⟩) ⟨_, one⟩
+      (fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ => ⟨_, mul _ _ _ _ hx hy⟩) fun x ⟨hx', hx⟩ => ⟨_, inv _ _ hx⟩
 #align subgroup.closure_induction' Subgroup.closure_induction'
 #align add_subgroup.closure_induction' AddSubgroup.closure_induction'
 

Mathlib/GroupTheory/Subgroup/Pointwise.lean

@@ -134,13 +134,13 @@ the closure of `k`. -/
   elements of `k` and their negation, and is preserved under addition, then `p` holds for all
   elements of the additive closure of `k`."]
 theorem closure_induction'' {p : (g : G) → g ∈ closure s → Prop}
-    (Hk : ∀ x (hx : x ∈ s), p x (subset_closure hx))
-    (Hk_inv : ∀ x (hx : x ∈ s), p x⁻¹ (inv_mem (subset_closure hx)))
-    (H1 : p 1 (one_mem _))
-    (Hmul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
+    (mem : ∀ x (hx : x ∈ s), p x (subset_closure hx))
+    (inv_mem : ∀ x (hx : x ∈ s), p x⁻¹ (inv_mem (subset_closure hx)))
+    (one : p 1 (one_mem _))
+    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
     {x} (h : x ∈ closure s) : p x h :=
-  closure_induction_left H1 (fun x hx y _ hy => Hmul x y _ _ (Hk x hx) hy)
-    (fun x hx y _ => Hmul x⁻¹ y _ _ <| Hk_inv x hx) h
+  closure_induction_left one (fun x hx y _ hy => mul x y _ _ (mem x hx) hy)
+    (fun x hx y _ => mul x⁻¹ y _ _ <| inv_mem x hx) h
 #align subgroup.closure_induction'' Subgroup.closure_induction''
 #align add_subgroup.closure_induction'' AddSubgroup.closure_induction''
 
@@ -151,17 +151,17 @@ then it holds for all elements of the supremum of `S`. -/
 If `C` holds for `0` and all elements of `S i` for all `i`, and is preserved under addition,
 then it holds for all elements of the supremum of `S`. "]
 theorem iSup_induction {ι : Sort*} (S : ι → Subgroup G) {C : G → Prop} {x : G} (hx : x ∈ ⨆ i, S i)
-    (hp : ∀ (i), ∀ x ∈ S i, C x) (h1 : C 1) (hmul : ∀ x y, C x → C y → C (x * y)) : C x := by
+    (mem : ∀ (i), ∀ x ∈ S i, C x) (one : C 1) (mul : ∀ x y, C x → C y → C (x * y)) : C x := by
   rw [iSup_eq_closure] at hx
   induction hx using closure_induction'' with
-  | H1 => exact h1
-  | Hk x hx =>
+  | one => exact one
+  | mem x hx =>
     obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
-    exact hp _ _ hi
-  | Hk_inv x hx =>
+    exact mem _ _ hi
+  | inv_mem x hx =>
     obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
-    exact hp _ _ (inv_mem hi)
-  | Hmul x y _ _ ihx ihy => exact hmul x y ihx ihy
+    exact mem _ _ (inv_mem hi)
+  | mul x y _ _ ihx ihy => exact mul x y ihx ihy
 #align subgroup.supr_induction Subgroup.iSup_induction
 #align add_subgroup.supr_induction AddSubgroup.iSup_induction
 
@@ -210,13 +210,13 @@ theorem mul_normal (H N : Subgroup G) [hN : N.Normal] : (↑(H ⊔ N) : Set G) =
   rw [sup_eq_closure_mul]
   refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
   induction hx using closure_induction'' with
-  | H1 => exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩
-  | Hk _ hx => exact hx
-  | Hk_inv x hx =>
+  | one => exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩
+  | mem _ hx => exact hx
+  | inv_mem x hx =>
     obtain ⟨x, hx, y, hy, rfl⟩ := hx
     simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
       using mul_mem_mul (inv_mem hx) (hN.conj_mem _ (inv_mem hy) x)
-  | Hmul x' x' _ _ hx hx' =>
+  | mul x' x' _ _ hx hx' =>
     obtain ⟨x, hx, y, hy, rfl⟩ := hx
     obtain ⟨x', hx', y', hy', rfl⟩ := hx'
     refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩

Mathlib/GroupTheory/Submonoid/Basic.lean

@@ -441,22 +441,22 @@ is preserved under multiplication, then `p` holds for all elements of the closur
       "An induction principle for additive closure membership. If `p` holds for `0` and all
       elements of `s`, and is preserved under addition, then `p` holds for all elements of the
       additive closure of `s`."]
-theorem closure_induction {p : M → Prop} {x} (h : x ∈ closure s) (Hs : ∀ x ∈ s, p x) (H1 : p 1)
-    (Hmul : ∀ x y, p x → p y → p (x * y)) : p x :=
-  (@closure_le _ _ _ ⟨⟨p, Hmul _ _⟩, H1⟩).2 Hs h
+theorem closure_induction {p : M → Prop} {x} (h : x ∈ closure s) (mem : ∀ x ∈ s, p x) (one : p 1)
+    (mul : ∀ x y, p x → p y → p (x * y)) : p x :=
+  (@closure_le _ _ _ ⟨⟨p, mul _ _⟩, one⟩).2 mem h
 #align submonoid.closure_induction Submonoid.closure_induction
 #align add_submonoid.closure_induction AddSubmonoid.closure_induction
 
 /-- A dependent version of `Submonoid.closure_induction`.  -/
 @[to_additive (attr := elab_as_elim) "A dependent version of `AddSubmonoid.closure_induction`. "]
 theorem closure_induction' (s : Set M) {p : ∀ x, x ∈ closure s → Prop}
-    (Hs : ∀ (x) (h : x ∈ s), p x (subset_closure h)) (H1 : p 1 (one_mem _))
-    (Hmul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) :
+    (mem : ∀ (x) (h : x ∈ s), p x (subset_closure h)) (one : p 1 (one_mem _))
+    (mul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) :
     p x hx := by
   refine' Exists.elim _ fun (hx : x ∈ closure s) (hc : p x hx) => hc
   exact
-    closure_induction hx (fun x hx => ⟨_, Hs x hx⟩) ⟨_, H1⟩ fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ =>
-      ⟨_, Hmul _ _ _ _ hx hy⟩
+    closure_induction hx (fun x hx => ⟨_, mem x hx⟩) ⟨_, one⟩ fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ =>
+      ⟨_, mul _ _ _ _ hx hy⟩
 #align submonoid.closure_induction' Submonoid.closure_induction'
 #align add_submonoid.closure_induction' AddSubmonoid.closure_induction'
 
@@ -481,9 +481,10 @@ and verify that `p x` and `p y` imply `p (x * y)`. -/
       "If `s` is a dense set in an additive monoid `M`, `AddSubmonoid.closure s = ⊤`, then in
       order to prove that some predicate `p` holds for all `x : M` it suffices to verify `p x` for
       `x ∈ s`, verify `p 0`, and verify that `p x` and `p y` imply `p (x + y)`."]
-theorem dense_induction {p : M → Prop} (x : M) {s : Set M} (hs : closure s = ⊤) (Hs : ∀ x ∈ s, p x)
-    (H1 : p 1) (Hmul : ∀ x y, p x → p y → p (x * y)) : p x := by
-  have : ∀ x ∈ closure s, p x := fun x hx => closure_induction hx Hs H1 Hmul
+theorem dense_induction {p : M → Prop} (x : M) {s : Set M} (hs : closure s = ⊤)
+    (mem : ∀ x ∈ s, p x)
+    (one : p 1) (mul : ∀ x y, p x → p y → p (x * y)) : p x := by
+  have : ∀ x ∈ closure s, p x := fun x hx => closure_induction hx mem one mul
   simpa [hs] using this x
 #align submonoid.dense_induction Submonoid.dense_induction
 #align add_submonoid.dense_induction AddSubmonoid.dense_induction

Mathlib/GroupTheory/Submonoid/Membership.lean

@@ -275,26 +275,26 @@ then it holds for all elements of the supremum of `S`. -/
       If `C` holds for `0` and all elements of `S i` for all `i`, and is preserved under addition,
       then it holds for all elements of the supremum of `S`. "]
 theorem iSup_induction {ι : Sort*} (S : ι → Submonoid M) {C : M → Prop} {x : M} (hx : x ∈ ⨆ i, S i)
-    (hp : ∀ (i), ∀ x ∈ S i, C x) (h1 : C 1) (hmul : ∀ x y, C x → C y → C (x * y)) : C x := by
+    (mem : ∀ (i), ∀ x ∈ S i, C x) (one : C 1) (mul : ∀ x y, C x → C y → C (x * y)) : C x := by
   rw [iSup_eq_closure] at hx
-  refine closure_induction hx (fun x hx => ?_) h1 hmul
+  refine closure_induction hx (fun x hx => ?_) one mul
   obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
-  exact hp _ _ hi
+  exact mem _ _ hi
 #align submonoid.supr_induction Submonoid.iSup_induction
 #align add_submonoid.supr_induction AddSubmonoid.iSup_induction
 
 /-- A dependent version of `Submonoid.iSup_induction`. -/
 @[to_additive (attr := elab_as_elim) "A dependent version of `AddSubmonoid.iSup_induction`. "]
 theorem iSup_induction' {ι : Sort*} (S : ι → Submonoid M) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
-    (hp : ∀ (i), ∀ (x) (hxS : x ∈ S i), C x (mem_iSup_of_mem i hxS)) (h1 : C 1 (one_mem _))
-    (hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x : M}
+    (mem : ∀ (i), ∀ (x) (hxS : x ∈ S i), C x (mem_iSup_of_mem i hxS)) (one : C 1 (one_mem _))
+    (mul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x : M}
     (hx : x ∈ ⨆ i, S i) : C x hx := by
   refine' Exists.elim (_ : ∃ Hx, C x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : C x hx) => hc
   refine' @iSup_induction _ _ ι S (fun m => ∃ hm, C m hm) _ hx (fun i x hx => _) _ fun x y => _
-  · exact ⟨_, hp _ _ hx⟩
-  · exact ⟨_, h1⟩
+  · exact ⟨_, mem _ _ hx⟩
+  · exact ⟨_, one⟩
   · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
-    exact ⟨_, hmul _ _ _ _ Cx Cy⟩
+    exact ⟨_, mul _ _ _ _ Cx Cy⟩
 #align submonoid.supr_induction' Submonoid.iSup_induction'
 #align add_submonoid.supr_induction' AddSubmonoid.iSup_induction'
 
@@ -430,11 +430,11 @@ theorem closure_induction_left {s : Set M} {p : (m : M) → m ∈ closure s →
 
 @[to_additive (attr := elab_as_elim)]
 theorem 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 := by
+    (one : p 1) (mul : ∀ x ∈ s, ∀ (y), p y → p (x * y)) : p x := by
   have : x ∈ closure s := by simp [hs]
   induction this using closure_induction_left with
-  | one => exact H1
-  | mul_left x hx y _ ih => exact Hmul x hx y ih
+  | one => exact one
+  | mul_left x hx y _ ih => exact mul x hx y ih
 #align submonoid.induction_of_closure_eq_top_left Submonoid.induction_of_closure_eq_top_left
 #align add_submonoid.induction_of_closure_eq_top_left AddSubmonoid.induction_of_closure_eq_top_left
 

Mathlib/GroupTheory/Subsemigroup/Basic.lean

@@ -353,22 +353,22 @@ is preserved under multiplication, then `p` holds for all elements of the closur
 @[to_additive (attr := elab_as_elim) "An induction principle for additive closure membership. If `p`
   holds for all elements of `s`, and is preserved under addition, then `p` holds for all
   elements of the additive closure of `s`."]
-theorem closure_induction {p : M → Prop} {x} (h : x ∈ closure s) (Hs : ∀ x ∈ s, p x)
-    (Hmul : ∀ x y, p x → p y → p (x * y)) : p x :=
-  (@closure_le _ _ _ ⟨p, Hmul _ _⟩).2 Hs h
+theorem closure_induction {p : M → Prop} {x} (h : x ∈ closure s) (mem : ∀ x ∈ s, p x)
+    (mul : ∀ x y, p x → p y → p (x * y)) : p x :=
+  (@closure_le _ _ _ ⟨p, mul _ _⟩).2 mem h
 #align subsemigroup.closure_induction Subsemigroup.closure_induction
 #align add_subsemigroup.closure_induction AddSubsemigroup.closure_induction
 
 /-- A dependent version of `Subsemigroup.closure_induction`.  -/
 @[to_additive (attr := elab_as_elim) "A dependent version of `AddSubsemigroup.closure_induction`. "]
 theorem closure_induction' (s : Set M) {p : ∀ x, x ∈ closure s → Prop}
-    (Hs : ∀ (x) (h : x ∈ s), p x (subset_closure h))
-    (Hmul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) :
+    (mem : ∀ (x) (h : x ∈ s), p x (subset_closure h))
+    (mul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) :
     p x hx := by
   refine' Exists.elim _ fun (hx : x ∈ closure s) (hc : p x hx) => hc
   exact
-    closure_induction hx (fun x hx => ⟨_, Hs x hx⟩) fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ =>
-      ⟨_, Hmul _ _ _ _ hx hy⟩
+    closure_induction hx (fun x hx => ⟨_, mem x hx⟩) fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ =>
+      ⟨_, mul _ _ _ _ hx hy⟩
 #align subsemigroup.closure_induction' Subsemigroup.closure_induction'
 #align add_subsemigroup.closure_induction' AddSubsemigroup.closure_induction'
 
@@ -391,9 +391,10 @@ and verify that `p x` and `p y` imply `p (x * y)`. -/
   `AddSubsemigroup.closure s = ⊤`, then in order to prove that some predicate `p` holds
   for all `x : M` it suffices to verify `p x` for `x ∈ s`, and verify that `p x` and `p y` imply
   `p (x + y)`."]
-theorem dense_induction {p : M → Prop} (x : M) {s : Set M} (hs : closure s = ⊤) (Hs : ∀ x ∈ s, p x)
-    (Hmul : ∀ x y, p x → p y → p (x * y)) : p x := by
-  have : ∀ x ∈ closure s, p x := fun x hx => closure_induction hx Hs Hmul
+theorem dense_induction {p : M → Prop} (x : M) {s : Set M} (hs : closure s = ⊤)
+    (mem : ∀ x ∈ s, p x)
+    (mul : ∀ x y, p x → p y → p (x * y)) : p x := by
+  have : ∀ x ∈ closure s, p x := fun x hx => closure_induction hx mem mul
   simpa [hs] using this x
 #align subsemigroup.dense_induction Subsemigroup.dense_induction
 #align add_subsemigroup.dense_induction AddSubsemigroup.dense_induction

Mathlib/GroupTheory/Subsemigroup/Membership.lean

@@ -119,27 +119,27 @@ then it holds for all elements of the supremum of `S`. -/
 elements of `S i` for all `i`, and is preserved under addition, then it holds for all elements of
 the supremum of `S`."]
 theorem iSup_induction (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i)
-    (hp : ∀ i, ∀ x₂ ∈ S i, C x₂) (hmul : ∀ x y, C x → C y → C (x * y)) : C x₁ := by
+    (mem : ∀ i, ∀ x₂ ∈ S i, C x₂) (mul : ∀ x y, C x → C y → C (x * y)) : C x₁ := by
   rw [iSup_eq_closure] at hx₁
-  refine' closure_induction hx₁ (fun x₂ hx₂ => _) hmul
+  refine' closure_induction hx₁ (fun x₂ hx₂ => _) mul
   obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂
-  exact hp _ _ hi
+  exact mem _ _ hi
 #align subsemigroup.supr_induction Subsemigroup.iSup_induction
 #align add_subsemigroup.supr_induction AddSubsemigroup.iSup_induction
 
 /-- A dependent version of `Subsemigroup.iSup_induction`. -/
 @[to_additive (attr := elab_as_elim)
 "A dependent version of `AddSubsemigroup.iSup_induction`."]
 theorem iSup_induction' (S : ι → Subsemigroup M) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
-    (hp : ∀ (i) (x) (hxS : x ∈ S i), C x (mem_iSup_of_mem i ‹_›))
-    (hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x₁ : M}
+    (mem : ∀ (i) (x) (hxS : x ∈ S i), C x (mem_iSup_of_mem i ‹_›))
+    (mul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x₁ : M}
     (hx₁ : x₁ ∈ ⨆ i, S i) : C x₁ hx₁ := by
   refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
   refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
       (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
-  · exact ⟨_, hp _ _ hx₂⟩
+  · exact ⟨_, mem _ _ hx₂⟩
   · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
-    exact ⟨_, hmul _ _ _ _ Cx Cy⟩
+    exact ⟨_, mul _ _ _ _ Cx Cy⟩
 #align subsemigroup.supr_induction' Subsemigroup.iSup_induction'
 #align add_subsemigroup.supr_induction' AddSubsemigroup.iSup_induction'