refine' ⟨ℚ ⧸ AddSubgroup.zmultiples (1 : ℚ), inferInstance, fun g => _, _⟩
⊢ ∃ G x, (∀ (g : G), IsOfFinAddOrder g) ∧ AddMonoid.exponent G = 0
case refine'_1
g : ℚ ⧸ AddSubgroup.zmultiples 1
⊢ IsOfFinAddOrder g

case refine'_2

⊢ AddMonoid.exponent (ℚ ⧸ AddSubgroup.zmultiples 1) = 0