Theorem: Algdata.BinaryHeap.size_as_popMax (Algdata/Data/BinaryHeap/Basic.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Array.size (popMax lt x).as = Array.size x.as
Tactic:
delta popMax
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Array.size
      (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as =
    Array.size x.as

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Array.size
      (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as =
    Array.size x.as
Tactic:
if h : x.start < x.stop then
  simp only [dif_pos h, size_as_heapifyDown, Subarray.size_as_shrinkOne', Subarray.size_as_swap]
else
  simp only [dif_neg h]
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ Array.size
      (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as =
    Array.size x.as
Tactic:
simp only [dif_pos h, size_as_heapifyDown, Subarray.size_as_shrinkOne', Subarray.size_as_swap]
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : ¬x.start < x.stop
⊢ Array.size
      (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as =
    Array.size x.as
Tactic:
simp only [dif_neg h]
State after:
no goals