simp only [h₁, mul_assoc, h₂, mul_comm I.a₂] at h
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : a * I.b₂ < b * I.a₂
⊢ False
case intro.intro.intro.refine_1
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