simp only [h₁, mul_assoc, h₂, mul_comm I.a₁] at h
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : b * I.a₁ < a * I.b₁
⊢ False
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : k₁ * (I.b₁ * I.a₁) < k₁ * (I.b₁ * I.a₁)
⊢ False