-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {K : ι → Subgroup G} (hK : Directed (· ≤ ·) K)
    {x : G} : x ∈ (iSup K : Subgroup G) ↔ ∃ i, x ∈ K i

Proof state:
case refine_3.intro
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
hx : x ∈ closure (⋃ i, ↑(K i))
x✝ : G
hx✝ : x✝ ∈ closure (⋃ i, ↑(K i))
i : ι
hi : x✝ ∈ K i
⊢ ∃ i, x✝⁻¹ ∈ K i

Tactic:
exact ⟨i, inv_mem hi⟩

Result:
no goals

Proof state:
case refine_3
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
hx : x ∈ closure (⋃ i, ↑(K i))
⊢ ∀ x ∈ closure (⋃ i, ↑(K i)), (∃ i, x ∈ K i) → ∃ i, x⁻¹ ∈ K i

Tactic:
rintro _ _ ⟨i, hi⟩

Result:
case refine_3.intro
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
hx : x ∈ closure (⋃ i, ↑(K i))
x✝ : G
hx✝ : x✝ ∈ closure (⋃ i, ↑(K i))
i : ι
hi : x✝ ∈ K i
⊢ ∃ i, x✝⁻¹ ∈ K i

Proof state:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
⊢ x ∈ iSup K → ∃ i, x ∈ K i

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

Result:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
⊢ x ∈ closure (⋃ i, ↑(K i)) → ∃ i, x ∈ K i

Proof state:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
this : x ∈ closure (⋃ i, ↑(K i)) → ∃ i, x ∈ K i
⊢ x ∈ iSup K → ∃ i, x ∈ K i

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

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
⊢ x ∈ iSup K ↔ ∃ i, x ∈ K i

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

Result:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
⊢ x ∈ iSup K → ∃ i, x ∈ K i

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
hx : x ∈ closure (⋃ i, ↑(K i))
⊢ ∀ (x y : G),
    x ∈ closure (⋃ i, ↑(K i)) → y ∈ closure (⋃ i, ↑(K i)) → (∃ i, x ∈ K i) → (∃ i, y ∈ K i) → ∃ i, x * y ∈ K i

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

Result:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x✝ : G
hx : x✝ ∈ closure (⋃ i, ↑(K i))
x y : G
hx✝ : x ∈ closure (⋃ i, ↑(K i))
hy✝ : y ∈ closure (⋃ i, ↑(K i))
i : ι
hi : x ∈ K i
j : ι
hj : y ∈ K j
⊢ ∃ i, x * y ∈ K i

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
hx : x ∈ closure (⋃ i, ↑(K i))
⊢ ∃ i, 1 ∈ K i

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

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
⊢ x ∈ closure (⋃ i, ↑(K i)) → ∃ i, x ∈ K i

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

Result:
case refine_1
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
hx : x ∈ closure (⋃ i, ↑(K i))
⊢ ∃ i, 1 ∈ K i

case refine_2
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
hx : x ∈ closure (⋃ i, ↑(K i))
⊢ ∀ (x y : G),
    x ∈ closure (⋃ i, ↑(K i)) → y ∈ closure (⋃ i, ↑(K i)) → (∃ i, x ∈ K i) → (∃ i, y ∈ K i) → ∃ i, x * y ∈ K i

case refine_3
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x : G
hx : x ∈ closure (⋃ i, ↑(K i))
⊢ ∀ x ∈ closure (⋃ i, ↑(K i)), (∃ i, x ∈ K i) → ∃ i, x⁻¹ ∈ K i

Proof state:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x✝ : G
hx : x✝ ∈ closure (⋃ i, ↑(K i))
x y : G
hx✝ : x ∈ closure (⋃ i, ↑(K i))
hy✝ : y ∈ closure (⋃ i, ↑(K i))
i : ι
hi : x ∈ K i
j : ι
hj : y ∈ K j
⊢ ∃ i, x * y ∈ K i

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

Result:
case refine_2.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x✝ : G
hx : x✝ ∈ closure (⋃ i, ↑(K i))
x y : G
hx✝ : x ∈ closure (⋃ i, ↑(K i))
hy✝ : y ∈ closure (⋃ i, ↑(K i))
i : ι
hi : x ∈ K i
j : ι
hj : y ∈ K j
k : ι
hki : K i ≤ K k
hkj : K j ≤ K k
⊢ ∃ i, x * y ∈ K i

Proof state:
case refine_2.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 => x1 ≤ x2) K
x✝ : G
hx : x✝ ∈ closure (⋃ i, ↑(K i))
x y : G
hx✝ : x ∈ closure (⋃ i, ↑(K i))
hy✝ : y ∈ closure (⋃ i, ↑(K i))
i : ι
hi : x ∈ K i
j : ι
hj : y ∈ K j
k : ι
hki : K i ≤ K k
hkj : K j ≤ K k
⊢ ∃ i, x * y ∈ K i

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

Result:
no goals