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

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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (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).stop =
    x.stop - 1
Tactic:
simp only [dif_pos h, stop_heapifyDown]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop =
    x.stop - 1

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop =
    x.stop - 1
Tactic:
refine Eq.trans (Subarray.stop_shrinkOne' _ ?_) ?_
State after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).start <
    (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).stop

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).stop -
      1 =
    x.stop - 1

State before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).start <
    (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).stop

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).stop -
      1 =
    x.stop - 1
Tactic:
all_goals simp only [Subarray.stop_swap, Subarray.start_swap]
State after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ x.start < x.stop

State before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ x.start < x.stop
Tactic:
exact h
State after:
no goals

State before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).stop -
      1 =
    x.stop - 1
Tactic:
simp only [Subarray.stop_swap, Subarray.start_swap]
State after:
no goals