rw [AddMonoid.exponent_eq_zero_iff, AddMonoid.ExponentExists]
case refine'_2

⊢ AddMonoid.exponent (ℚ ⧸ AddSubgroup.zmultiples 1) = 0
case refine'_2

⊢ ¬∃ n, 0 < n ∧ ∀ (g : ℚ ⧸ AddSubgroup.zmultiples 1), n • g = 0