G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : LeftCancelMonoid G
inst✝¹ : AddLeftCancelMonoid A
inst✝ : Finite G
x : G
H : Set.Finite Set.univ
⊢ IsOfFinOrder x
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : LeftCancelMonoid G
inst✝¹ : AddLeftCancelMonoid A
inst✝ : Finite G
x : G
⊢ IsOfFinOrder x
have H : (Set.univ : Set G).Finite := Set.univ.toFinite
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : LeftCancelMonoid G
inst✝¹ : AddLeftCancelMonoid A
inst✝ : Finite G
x : G
H : ¬IsOfFinOrder x
⊢ ¬Set.Finite Set.univ
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : LeftCancelMonoid G
inst✝¹ : AddLeftCancelMonoid A
inst✝ : Finite G
x : G
H : Set.Finite Set.univ
⊢ IsOfFinOrder x
contrapose! H
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : LeftCancelMonoid G
inst✝¹ : AddLeftCancelMonoid A
inst✝ : Finite G
x : G
H : ¬IsOfFinOrder x
⊢ ¬Set.Finite Set.univ
exact Set.Infinite.mono (Set.subset_univ _) (infinite_not_isOfFinOrder H)