/-
Copyright (c) 2022 Jireh Loreaux. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jireh Loreaux

! This file was ported from Lean 3 source module group_theory.subsemigroup.membership
! leanprover-community/mathlib commit 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.Subsemigroup.Basic

/-!
# Subsemigroups: membership criteria

In this file we prove various facts about membership in a subsemigroup.
The intent is to mimic `GroupTheory/Submonoid/Membership`, but currently this file is mostly a
stub and only provides rudimentary support.

* `mem_iSup_of_directed`, `coe_iSup_of_directed`, `mem_sSup_of_directed_on`,
  `coe_sSup_of_directed_on`: the supremum of a directed collection of subsemigroup is their union.

## TODO

* Define the `FreeSemigroup` generated by a set. This might require some rather substantial
  additions to low-level API. For example, developing the subtype of nonempty lists, then defining
  a product on nonempty lists, powers where the exponent is a positive natural, et cetera.
  Another option would be to define the `FreeSemigroup` as the subsemigroup (pushed to be a
  semigroup) of the `FreeMonoid` consisting of non-identity elements.

## Tags
subsemigroup
-/

variable {
ι: Sort ?u.14
ι : 
Sort _: Type ?u.2
Sort
Sort _: Type ?u.2
 _} {
M: Type ?u.5
M 
A: Type ?u.7996
A 
B: Type ?u.7999
B : 
Type _: Type (?u.11+1)
Type _}

section NonAssoc

variable [
Mul: Type ?u.8313 → Type ?u.8313
Mul 
M: Type ?u.17
M]

open Set

namespace Subsemigroup

-- TODO: this section can be generalized to `[MulMemClass B M] [CompleteLattice B]`
-- such that `complete_lattice.le` coincides with `set_like.le`
@[
to_additive: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι → AddSubsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i
to_additive]
theorem 
mem_iSup_of_directed: ∀ {S : ι → Subsemigroup M}, Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i
mem_iSup_of_directed {
S: ι → Subsemigroup M
S : 
ι: Sort ?u.29
ι → 
Subsemigroup: (M : Type ?u.46) → [inst : Mul M] → Type ?u.46
Subsemigroup 
M: Type ?u.32
M} (
hS: Directed (fun x x_1 => x ≤ x_1) S
hS : 
Directed: {α : Type ?u.57} → {ι : Sort ?u.56} → (α → α → Prop) → (ι → α) → Prop
Directed 
(· ≤ ·): Subsemigroup M → Subsemigroup M → Prop
(· ≤ ·) 
S: ι → Subsemigroup M
S) {
x: M
x : 
M: Type ?u.32
M} :
    (
x: M
x ∈ ⨆ 
i: ?m.147
i, 
S: ι → Subsemigroup M
S 
i: ?m.147
i) ↔ ∃ 
i: ?m.193
i, 
x: M
x ∈ 
S: ι → Subsemigroup M
S 
i: ?m.193
i := by
Goals accomplished! 🐙
  
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

