cases' dom_of_mem d hab hIab (condition_of_feasible hI) with H H
case inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
case inr.intro.intro.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b

case inr.intro.intro.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b