Theorem: Algdata.BinaryHeap.heapSort_spec (Algdata/Data/BinaryHeap/Lemmas.lean)

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ lt (heapSort lt x)[j] (heapSort lt x)[i] = false
Tactic:
refine (heapSort.Intermed.mkHeap lt x).of_spec (.mk lt (mkHeap lt x) _) .refl i j ?_ hij ?_
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ (mkHeap lt x).stop - Subarray.size (mkHeap lt x) ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < (mkHeap lt x).stop

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ (mkHeap lt x).stop - Subarray.size (mkHeap lt x) ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < (mkHeap lt x).stop
Tactic:
all_goals simp only [size_mkHeap, stop_mkHeap]
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.stop - Subarray.size x ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.stop - Subarray.size x ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Tactic:
. simp only [Subarray.size, Nat.sub_sub_self x.h₁]
  exact hi
State after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Tactic:
. exact hj
State after:
no goals

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < (mkHeap lt x).stop
Tactic:
simp only [size_mkHeap, stop_mkHeap]
State after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.stop - Subarray.size x ≤ i
Tactic:
simp only [Subarray.size, Nat.sub_sub_self x.h₁]
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.start ≤ i

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.start ≤ i
Tactic:
exact hi
State after:
no goals

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Tactic:
exact hj
State after:
no goals