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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Subarray.size (popMax lt x) = Subarray.size x - 1
Tactic:
delta popMax
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Subarray.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) =
    Subarray.size x - 1

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Subarray.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) =
    Subarray.size x - 1
Tactic:
cases Nat.lt_or_eq_of_le x.h₁ with
| inl hlt =>
  simp only [dif_pos hlt, size_heapifyDown, Subarray.size_shrinkOne', Subarray.size_swap]
| inr heq =>
  rewrite [dif_neg (c:=x.start < x.stop) (heq ▸ x.start.lt_irrefl)]
  simp only [Subarray.size, heq, x.stop.sub_self]
State after:
no goals

State before:
case inl
α : Type u
lt : α → α → Bool
x : Subarray α
hlt : x.start < x.stop
⊢ Subarray.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) =
    Subarray.size x - 1
Tactic:
simp only [dif_pos hlt, size_heapifyDown, Subarray.size_shrinkOne', Subarray.size_swap]
State after:
no goals

State before:
case inr
α : Type u
lt : α → α → Bool
x : Subarray α
heq : x.start = x.stop
⊢ Subarray.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) =
    Subarray.size x - 1
Tactic:
rewrite [dif_neg (c:=x.start < x.stop) (heq ▸ x.start.lt_irrefl)]
State after:
case inr
α : Type u
lt : α → α → Bool
x : Subarray α
heq : x.start = x.stop
⊢ Subarray.size x = Subarray.size x - 1

State before:
case inr
α : Type u
lt : α → α → Bool
x : Subarray α
heq : x.start = x.stop
⊢ Subarray.size x = Subarray.size x - 1
Tactic:
simp only [Subarray.size, heq, x.stop.sub_self]
State after:
no goals