case h
G : Type u_1
H : Type ?u.193982
inst✝ : CommMonoid G
tG : IsTorsion G
x✝ : G
⊢ x✝ ∈ torsion G ↔ x✝ ∈ ⊤
G : Type u_1
H : Type ?u.193982
inst✝ : CommMonoid G
tG : IsTorsion G
⊢ torsion G = ⊤
ext
no goals
case h
G : Type u_1
H : Type ?u.193982
inst✝ : CommMonoid G
tG : IsTorsion G
x✝ : G
⊢ x✝ ∈ torsion G ↔ x✝ ∈ ⊤
tauto