cases' Nat.eq_zero_or_pos (Nat.gcd a b) with h₀ h₀
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
a b : ℕ
h₁ : mem_S_ge d ↑a ↑b
h₂ : mem a b I
⊢ a * I.b₁ = b * I.a₁
case inl
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
a b : ℕ
h₁ : mem_S_ge d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b = 0
⊢ a * I.b₁ = b * I.a₁

case inr
d : ℕ
inst✝ : NeZero d
I : BasicInterval
H : ∀ (a b : ℕ), Nat.Coprime a b → mem_S_ge d ↑a ↑b → mem a b I → a * I.b₁ = b * I.a₁
a b : ℕ
h₁ : mem_S_ge d ↑a ↑b
h₂ : mem a b I
h₀ : Nat.gcd a b > 0
⊢ a * I.b₁ = b * I.a₁