all_goals simp [ha, hb]
case b0
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ 0 < 2 * ↑b

case d0
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ 0 < ↑a
no goals