obtain ⟨h₁, h₂⟩ := h
I : BasicInterval
a b g : ℕ
hg : 0 < g
h : mem (a * g) (b * g) I
⊢ mem a b I
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : b * g * I.a₁ ≤ a * g * I.b₁
h₂ : a * g * I.b₂ ≤ b * g * I.a₂
⊢ mem a b I