G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
let s := { n | 0 < n }.image fun n : ℕ => x ^ n
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
have hs : s ⊆ { y : G | ¬IsOfFinOrder y } := by
  rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
  apply h
  rw [isOfFinOrder_iff_pow_eq_one] at contra⊢
  obtain ⟨m, hm, hm'⟩ := contra
  exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ Set.Infinite s
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
suffices s.Infinite by exact this.mono hs
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
⊢ IsOfFinOrder x
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ Set.Infinite s
contrapose! h
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
this : ¬Injective fun n => x ^ n
⊢ IsOfFinOrder x
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
⊢ IsOfFinOrder x
have : ¬Injective fun n : ℕ => x ^ n := by
  have H := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) (Set.not_infinite.mp h)
  contrapose! H rw [not_not] at H exact Set.injOn_of_injective H _
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
this : ¬Injective fun n => x ^ n
⊢ IsOfFinOrder x
rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ False
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
⊢ s ⊆ {y | ¬IsOfFinOrder y}
rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ IsOfFinOrder x
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ False
apply h
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : ∃ n_1, 0 < n_1 ∧ (x ^ n) ^ n_1 = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ IsOfFinOrder x
rw [isOfFinOrder_iff_pow_eq_one] at contra⊢
case intro.intro.intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m✝ : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : ∃ n_1, 0 < n_1 ∧ (x ^ n) ^ n_1 = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
obtain ⟨m, hm, hm'⟩ := contra
no goals
case intro.intro.intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m✝ : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m✝ : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ x ^ (n * m) = 1
rwa [pow_mul]
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
this : Set.Infinite s
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
exact this.mono hs
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
H : ¬Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n => x ^ n
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
⊢ ¬Injective fun n => x ^ n
have H := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) (Set.not_infinite.mp h)
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
H : ¬¬Injective fun n => x ^ n
⊢ Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
H : ¬Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n => x ^ n
contrapose! H
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
H : Injective fun n => x ^ n
⊢ Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
H : ¬¬Injective fun n => x ^ n
⊢ Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
rw [not_not] at H
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
H : Injective fun n => x ^ n
⊢ Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
exact Set.injOn_of_injective H _