rcases help i j hij with rfl | rfl | ⟨rfl, rfl⟩
case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i j : Fin (Nat.succ 2)
hij : i ≤ j
⊢ of_fraction d a b i ≤ of_fraction d a b j
case refine_2.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
j : Fin (Nat.succ 2)
hij : 0 ≤ j
⊢ of_fraction d a b 0 ≤ of_fraction d a b j

case refine_2.inr.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i : Fin (Nat.succ 2)
hij : i ≤ i
⊢ of_fraction d a b i ≤ of_fraction d a b i

case refine_2.inr.inr.intro
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
hij : 1 ≤ 2
⊢ of_fraction d a b 1 ≤ of_fraction d a b 2