(x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S irefine' ⟨
_: ?m.249 → ?m.250
_, fun ⟨
i: ι
i, 
hi: x ∈ S i
hi⟩ => (
SetLike.le_def: ∀ {A : Type ?u.289} {B : Type ?u.290} [i : SetLike A B] {S T : A}, S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T
SetLike.le_def.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 <| 
le_iSup: ∀ {α : Type ?u.308} {ι : Sort ?u.309} [inst : CompleteLattice α] (f : ι → α) (i : ι), f i ≤ iSup f
le_iSup 
S: ι → Subsemigroup M
S 
i: ι
i) 
hi: x ∈ S i
hi⟩
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

(x ∈ ⨆ i, S i) → ∃ i, x ∈ S i
  
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

(x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S isuffices 
x: M
x ∈ 
closure: {M : Type ?u.532} → [inst : Mul M] → Set M → Subsemigroup M
closure (⋃ 
i: ?m.553
i, (
S: ι → Subsemigroup M
S 
i: ?m.553
i : 
Set: Type ?u.556 → Type ?u.556
Set 
M: Type u_1
M)) → ∃ 
i: ?m.674
i, 
x: M
x ∈ 
S: ι → Subsemigroup M
S 
i: ?m.674
i by
    
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

(x ∈ ⨆ i, S i) → ∃ i, x ∈ S isimpa only [
closure_iUnion: ∀ {M : Type ?u.699} [inst : Mul M] {ι : Sort ?u.698} (s : ι → Set M), closure (iUnion fun i => s i) = ⨆ i, closure (s i)
closure_iUnion, 
closure_eq: ∀ {M : Type ?u.720} [inst : Mul M] (S : Subsemigroup M), closure ↑S = S
closure_eq (
S: ι → Subsemigroup M
S 
_: ι
_)] using 
this: x ∈ closure (iUnion fun i => ↑(S i)) → ∃ i, x ∈ S i
this
Goals accomplished! 🐙
  
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

(x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S irefine' fun 
hx: ?m.1015
hx => 
closure_induction: ∀ {M : Type ?u.1017} [inst : Mul M] {s : Set M} {p : M → Prop} {x : M},
  x ∈ closure s → (∀ (x : M), x ∈ s → p x) → (∀ (x y : M), p x → p y → p (x * y)) → p x
closure_induction 
hx: ?m.1015
hx (fun 
y: ?m.1077
y 
hy: ?m.1080
hy => 
mem_iUnion: ∀ {α : Type ?u.1082} {ι : Sort ?u.1083} {x : α} {s : ι → Set α}, (x ∈ iUnion fun i => s i) ↔ ∃ i, x ∈ s i
mem_iUnion.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp 
hy: ?m.1080
hy) 
_: ∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
_
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

hx: x ∈ closure (iUnion fun i => ↑(S i))

∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
  
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

(x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i·
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

hx: x ∈ closure (iUnion fun i => ↑(S i))

∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i 
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

hx: x ∈ closure (iUnion fun i => ↑(S i))

∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S irintro 
x: M
x 
y: M
y 
⟨i, hi⟩: ∃ i, x ∈ S i
⟨
i: ι
i
⟨i, hi⟩: ∃ i, x ∈ S i
, 
hi: x ∈ S i
hi
⟨i, hi⟩: ∃ i, x ∈ S i
⟩ 
⟨j, hj⟩: ∃ i, y ∈ S i
⟨
j: ι
j
⟨j, hj⟩: ∃ i, y ∈ S i
, 
hj: y ∈ S j
hj
⟨j, hj⟩: ∃ i, y ∈ S i
⟩
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x✝: M

hx: x✝ ∈ closure (iUnion fun i => ↑(S i))

x, y: M

i: ι

hi: x ∈ S i

j: ι

hj: y ∈ S j

intro.intro
∃ i, x * y ∈ S i
    
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

hx: x ∈ closure (iUnion fun i => ↑(S i))

∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S ircases 
hS: Directed (fun x x_1 => x ≤ x_1) S
hS 
i: ι
i 
j: ι
j with 
⟨k, hki, hkj⟩: ∃ z, (fun x x_1 => x ≤ x_1) (S i) (S z) ∧ (fun x x_1 => x ≤ x_1) (S j) (S z)
⟨
k: ι
k
⟨k, hki, hkj⟩: ∃ z, (fun x x_1 => x ≤ x_1) (S i) (S z) ∧ (fun x x_1 => x ≤ x_1) (S j) (S z)
, 
hki: S i ≤ S k
hki
⟨k, hki, hkj⟩: ∃ z, (fun x x_1 => x ≤ x_1) (S i) (S z) ∧ (fun x x_1 => x ≤ x_1) (S j) (S z)
, 
hkj: S j ≤ S k
hkj
⟨k, hki, hkj⟩: ∃ z, (fun x x_1 => x ≤ x_1) (S i) (S z) ∧ (fun x x_1 => x ≤ x_1) (S j) (S z)
⟩
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x✝: M

hx: x✝ ∈ closure (iUnion fun i => ↑(S i))

x, y: M

i: ι

hi: x ∈ S i

j: ι

hj: y ∈ S j

k: ι

hki: S i ≤ S k

hkj: S j ≤ S k

intro.intro.intro.intro
∃ i, x * y ∈ S i
    
ι: Sort u_2

M: Type u_1

A: Type ?u.35

B: Type ?u.38

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

hx: x ∈ closure (iUnion fun i => ↑(S i))

∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S iexact ⟨
k: ι
k, (
S: ι → Subsemigroup M
S 
k: ι
k).
mul_mem: ∀ {M : Type ?u.1230} [inst : Mul M] (S : Subsemigroup M) {x y : M}, x ∈ S → y ∈ S → x * y ∈ S
mul_mem (
hki: S i ≤ S k
hki 
hi: x ∈ S i
hi) (
hkj: S j ≤ S k
hkj 
hj: y ∈ S j
hj)⟩
Goals accomplished! 🐙
#align subsemigroup.mem_supr_of_directed 
Subsemigroup.mem_iSup_of_directed: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Mul M] {S : ι → Subsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i
Subsemigroup.mem_iSup_of_directed
#align add_subsemigroup.mem_supr_of_directed 
AddSubsemigroup.mem_iSup_of_directed: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι → AddSubsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i
AddSubsemigroup.mem_iSup_of_directed

@[
to_additive: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι → AddSubsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ↑(⨆ i, S i) = iUnion fun i => ↑(S i)
to_additive]
theorem 
coe_iSup_of_directed: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Mul M] {S : ι → Subsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ↑(⨆ i, S i) = iUnion fun i => ↑(S i)
coe_iSup_of_directed {
S: ι → Subsemigroup M
S : 
ι: Sort ?u.1440
ι → 
Subsemigroup: (M : Type ?u.1457) → [inst : Mul M] → Type ?u.1457
Subsemigroup 
M: Type ?u.1443
M} (
hS: Directed (fun x x_1 => x ≤ x_1) S
hS : 
Directed: {α : Type ?u.1468} → {ι : Sort ?u.1467} → (α → α → Prop) → (ι → α) → Prop
Directed 
(· ≤ ·): Subsemigroup M → Subsemigroup M → Prop
(· ≤ ·) 
S: ι → Subsemigroup M
S) :
    ((⨆ 
i: ?m.1557
i, 
S: ι → Subsemigroup M
S 
i: ?m.1557
i : 
Subsemigroup: (M : Type ?u.1537) → [inst : Mul M] → Type ?u.1537
Subsemigroup 
M: Type ?u.1443
M) : 
Set: Type ?u.1535 → Type ?u.1535
Set 
M: Type ?u.1443
M) = ⋃ 
i: ?m.1679
i, ↑(
S: ι → Subsemigroup M
S 
i: ?m.1679
i) :=
  
Set.ext: ∀ {α : Type ?u.1956} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b
Set.ext fun 
x: ?m.1965
x => by
Goals accomplished! 🐙 
ι: Sort u_2

M: Type u_1

A: Type ?u.1446

B: Type ?u.1449

inst✝: Mul M

S: ι → Subsemigroup M

hS: Directed (fun x x_1 => x ≤ x_1) S

x: M

x ∈ ↑(⨆ i, S i) ↔ x ∈ iUnion fun i => ↑(S i)simp [
mem_iSup_of_directed: ∀ {ι : Sort ?u.1976} {M : Type ?u.1975} [inst : Mul M] {S : ι → Subsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i
mem_iSup_of_directed 
hS: Directed (fun x x_1 => x ≤ x_1) S
hS]
Goals accomplished! 🐙
#align subsemigroup.coe_supr_of_directed 
Subsemigroup.coe_iSup_of_directed: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Mul M] {S : ι → Subsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ↑(⨆ i, S i) = iUnion fun i => ↑(S i)
Subsemigroup.coe_iSup_of_directed
#align add_subsemigroup.coe_supr_of_directed 
AddSubsemigroup.coe_iSup_of_directed: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι → AddSubsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ↑(⨆ i, S i) = iUnion fun i => ↑(S i)
AddSubsemigroup.coe_iSup_of_directed

@[
to_additive: ∀ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)},
  DirectedOn (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
to_additive]
theorem 
mem_sSup_of_directed_on: ∀ {S : Set (Subsemigroup M)}, DirectedOn (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
mem_sSup_of_directed_on {
S: Set (Subsemigroup M)
S : 
Set: Type ?u.3761 → Type ?u.3761
Set (
Subsemigroup: (M : Type ?u.3762) → [inst : Mul M] → Type ?u.3762
Subsemigroup 
M: Type ?u.3749
M)} (
hS: DirectedOn (fun x x_1 => x ≤ x_1) S
hS : 
DirectedOn: {α : Type ?u.3772} → (α → α → Prop) → Set α → Prop
DirectedOn 
(· ≤ ·): Subsemigroup M → Subsemigroup M → Prop
(· ≤ ·) 
S: Set (Subsemigroup M)
S) {
x: M
x : 
M: Type ?u.3749
M} :
    
x: M
x ∈ 
sSup: {α : Type ?u.3841} → [self : SupSet α] → Set α → α
sSup 
S: Set (Subsemigroup M)
S ↔ ∃ 
s: ?m.3900
s ∈ 
S: Set (Subsemigroup M)
S, 
x: M
x ∈ 
s: ?m.3900
s := by
Goals accomplished! 🐙
  
ι: Sort ?u.3746

M: Type u_1

A: Type ?u.3752

B: Type ?u.3755

inst✝: Mul M

S: Set (Subsemigroup M)

hS: DirectedOn (fun x x_1 => x ≤ x_1) S

x: M

x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ ssimp only [
sSup_eq_iSup': ∀ {α : Type ?u.3980} [inst : SupSet α] (s : Set α), sSup s = ⨆ a, ↑a
sSup_eq_iSup', 
mem_iSup_of_directed: ∀ {ι : Sort ?u.3994} {M : Type ?u.3993} [inst : Mul M] {S : ι → Subsemigroup M},
  Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i
mem_iSup_of_directed 
hS: DirectedOn (fun x x_1 => x ≤ x_1) S
hS.
directed_val: ∀ {α : Type ?u.3999} {r : α → α → Prop} {s : Set α}, DirectedOn r s → Directed r Subtype.val
directed_val, 
SetCoe.exists: ∀ {α : Type ?u.4070} {s : Set α} {p : ↑s → Prop}, (∃ x, p x) ↔ ∃ x h, p { val := x, property := h }
SetCoe.exists, 
Subtype.coe_mk: ∀ {α : Sort ?u.4089} {p : α → Prop} (a : α) (h : p a), ↑{ val := a, property := h } = a
Subtype.coe_mk,
    
exists_prop: ∀ {b a : Prop}, (∃ _h, b) ↔ a ∧ b
exists_prop]
Goals accomplished! 🐙
#align subsemigroup.mem_Sup_of_directed_on 
Subsemigroup.mem_sSup_of_directed_on: ∀ {M : Type u_1} [inst : Mul M] {S : Set (Subsemigroup M)},
  DirectedOn (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
Subsemigroup.mem_sSup_of_directed_on
#align add_subsemigroup.mem_Sup_of_directed_on 
AddSubsemigroup.mem_sSup_of_directed_on: ∀ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)},
  DirectedOn (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
AddSubsemigroup.mem_sSup_of_directed_on

@[
to_additive: ∀ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)},
  DirectedOn (fun x x_1 => x ≤ x_1) S → ↑(sSup S) = iUnion fun s => iUnion fun h => ↑s
to_additive]
theorem 
coe_sSup_of_directed_on: ∀ {S : Set (Subsemigroup M)}, DirectedOn (fun x x_1 => x ≤ x_1) S → ↑(sSup S) = iUnion fun s => iUnion fun h => ↑s
coe_sSup_of_directed_on {
S: Set (Subsemigroup M)
S : 
Set: Type ?u.4522 → Type ?u.4522
Set (
Subsemigroup: (M : Type ?u.4523) → [inst : Mul M] → Type ?u.4523
Subsemigroup 
M: Type ?u.4510
M)} (
hS: DirectedOn (fun x x_1 => x ≤ x_1) S
hS : 
DirectedOn: {α : Type ?u.4533} → (α → α → Prop) → Set α → Prop
DirectedOn 
(· ≤ ·): Subsemigroup M → Subsemigroup M → Prop
(· ≤ ·) 
S: Set (Subsemigroup M)
S) :
    (↑(
sSup: {α : Type ?u.4598} → [self : SupSet α] → Set α → α
sSup 
S: Set (Subsemigroup M)
S) : 
Set: Type ?u.4597 → Type ?u.4597
Set 
M: Type ?u.4510
M) = ⋃ 
s: ?m.4715
s ∈ 
S: Set (Subsemigroup M)
S, ↑
s: ?m.4715
s :=
  
Set.ext: ∀ {α : Type ?u.5035} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b
Set.ext fun 
x: ?m.5044
x => by
Goals accomplished! 🐙 
ι: Sort ?u.4507

M: Type u_1

A: Type ?u.4513

B: Type ?u.4516

inst✝: Mul M

S: Set (Subsemigroup M)

hS: DirectedOn (fun x x_1 => x ≤ x_1) S

x: M

x ∈ ↑(sSup S) ↔ x ∈ iUnion fun s => iUnion fun h => ↑ssimp [
mem_sSup_of_directed_on: ∀ {M : Type ?u.5054} [inst : Mul M] {S : Set (Subsemigroup M)},
  DirectedOn (fun x x_1 => x ≤ x_1) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
mem_sSup_of_directed_on 
hS: DirectedOn (fun x x_1 => x ≤ x_1) S
hS]
Goals accomplished! 🐙
#align subsemigroup.coe_Sup_of_directed_on 
Subsemigroup.coe_sSup_of_directed_on: ∀ {M : Type u_1} [inst : Mul M] {S : Set (Subsemigroup M)},
  DirectedOn (fun x x_1 => x ≤ x_1) S → ↑(sSup S) = iUnion fun s => iUnion fun h => ↑s
Subsemigroup.coe_sSup_of_directed_on
#align add_subsemigroup.coe_Sup_of_directed_on 
AddSubsemigroup.coe_sSup_of_directed_on: ∀ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)},
  DirectedOn (fun x x_1 => x ≤ x_1) S → ↑(sSup S) = iUnion fun s => iUnion fun h => ↑s
AddSubsemigroup.coe_sSup_of_directed_on

@[
to_additive: ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M} {x : M}, x ∈ S → x ∈ S ⊔ T
to_additive]
theorem 
mem_sup_left: ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M} {x : M}, x ∈ S → x ∈ S ⊔ T
mem_sup_left {
S: Subsemigroup M
S 
T: Subsemigroup M
T : 
Subsemigroup: (M : Type ?u.7704) → [inst : Mul M] → Type ?u.7704
Subsemigroup 
M: Type ?u.7682
M} : ∀ {
x: M
x : 
M: Type ?u.7682
M}, 
x: M
x ∈ 
S: Subsemigroup M
S → 
x: M
x ∈ 
S: Subsemigroup M
S ⊔ 
T: Subsemigroup M
T := by
Goals accomplished! 🐙
  
