G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
⊢ ¬IsOfFinOrder x
simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ False
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1
intro n hn_pos hnx
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ False
rw [← pow_zero x] at hnx
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False
rw [h hnx] at hn_pos
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False
exact irrefl 0 hn_pos