M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ (x ∈ ⨆ (i : ι), S i) ↔ ∃ i, x ∈ S i
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
  simpa only [closure_iUnion, closure_eq (S _)] using this
case refine'_1
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∃ i, 1 ∈ S i

case refine'_2
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
refine' fun hx => closure_induction hx (fun _ => mem_iUnion.1) _ _
no goals
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
this : x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
simpa only [closure_iUnion, closure_eq (S _)] using this
no goals
case refine'_1
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∃ i, 1 ∈ S i
exact hι.elim fun i => ⟨i, (S i).one_mem⟩
case refine'_2.intro.intro
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
case refine'_2
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
rintro x y ⟨i, hi⟩ ⟨j, hj⟩
case refine'_2.intro.intro.intro.intro
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (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
⊢ ∃ i, x * y ∈ S i
case refine'_2.intro.intro
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
rcases hS i j with ⟨k, hki, hkj⟩
no goals
case refine'_2.intro.intro.intro.intro
M : Type u_2
A : Type ?u.32885
B : Type ?u.32888
inst✝ : MulOneClass M
ι : Sort u_1
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (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
⊢ ∃ i, x * y ∈ S i
exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