. simpa [← ENNReal.sub_right_inj ha' hba]
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b ≤ a
⊢ b = 0

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a