α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ ∀ (n : ℕ), 0 < n → g ^ n ≠ 1
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = 0
rw [orderOf_eq_zero_iff']
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
⊢ False
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ ∀ (n : ℕ), 0 < n → g ^ n ≠ 1
refine' fun n hn hgn => _
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
⊢ False
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
⊢ False
have ho := orderOf_pos' ((isOfFinOrder_iff_pow_eq_one g).mpr ⟨n, hn, hgn⟩)
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : ?m.100048
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ False
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
⊢ False
obtain ⟨x, hx⟩ :=
  Infinite.exists_not_mem_finset
    (Finset.image (fun x => g ^ x) <| Finset.range <| orderOf g)
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : ?m.100048
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ False
apply hx
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ ∃ n, g ^ n = x
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
rw [← mem_powers_iff_mem_range_order_of' (x:=g) (y:=x) ho, Submonoid.mem_powers_iff]
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℤ
hk : (fun x x_1 => x ^ x_1) g k = x
⊢ ∃ n, g ^ n = x
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ ∃ n, g ^ n = x
obtain ⟨k, hk⟩ := h x
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℤ
hk : g ^ k = x
⊢ ∃ n, g ^ n = x
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℤ
hk : (fun x x_1 => x ^ x_1) g k = x
⊢ ∃ n, g ^ n = x
dsimp at hk
case intro.intro.intro.inl
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ ↑k = x
⊢ ∃ n, g ^ n = x

case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k) = x
⊢ ∃ n, g ^ n = x
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℤ
hk : g ^ k = x
⊢ ∃ n, g ^ n = x
obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
⊢ ∃ n, g ^ n = x
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k) = x
⊢ ∃ n, g ^ n = x
rw [zpow_eq_mod_orderOf] at hk
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
this : 0 ≤ -↑k % ↑(orderOf g)
⊢ ∃ n, g ^ n = x
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
⊢ ∃ n, g ^ n = x
have : 0 ≤ (-k % orderOf g : ℤ) := Int.emod_nonneg (-k) (by exact_mod_cast ho.ne')
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
this : 0 ≤ -↑k % ↑(orderOf g)
⊢ g ^ Int.toNat (-↑k % ↑(orderOf g)) = x
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
this : 0 ≤ -↑k % ↑(orderOf g)
⊢ ∃ n, g ^ n = x
refine' ⟨(-k % orderOf g : ℤ).toNat, _⟩
no goals
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
this : 0 ≤ -↑k % ↑(orderOf g)
⊢ g ^ Int.toNat (-↑k % ↑(orderOf g)) = x
rwa [← zpow_ofNat, Int.toNat_of_nonneg this]
no goals
case intro.intro.intro.inl
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ ↑k = x
⊢ ∃ n, g ^ n = x
exact ⟨k, by exact_mod_cast hk⟩
no goals
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ ↑k = x
⊢ g ^ k = x
exact_mod_cast hk
no goals
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
⊢ ↑(orderOf g) ≠ 0
exact_mod_cast ho.ne'