ι: Sort ?u.7679

M: Type u_1

A: Type ?u.7685

B: Type ?u.7688

inst✝: Mul M

S, T: Subsemigroup M

∀ {x : M}, x ∈ S → x ∈ S ⊔ Thave : 
S: Subsemigroup M
S ≤ 
S: Subsemigroup M
S ⊔ 
T: Subsemigroup M
T := 
le_sup_left: ∀ {α : Type ?u.7893} [inst : SemilatticeSup α] {a b : α}, a ≤ a ⊔ b
le_sup_left
ι: Sort ?u.7679

M: Type u_1

A: Type ?u.7685

B: Type ?u.7688

inst✝: Mul M

S, T: Subsemigroup M

this: S ≤ S ⊔ T

∀ {x : M}, x ∈ S → x ∈ S ⊔ T
  
ι: Sort ?u.7679

M: Type u_1

A: Type ?u.7685

B: Type ?u.7688

inst✝: Mul M

S, T: Subsemigroup M

∀ {x : M}, x ∈ S → x ∈ S ⊔ Ttauto
Goals accomplished! 🐙
#align subsemigroup.mem_sup_left 
Subsemigroup.mem_sup_left: ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M} {x : M}, x ∈ S → x ∈ S ⊔ T
Subsemigroup.mem_sup_left
#align add_subsemigroup.mem_sup_left 
AddSubsemigroup.mem_sup_left: ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M} {x : M}, x ∈ S → x ∈ S ⊔ T
AddSubsemigroup.mem_sup_left

