-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Submonoid M} (hS : Directed (· ≤ ·) S)
    {x : M} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Proof state:
case refine_2.intro.intro.intro.intro
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x✝ 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

Tactic:
exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x✝ x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i

Tactic:
rcases hS i j with ⟨k, hki, hkj⟩

Result:
case refine_2.intro.intro.intro.intro
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x✝ 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

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i

Tactic:
refine closure_induction (fun _ ↦ mem_iUnion.1) ?_ ?_

Result:
case refine_1
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ ∃ i, 1 ∈ S i

case refine_2
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ ∀ (x y : M),
    x ∈ closure (⋃ i, ↑(S i)) → y ∈ closure (⋃ i, ↑(S i)) → (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Result:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
this : x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa only [closure_iUnion, closure_eq (S _)] using this

Result:
no goals

Proof state:
case refine_1
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ ∃ i, 1 ∈ S i

Tactic:
exact hι.elim fun i ↦ ⟨i, (S i).one_mem⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
  simpa only [closure_iUnion, closure_eq (S _)] using this

Result:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i

Proof state:
case refine_2
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ ∀ (x y : M),
    x ∈ closure (⋃ i, ↑(S i)) → y ∈ closure (⋃ i, ↑(S i)) → (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i

Tactic:
rintro x y - - ⟨i, hi⟩ ⟨j, hj⟩

Result:
case refine_2.intro.intro
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x✝ x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i