G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
⊢ x ∈ iSup K → ∃ i, x ∈ K i
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
⊢ x ∈ iSup K ↔ ∃ i, x ∈ K i
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup K i) hi⟩
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
⊢ x ∈ closure (⋃ (i : ι), ↑(K i)) → ∃ i, x ∈ K i
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
⊢ x ∈ iSup K → ∃ i, x ∈ K i
suffices x ∈ closure (⋃ i, (K i : Set G)) → ∃ i, x ∈ K i by
  simpa only [closure_iUnion, closure_eq (K _)] using this
case refine'_1
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(K i))
⊢ ∃ i, 1 ∈ K i

case refine'_2
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(K i))
⊢ ∀ (x y : G), (∃ i, x ∈ K i) → (∃ i, y ∈ K i) → ∃ i, x * y ∈ K i

case refine'_3
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(K i))
⊢ ∀ (x : G), (∃ i, x ∈ K i) → ∃ i, x⁻¹ ∈ K i
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
⊢ x ∈ closure (⋃ (i : ι), ↑(K i)) → ∃ i, x ∈ K i
refine' fun hx => closure_induction hx (fun _ => mem_iUnion.1) _ _ _
case refine'_3.intro
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(K i))
x✝ : G
i : ι
hi : x✝ ∈ K i
⊢ ∃ i, x✝⁻¹ ∈ K i
case refine'_3
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(K i))
⊢ ∀ (x : G), (∃ i, x ∈ K i) → ∃ i, x⁻¹ ∈ K i
rintro _ ⟨i, hi⟩
no goals
case refine'_3.intro
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(K i))
x✝ : G
i : ι
hi : x✝ ∈ K i
⊢ ∃ i, x✝⁻¹ ∈ K i
exact ⟨i, inv_mem hi⟩
no goals
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
this : x ∈ closure (⋃ (i : ι), ↑(K i)) → ∃ i, x ∈ K i
⊢ x ∈ iSup K → ∃ i, x ∈ K i
simpa only [closure_iUnion, closure_eq (K _)] using this
no goals
case refine'_1
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(K i))
⊢ ∃ i, 1 ∈ K i
exact hι.elim fun i => ⟨i, (K i).one_mem⟩
case refine'_2.intro.intro
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x✝ : G
hx : x✝ ∈ closure (⋃ (i : ι), ↑(K i))
x y : G
i : ι
hi : x ∈ K i
j : ι
hj : y ∈ K j
⊢ ∃ i, x * y ∈ K i
case refine'_2
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(K i))
⊢ ∀ (x y : G), (∃ i, x ∈ K i) → (∃ i, y ∈ K i) → ∃ i, x * y ∈ K i
rintro x y ⟨i, hi⟩ ⟨j, hj⟩
case refine'_2.intro.intro.intro.intro
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k✝ : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x✝ : G
hx : x✝ ∈ closure (⋃ (i : ι), ↑(K i))
x y : G
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
case refine'_2.intro.intro
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x✝ : G
hx : x✝ ∈ closure (⋃ (i : ι), ↑(K i))
x y : G
i : ι
hi : x ∈ K i
j : ι
hj : y ∈ K j
⊢ ∃ i, x * y ∈ K i
rcases hK i j with ⟨k, hki, hkj⟩
no goals
case refine'_2.intro.intro.intro.intro
G : Type u_2
G' : Type ?u.224092
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.224101
inst✝ : AddGroup A
H K✝ : Subgroup G
k✝ : Set G
ι : Sort u_1
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x x_1 => x ≤ x_1) K
x✝ : G
hx : x✝ ∈ closure (⋃ (i : ι), ↑(K i))
x y : G
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
exact ⟨k, mul_mem (hki hi) (hkj hj)⟩