@[
to_additive: ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M} {x : M}, x ∈ T → x ∈ S ⊔ T
to_additive]
theorem 
mem_sup_right: ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M} {x : M}, x ∈ T → x ∈ S ⊔ T
mem_sup_right {
S: Subsemigroup M
S 
T: Subsemigroup M
T : 
Subsemigroup: (M : Type ?u.8015) → [inst : Mul M] → Type ?u.8015
Subsemigroup 
M: Type ?u.7993
M} : ∀ {
x: M
x : 
M: Type ?u.7993
M}, 
x: M
x ∈ 
T: Subsemigroup M
T → 
x: M
x ∈ 
S: Subsemigroup M
S ⊔ 
T: Subsemigroup M
T := by
Goals accomplished! 🐙
  
ι: Sort ?u.7990

M: Type u_1

A: Type ?u.7996

B: Type ?u.7999

inst✝: Mul M

S, T: Subsemigroup M

∀ {x : M}, x ∈ T → x ∈ S ⊔ Thave : 
T: Subsemigroup M
T ≤ 
S: Subsemigroup M
S ⊔ 
T: Subsemigroup M
T := 
le_sup_right: ∀ {α : Type ?u.8204} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ b
le_sup_right
ι: Sort ?u.7990

M: Type u_1

A: Type ?u.7996

B: Type ?u.7999

inst✝: Mul M

S, T: Subsemigroup M

this: T ≤ S ⊔ T

∀ {x : M}, x ∈ T → x ∈ S ⊔ T
  
ι: Sort ?u.7990

M: Type u_1

A: Type ?u.7996

B: Type ?u.7999

inst✝: Mul M

S, T: Subsemigroup M

