case intro
G : Type u_1
H : Type ?u.211777
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
x : G
hx : x ≠ 1
⊢ ∃ g, ¬IsOfFinOrder g
G : Type u_1
H : Type ?u.211777
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
⊢ ∃ g, ¬IsOfFinOrder g
obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
no goals
case intro
G : Type u_1
H : Type ?u.211777
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
x : G
hx : x ≠ 1
⊢ ∃ g, ¬IsOfFinOrder g
exact ⟨x, (tfG x) hx⟩