α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ ⨆ (i : ι), S i
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
rw [iSup_eq_closure] at hx
case refine'_1
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x

case refine'_2
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x⁻¹
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
refine' closure_induction'' hx (fun x hx => _) (fun x hx => _) h1 hmul
case refine'_1.intro
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x
case refine'_1
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
no goals
case refine'_1.intro
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x
exact hp _ _ hi
case refine'_2.intro
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x⁻¹
case refine'_2
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x⁻¹
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
no goals
case refine'_2.intro
α : Type ?u.10942
G : Type u_2
A : Type ?u.10948
S✝ : Type ?u.10951
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_1
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x⁻¹
exact hp _ _ (inv_mem hi)