∀ {x : M}, x ∈ T → x ∈ S ⊔ Ttauto
Goals accomplished! 🐙
#align subsemigroup.mem_sup_right 
Subsemigroup.mem_sup_right: ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M} {x : M}, x ∈ T → x ∈ S ⊔ T
Subsemigroup.mem_sup_right
#align add_subsemigroup.mem_sup_right 
AddSubsemigroup.mem_sup_right: ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M} {x : M}, x ∈ T → x ∈ S ⊔ T
AddSubsemigroup.mem_sup_right

@[
to_additive: ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M} {x y : M}, x ∈ S → y ∈ T → x + y ∈ S ⊔ T
to_additive]
theorem 
mul_mem_sup: ∀ {S T : Subsemigroup M} {x y : M}, x ∈ S → y ∈ T → x * y ∈ S ⊔ T
mul_mem_sup {
S: Subsemigroup M
S 
T: Subsemigroup M
T : 
Subsemigroup: (M : Type ?u.8326) → [inst : Mul M] → Type ?u.8326
Subsemigroup 
M: Type ?u.8304
M} {
x: M
x 
y: M
y : 
M: Type ?u.8304
M} (
hx: x ∈ S
hx : 
x: M
x ∈ 
S: Subsemigroup M
S) (
hy: y ∈ T
hy : 
y: M
y ∈ 
T: Subsemigroup M
T) : 
x: M
x * 
y: M
y ∈ 
S: Subsemigroup M
S ⊔ 
T: Subsemigroup M
T :=
  
mul_mem: ∀ {S : Type ?u.8507} {M : Type ?u.8506} [inst : Mul M] [inst_1 : SetLike S M] [self : MulMemClass S M] {s : S}
  {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
mul_mem (
mem_sup_left: ∀ {M : Type ?u.8562} [inst : Mul M] {S T : Subsemigroup M} {x : M}, x ∈ S → x ∈ S ⊔ T
mem_sup_left 
hx: x ∈ S
hx) (
mem_sup_right: ∀ {M : Type ?u.8600} [inst : Mul M] {S T : Subsemigroup M} {x : M}, x ∈ T → x ∈ S ⊔ T
mem_sup_right 
hy: y ∈ T
hy)
#align subsemigroup.mul_mem_sup 
Subsemigroup.mul_mem_sup: ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M} {x y : M}, x ∈ S → y ∈ T → x * y ∈ S ⊔ T
Subsemigroup.mul_mem_sup
#align add_subsemigroup.add_mem_sup 
AddSubsemigroup.add_mem_sup: ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M} {x y : M}, x ∈ S → y ∈ T → x + y ∈ S ⊔ T
AddSubsemigroup.add_mem_sup

@[
to_additive: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι → AddSubsemigroup M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
to_additive]
theorem 
mem_iSup_of_mem: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Mul M] {S : ι → Subsemigroup M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
mem_iSup_of_mem {
S: ι → Subsemigroup M
S : 
ι: Sort ?u.8691
ι → 
Subsemigroup: (M : Type ?u.8708) → [inst : Mul M] → Type ?u.8708
Subsemigroup 
M: Type ?u.8694
M} (
i: ι
i : 
ι: Sort ?u.8691
ι) : ∀ {
x: M
x : 
M: Type ?u.8694
M}, 
x: M
x ∈ 
S: ι → Subsemigroup M
S 
i: ι
i → 
x: M
x ∈ 
iSup: {α : Type ?u.8783} → [inst : SupSet α] → {ι : Sort ?u.8782} → (ι → α) → α
iSup 
S: ι → Subsemigroup M
S := by
Goals accomplished! 🐙
  
ι: Sort u_2

M: Type u_1

A: Type ?u.8697

B: Type ?u.8700

inst✝: Mul M

S: ι → Subsemigroup M

i: ι

∀ {x : M}, x ∈ S i → x ∈ iSup Shave : 
S: ι → Subsemigroup M
S 
i: ι
i ≤ 
iSup: {α : Type ?u.8832} → [inst : SupSet α] → {ι : Sort ?u.8831} → (ι → α) → α
iSup 
S: ι → Subsemigroup M
S := 
le_iSup: ∀ {α : Type ?u.8895} {ι : Sort ?u.8896} [inst : CompleteLattice α] (f : ι → α) (i : ι), f i ≤ iSup f
le_iSup 
_: ?m.8898 → ?m.8897
_ 
_: ?m.8898
_
ι: Sort u_2

M: Type u_1

A: Type ?u.8697

B: Type ?u.8700

inst✝: Mul M

S: ι → Subsemigroup M

i: ι

this: S i ≤ iSup S

∀ {x : M}, x ∈ S i → x ∈ iSup S
  
ι: Sort u_2

M: Type u_1

A: Type ?u.8697

B: Type ?u.8700

inst✝: Mul M

S: ι → Subsemigroup M

i: ι

∀ {x : M}, x ∈ S i → x ∈ iSup Stauto
Goals accomplished! 🐙
#align subsemigroup.mem_supr_of_mem 
Subsemigroup.mem_iSup_of_mem: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Mul M] {S : ι → Subsemigroup M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
Subsemigroup.mem_iSup_of_mem
#align add_subsemigroup.mem_supr_of_mem 
AddSubsemigroup.mem_iSup_of_mem: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι → AddSubsemigroup M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
AddSubsemigroup.mem_iSup_of_mem

@[
to_additive: ∀ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)} {s : AddSubsemigroup M},
  s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
