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

Proof state:
case intro.intro
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) 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

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

Result:
case intro.intro.intro.intro
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) 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

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
⊢ ∀ (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 intro.intro
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) 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

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup 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:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i

Tactic:
refine fun hx ↦ closure_induction (fun y hy ↦ mem_iUnion.mp hy) ?_ hx

Result:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
⊢ ∀ (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:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup 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:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
case intro.intro.intro.intro
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) 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

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

Result:
no goals

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup 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:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i