simp only [Subarray.size_as_swap] at *
case node_odd_next
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y x✝ : Subarray α
i✝ : Nat
hi✝ : i✝ < Subarray.size x✝
hl✝ : 2 * i✝ + 1 < Subarray.size x✝
a✝¹ : 2 * i✝ + 2 ≥ Subarray.size x✝
a✝ : lt x✝[i✝] x✝[2 * i✝ + 1] = true
⊢ Array.size (Subarray.swap x✝ { val := i✝, isLt := hi✝ } { val := 2 * i✝ + 1, isLt := hl✝ }).as = Array.size x✝.as
no goals