to_additive]
theorem 
mem_sSup_of_mem: ∀ {S : Set (Subsemigroup M)} {s : Subsemigroup M}, s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
mem_sSup_of_mem {
S: Set (Subsemigroup M)
S : 
Set: Type ?u.9014 → Type ?u.9014
Set (
Subsemigroup: (M : Type ?u.9015) → [inst : Mul M] → Type ?u.9015
Subsemigroup 
M: Type ?u.9002
M)} {
s: Subsemigroup M
s : 
Subsemigroup: (M : Type ?u.9025) → [inst : Mul M] → Type ?u.9025
Subsemigroup 
M: Type ?u.9002
M} (
hs: s ∈ S
hs : 
s: Subsemigroup M
s ∈ 
S: Set (Subsemigroup M)
S) :
    ∀ {
x: M
x : 
M: Type ?u.9002
M}, 
x: M
x ∈ 
s: Subsemigroup M
s → 
x: M
x ∈ 
sSup: {α : Type ?u.9119} → [self : SupSet α] → Set α → α
sSup 
S: Set (Subsemigroup M)
S := by
Goals accomplished! 🐙
  
ι: Sort ?u.8999

M: Type u_1

A: Type ?u.9005

B: Type ?u.9008

inst✝: Mul M

S: Set (Subsemigroup M)

s: Subsemigroup M

hs: s ∈ S

∀ {x : M}, x ∈ s → x ∈ sSup Shave : 
s: Subsemigroup M
s ≤ 
sSup: {α : Type ?u.9167} → [self : SupSet α] → Set α → α
sSup 
S: Set (Subsemigroup M)
S := 
le_sSup: ∀ {α : Type ?u.9229} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, a ∈ s → a ≤ sSup s
le_sSup 
hs: s ∈ S
hs
ι: Sort ?u.8999

M: Type u_1

A: Type ?u.9005

B: Type ?u.9008

inst✝: Mul M

S: Set (Subsemigroup M)

s: Subsemigroup M

hs: s ∈ S

this: s ≤ sSup S

∀ {x : M}, x ∈ s → x ∈ sSup S
  
ι: Sort ?u.8999

M: Type u_1

A: Type ?u.9005

B: Type ?u.9008

inst✝: Mul M

S: Set (Subsemigroup M)

s: Subsemigroup M

hs: s ∈ S

∀ {x : M}, x ∈ s → x ∈ sSup Stauto
Goals accomplished! 🐙
#align subsemigroup.mem_Sup_of_mem 
Subsemigroup.mem_sSup_of_mem: ∀ {M : Type u_1} [inst : Mul M] {S : Set (Subsemigroup M)} {s : Subsemigroup M}, s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
Subsemigroup.mem_sSup_of_mem
#align add_subsemigroup.mem_Sup_of_mem 
AddSubsemigroup.mem_sSup_of_mem: ∀ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)} {s : AddSubsemigroup M},
  s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
AddSubsemigroup.mem_sSup_of_mem

/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds all elements of `S i` for all `i`, and is preserved under multiplication,
then it holds for all elements of the supremum of `S`. -/
@[
to_additive: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] (S : ι → AddSubsemigroup M) {C : M → Prop} {x₁ : M},
  (x₁ ∈ ⨆ i, S i) → (∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂) → (∀ (x y : M), C x → C y → C (x + y)) → C x₁
to_additive (attr := elab_as_elim)
"An induction principle for elements of `⨆ i, S i`. If `C` holds 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: ∀ (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M},
  (x₁ ∈ ⨆ i, S i) → (∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂) → (∀ (x y : M), C x → C y → C (x * y)) → C x₁
iSup_induction (
S: ι → Subsemigroup M
S : 
ι: Sort ?u.9342
ι → 
Subsemigroup: (M : Type ?u.9359) → [inst : Mul M] → Type ?u.9359
Subsemigroup 
M: Type ?u.9345
M) {
C: M → Prop
C : 
M: Type ?u.9345
M → 
Prop: Type
Prop} {
x₁: M
x₁ : 
M: Type ?u.9345
M} (
hx₁: x₁ ∈ ⨆ i, S i
hx₁ : 
x₁: M
x₁ ∈ ⨆ 
i: ?m.9410
i, 
S: ι → Subsemigroup M
S 
i: ?m.9410
i)
    (
hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hp : ∀ (
i: ?m.9458
i) (
x₂: M
x₂ : 
M: Type ?u.9345
M) (
_hxS: x₂ ∈ S i
_hxS : 
x₂: M
x₂ ∈ 
S: ι → Subsemigroup M
S 
i: ?m.9458
i), 
C: M → Prop
C 
x₂: M
x₂) (
hmul: ∀ (x y : M), C x → C y → C (x * y)
hmul : ∀ 
x: ?m.9485
x 
y: ?m.9488
y, 
C: M → Prop
C 
x: ?m.9485
x → 
C: M → Prop
C 
y: ?m.9488
y → 
C: M → Prop
C (
x: ?m.9485
x * 
y: ?m.9488
y)) : 
C: M → Prop
C 
x₁: M
x₁ := by
Goals accomplished! 🐙
  
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

C x₁rw [
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

C x₁
iSup_eq_closure: ∀ {M : Type ?u.9545} [inst : Mul M] {ι : Sort ?u.9544} (p : ι → Subsemigroup M),
  (⨆ i, p i) = closure (iUnion fun i => ↑(p i))
iSup_eq_closure
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ closure (iUnion fun i => ↑(S i))

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

C x₁]
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ closure (iUnion fun i => ↑(S i))

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

C x₁ at 
hx₁: x₁ ∈ ⨆ i, S i
hx₁
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ closure (iUnion fun i => ↑(S i))

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

C x₁
  
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

