rcases eq_or_eq_or_mem_interior_of_mem hm with H | H | H
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₁ = b * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

case inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₂ = b * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

case inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b