G : Type u_1
G' : Type ?u.201068
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.201077
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
p : (x : G) → x ∈ closure k → Prop
Hs : ∀ (x : G) (h : x ∈ k), p x (_ : x ∈ ↑(closure k))
H1 : p 1 (_ : 1 ∈ closure k)
Hmul : ∀ (x : G) (hx : x ∈ closure k) (y : G) (hy : y ∈ closure k), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure k)
Hinv : ∀ (x : G) (hx : x ∈ closure k), p x hx → p x⁻¹ (_ : x⁻¹ ∈ closure k)
x : G
hx : x ∈ closure k
⊢ ∃ x_1, p x x_1
G : Type u_1
G' : Type ?u.201068
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.201077
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
p : (x : G) → x ∈ closure k → Prop
Hs : ∀ (x : G) (h : x ∈ k), p x (_ : x ∈ ↑(closure k))
H1 : p 1 (_ : 1 ∈ closure k)
Hmul : ∀ (x : G) (hx : x ∈ closure k) (y : G) (hy : y ∈ closure k), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure k)
Hinv : ∀ (x : G) (hx : x ∈ closure k), p x hx → p x⁻¹ (_ : x⁻¹ ∈ closure k)
x : G
hx : x ∈ closure k
⊢ p x hx
refine' Exists.elim _ fun (hx : x ∈ closure k) (hc : p x hx) => hc
no goals
G : Type u_1
G' : Type ?u.201068
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.201077
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
p : (x : G) → x ∈ closure k → Prop
Hs : ∀ (x : G) (h : x ∈ k), p x (_ : x ∈ ↑(closure k))
H1 : p 1 (_ : 1 ∈ closure k)
Hmul : ∀ (x : G) (hx : x ∈ closure k) (y : G) (hy : y ∈ closure k), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure k)
Hinv : ∀ (x : G) (hx : x ∈ closure k), p x hx → p x⁻¹ (_ : x⁻¹ ∈ closure k)
x : G
hx : x ∈ closure k
⊢ ∃ x_1, p x x_1
exact
  closure_induction hx (fun x hx => ⟨_, Hs x hx⟩) ⟨_, H1⟩
    (fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ => ⟨_, Hmul _ _ _ _ hx hy⟩) fun x ⟨hx', hx⟩ => ⟨_, Hinv _ _ hx⟩