C x₁refine' 
closure_induction: ∀ {M : Type ?u.9614} [inst : Mul M] {s : Set M} {p : M → Prop} {x : M},
  x ∈ closure s → (∀ (x : M), x ∈ s → p x) → (∀ (x y : M), p x → p y → p (x * y)) → p x
closure_induction 
hx₁: x₁ ∈ closure (iUnion fun i => ↑(S i))
hx₁ (fun 
x₂: ?m.9675
x₂ 
hx₂: ?m.9678
hx₂ => 
_: C x₂
_) 
hmul: ∀ (x y : M), C x → C y → C (x * y)
hmul
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ closure (iUnion fun i => ↑(S i))

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

x₂: M

hx₂: x₂ ∈ iUnion fun i => ↑(S i)

C x₂
  
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

C x₁obtain 
⟨i, hi⟩: ∃ i, x₂ ∈ ↑(S i)
⟨
i: ι
i
⟨i, hi⟩: ∃ i, x₂ ∈ ↑(S i)
, 
hi: x₂ ∈ ↑(S i)
hi
⟨i, hi⟩: ∃ i, x₂ ∈ ↑(S i)
⟩ := 
Set.mem_iUnion: ∀ {α : Type ?u.9688} {ι : Sort ?u.9689} {x : α} {s : ι → Set α}, (x ∈ iUnion fun i => s i) ↔ ∃ i, x ∈ s i
Set.mem_iUnion.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp 
hx₂: ?m.9678
hx₂
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ closure (iUnion fun i => ↑(S i))

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

x₂: M

hx₂: x₂ ∈ iUnion fun i => ↑(S i)

i: ι

hi: x₂ ∈ ↑(S i)

intro
C x₂
  
ι: Sort u_2

M: Type u_1

A: Type ?u.9348

B: Type ?u.9351

inst✝: Mul M

S: ι → Subsemigroup M

C: M → Prop

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂

hmul: ∀ (x y : M), C x → C y → C (x * y)

C x₁exact 
hp: ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hp 
_: ι
_ 
_: M
_ 
hi: x₂ ∈ ↑(S i)
hi
Goals accomplished! 🐙
#align subsemigroup.supr_induction 
Subsemigroup.iSup_induction: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Mul M] (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M},
  (x₁ ∈ ⨆ i, S i) → (∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂) → (∀ (x y : M), C x → C y → C (x * y)) → C x₁
Subsemigroup.iSup_induction
#align add_subsemigroup.supr_induction 
AddSubsemigroup.iSup_induction: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] (S : ι → AddSubsemigroup M) {C : M → Prop} {x₁ : M},
  (x₁ ∈ ⨆ i, S i) → (∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂) → (∀ (x y : M), C x → C y → C (x + y)) → C x₁
AddSubsemigroup.iSup_induction

/-- A dependent version of `Subsemigroup.iSup_induction`. -/
@[
to_additive: ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] (S : ι → AddSubsemigroup M) {C : (x : M) → (x ∈ ⨆ i, S i) → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)) →
    (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ i, S i)) →
      ∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁
to_additive (attr := elab_as_elim)
"A dependent version of `AddSubsemigroup.iSup_induction`."]
theorem 
iSup_induction': ∀ {ι : Sort u_2} {M : Type u_1} [inst : Mul M] (S : ι → Subsemigroup M) {C : (x : M) → (x ∈ ⨆ i, S i) → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)) →
    (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)) →
      ∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁
iSup_induction' (
S: ι → Subsemigroup M
S : 
ι: Sort ?u.9923
ι → 
Subsemigroup: (M : Type ?u.9940) → [inst : Mul M] → Type ?u.9940
Subsemigroup 
M: Type ?u.9926
M) {
C: (x : M) → (x ∈ ⨆ i, S i) → Prop
C : ∀ 
x: ?m.9951
x, (
x: ?m.9951
x ∈ ⨆ 
i: ?m.9990
i, 
S: ι → Subsemigroup M
S 
i: ?m.9990
i) → 
Prop: Type
Prop}
    (
hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)
hp : ∀ (
i: ?m.10043
i) (
x: ?m.10046
x) (
hxS: x ∈ S i
hxS : 
x: ?m.10046
x ∈ 
S: ι → Subsemigroup M
S 
i: ?m.10043
i), 
C: (x : M) → (x ∈ ⨆ i, S i) → Prop
C 
x: ?m.10046
x (
mem_iSup_of_mem: ∀ {ι : Sort ?u.10087} {M : Type ?u.10086} [inst : Mul M] {S : ι → Subsemigroup M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
mem_iSup_of_mem 
i: ?m.10043
i ‹_›))
    (
hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)
hmul : ∀ 
x: ?m.10132
x 
y: ?m.10135
y 
hx: ?m.10138
hx 
hy: ?m.10141
hy, 
C: (x : M) → (x ∈ ⨆ i, S i) → Prop
C 
x: ?m.10132
x 
hx: ?m.10138
hx → 
C: (x : M) → (x ∈ ⨆ i, S i) → Prop
C 
y: ?m.10135
y 
hy: ?m.10141
hy → 
C: (x : M) → (x ∈ ⨆ i, S i) → Prop
C (
x: ?m.10132
x * 
y: ?m.10135
y) (
mul_mem: ∀ {S : Type ?u.10187} {M : Type ?u.10186} [inst : Mul M] [inst_1 : SetLike S M] [self : MulMemClass S M] {s : S}
  {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
mul_mem ‹_› ‹_›)) {
x₁: M
x₁ : 
M: Type ?u.9926
M}
    (
hx₁: x₁ ∈ ⨆ i, S i
hx₁ : 
x₁: M
x₁ ∈ ⨆ 
i: ?m.10301
i, 
S: ι → Subsemigroup M
S 
i: ?m.10301
i) : 
C: (x : M) → (x ∈ ⨆ i, S i) → Prop
C 
x₁: M
x₁ 
hx₁: x₁ ∈ ⨆ i, S i
hx₁ := by
Goals accomplished! 🐙
  
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

