Theorem: l1_2_20_iii' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
g : G
h : ¬IsOfFinOrder g
⊢ Set.Infinite ↑(Subgroup.closure {g})
Tactic:
rw [l1_2_20_ii' _ _ h]
State after:
G : Type u_1
inst✝ : Group G
g : G
h : ¬IsOfFinOrder g
⊢ Set.Infinite {x | ∃ i, g ^ i = x}

State before:
G : Type u_1
inst✝ : Group G
g : G
h : ¬IsOfFinOrder g
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Tactic:
rw [← orderOf_eq_zero_iff] at h
State after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite {x | ∃ i, g ^ i = x}

State before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Tactic:
have : ((Set.univ : Set ℕ).image fun i => g ^ i).Infinite := by
  simp
  apply Set.infinite_range_of_injective
  intro x y hxy
  rwa [pow_inj_iff_of_orderOf_eq_zero h] at hxy
State after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ Set.Infinite {x | ∃ i, g ^ i = x}

State before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
Tactic:
apply Set.Infinite.mono _ this
State after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ (fun i => g ^ i) '' Set.univ ⊆ {x | ∃ i, g ^ i = x}

State before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ (fun i => g ^ i) '' Set.univ ⊆ {x | ∃ i, g ^ i = x}
Tactic:
intro x hx
State after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : x ∈ (fun i => g ^ i) '' Set.univ
⊢ x ∈ {x | ∃ i, g ^ i = x}

State before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : x ∈ (fun i => g ^ i) '' Set.univ
⊢ x ∈ {x | ∃ i, g ^ i = x}
Tactic:
simp only [Set.image_univ, Set.mem_range] at hx
State after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ x ∈ {x | ∃ i, g ^ i = x}

State before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ x ∈ {x | ∃ i, g ^ i = x}
Tactic:
simp only [Set.mem_setOf]
State after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ ∃ i, g ^ i = x

State before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ ∃ i, g ^ i = x
Tactic:
obtain ⟨n, hn⟩ := hx
State after:
case intro
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ ∃ i, g ^ i = x

State before:
case intro
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ ∃ i, g ^ i = x
Tactic:
use n
State after:
case h
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ g ^ ↑n = x

State before:
case h
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ g ^ ↑n = x
Tactic:
simp only [zpow_ofNat, hn]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite ((fun i => g ^ i) '' Set.univ)
Tactic:
simp
State after:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite (Set.range fun i => g ^ i)

State before:
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite (Set.range fun i => g ^ i)
Tactic:
apply Set.infinite_range_of_injective
State after:
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Function.Injective fun i => g ^ i

State before:
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Function.Injective fun i => g ^ i
Tactic:
intro x y hxy
State after:
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
x y : ℕ
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y

State before:
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
x y : ℕ
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y
Tactic:
rwa [pow_inj_iff_of_orderOf_eq_zero h] at hxy
State after:
no goals