Theorem: l1_2_20_ii' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
⊢ ↑(Subgroup.closure {g}) = {x | ∃ i, g ^ i = x}
Tactic:
rw [← Subgroup.zpowers_eq_closure]
State after:
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
⊢ ↑(Subgroup.zpowers g) = {x | ∃ i, g ^ i = x}

State before:
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
⊢ ↑(Subgroup.zpowers g) = {x | ∃ i, g ^ i = x}
Tactic:
ext
State after:
case h
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
x✝ : G
⊢ x✝ ∈ ↑(Subgroup.zpowers g) ↔ x✝ ∈ {x | ∃ i, g ^ i = x}

State before:
case h
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
x✝ : G
⊢ x✝ ∈ ↑(Subgroup.zpowers g) ↔ x✝ ∈ {x | ∃ i, g ^ i = x}
Tactic:
simp [Subgroup.mem_zpowers_iff]
State after:
no goals