C x₁ hx₁refine 
Exists.elim: ∀ {α : Sort ?u.10361} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → b
Exists.elim 
?_: ∃ x, ?m.10363 x
?_ fun (
hx₁': x₁ ∈ ⨆ i, S i
hx₁' : 
x₁: M
x₁ ∈ ⨆ 
i: ?m.10402
i, 
S: ι → Subsemigroup M
S 
i: ?m.10402
i) (
hc: C x₁ hx₁'
hc : 
C: (x : M) → (x ∈ ⨆ i, S i) → Prop
C 
x₁: M
x₁ 
hx₁': x₁ ∈ ⨆ i, S i
hx₁') => 
hc: C x₁ hx₁'
hc
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

∃ x, C x₁ x
  
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

C x₁ hx₁refine @
iSup_induction: ∀ {ι : Sort ?u.10461} {M : Type ?u.10460} [inst : Mul M] (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M},
  (x₁ ∈ ⨆ i, S i) → (∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂) → (∀ (x y : M), C x → C y → C (x * y)) → C x₁
iSup_induction 
_: Sort ?u.10461
_ 
_: Type ?u.10460
_ _ 
S: ι → Subsemigroup M
S (fun 
x': ?m.10473
x' => ∃ 
hx'': ?m.10478
hx'', 
C: (x : M) → (x ∈ ⨆ i, S i) → Prop
C 
x': ?m.10473
x' 
hx'': ?m.10478
hx'') 
_: ?m.10463
_ 
hx₁: x₁ ∈ ⨆ i, S i
hx₁
      (fun 
i: ?m.10501
i 
x₂: ?m.10504
x₂ 
hx₂: ?m.10507
hx₂ => 
?_: (fun x' => ∃ hx'', C x' hx'') x₂
?_) fun 
x₃: ?m.10518
x₃ 
y: ?m.10521
y => 
?_: (fun x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y)
?_
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

i: ι

x₂: M

hx₂: x₂ ∈ S i

refine_1
(fun x' => ∃ hx'', C x' hx'') x₂
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

x₃, y: M

refine_2
(fun x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y)
  
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

C x₁ hx₁·
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

i: ι

x₂: M

hx₂: x₂ ∈ S i

refine_1
(fun x' => ∃ hx'', C x' hx'') x₂ 
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

i: ι

x₂: M

hx₂: x₂ ∈ S i

refine_1
(fun x' => ∃ hx'', C x' hx'') x₂
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

x₃, y: M

refine_2
(fun x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y)exact ⟨
_: ?m.10536
_, 
hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)
hp 
_: ι
_ 
_: M
_ 
hx₂: ?m.10507
hx₂⟩
Goals accomplished! 🐙
  
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

C x₁ hx₁·
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

x₃, y: M

refine_2
(fun x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y) 
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

x₃, y: M

refine_2
(fun x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y)rintro 
⟨_, Cx⟩: ∃ hx'', C x₃ hx''
⟨
_: x₃ ∈ ⨆ i, S i
_
⟨_, Cx⟩: ∃ hx'', C x₃ hx''
, 
Cx: C x₃ w✝
Cx
⟨_, Cx⟩: ∃ hx'', C x₃ hx''
⟩ 
⟨_, Cy⟩: ∃ hx'', C y hx''
⟨
_: y ∈ ⨆ i, S i
_
⟨_, Cy⟩: ∃ hx'', C y hx''
, 
Cy: C y w✝
Cy
⟨_, Cy⟩: ∃ hx'', C y hx''
⟩
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

x₃, y: M

w✝¹: x₃ ∈ ⨆ i, S i

Cx: C x₃ w✝¹

w✝: y ∈ ⨆ i, S i

Cy: C y w✝

refine_2.intro.intro
∃ hx'', C (x₃ * y) hx''
    
ι: Sort u_2

M: Type u_1

A: Type ?u.9929

B: Type ?u.9932

inst✝: Mul M

S: ι → Subsemigroup M

C: (x : M) → (x ∈ ⨆ i, S i) → Prop

hp: ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)

hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)

x₁: M

hx₁: x₁ ∈ ⨆ i, S i

x₃, y: M

refine_2
(fun x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y)exact ⟨
_: ?m.10599
_, 
hmul: ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)
hmul 
_: M
_ 
_: M
_ 
_: ?m.10604 ∈ ⨆ i, S i
_ 
_: ?m.10605 ∈ ⨆ i, S i
_ 
Cx: C x₃ w✝¹
Cx 
Cy: C y w✝
Cy⟩
Goals accomplished! 🐙
#align subsemigroup.supr_induction' 
Subsemigroup.iSup_induction': ∀ {ι : Sort u_2} {M : Type u_1} [inst : Mul M] (S : ι → Subsemigroup M) {C : (x : M) → (x ∈ ⨆ i, S i) → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)) →
    (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i)) →
      ∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁
Subsemigroup.iSup_induction'
#align add_subsemigroup.supr_induction' 
AddSubsemigroup.iSup_induction': ∀ {ι : Sort u_2} {M : Type u_1} [inst : Add M] (S : ι → AddSubsemigroup M) {C : (x : M) → (x ∈ ⨆ i, S i) → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ i, S i)) →
    (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ i, S i)) →
      ∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁
AddSubsemigroup.iSup_induction'

end Subsemigroup

end NonAssoc