G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
⊢ False
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
⊢ ∃ g, g ^ m ≠ 1
by_contra' h
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
hcon : exponent G ≤ m
⊢ False
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
⊢ False
have hcon : exponent G ≤ m := exponent_min' m hpos h
no goals
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
hcon : exponent G ≤ m
⊢ False
linarith