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

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ IsHeap lt (mkHeap lt x) 0
Tactic:
rewrite [mkHeap_eq_foldRev]
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ IsHeap lt (Nat.foldRev (fun n x => heapifyDown lt x n) (Subarray.size x / 2) x) 0

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ IsHeap lt (Nat.foldRev (fun n x => heapifyDown lt x n) (Subarray.size x / 2) x) 0
Tactic:
refine Nat.foldRev_induction (motive:=fun n x => ∀ k, n ≤ k → IsHeap lt x k) _ _ x ?_ ?_ 0 .refl
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (Subarray.size x / 2) x

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (Subarray.size x / 2) x

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
Tactic:
. show ∀ k, x.size / 2 ≤ k → IsHeap lt x k
  intro k hk
  refine .leaf lt x k ?_
  rewrite [← Nat.div_add_mod x.size 2]
  refine Nat.add_le_add ?_ ?_
  . exact Nat.mul_le_mul_left 2 hk
  . apply Nat.le_of_succ_le_succ
    exact show x.size % 2 < 2 from Nat.mod_lt x.size (by decide)
State after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
Tactic:
. show ∀ (n : Nat) (x : Subarray α), (∀ k, n+1 ≤ k → IsHeap lt x k) → ∀ k, n ≤ k → IsHeap lt (heapifyDown lt x n) k
  clear x; intro n x IH k hk
  if hk' : Descendant n k then
    suffices IsHeap lt (heapifyDown lt x n) n from
      this.descend hk'
    have : n ≤ 2 * n := by
      rewrite [Nat.two_mul]; exact Nat.le_add_left n n
    refine is_heap_heapifyDown lt x n ?_ ?_
    all_goals apply IH; apply Nat.succ_le_succ
    . exact this
    . exact .step this
  else
    have : n < k := Nat.lt_of_not_le fun h => by
      cases Nat.le_antisymm hk h
      exact hk' (.refl _)
    refine .of_subext (IH k this) (Nat.le_of_eq <| size_heapifyDown lt x _) ?_
    intro i hi hki
    suffices ¬ Descendant n i from
      get_heapifyDown_not_descendant lt x n i this
    intro hni
    exact hk' <| Descendant.ascend_right hk hni hki
State after:
no goals

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (Subarray.size x / 2) x
Tactic:
show ∀ k, x.size / 2 ≤ k → IsHeap lt x k
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat), Subarray.size x / 2 ≤ k → IsHeap lt x k

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat), Subarray.size x / 2 ≤ k → IsHeap lt x k
Tactic:
intro k hk
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ IsHeap lt x k

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ IsHeap lt x k
Tactic:
refine .leaf lt x k ?_
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * k + 1 ≥ Subarray.size x

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * k + 1 ≥ Subarray.size x
Tactic:
rewrite [← Nat.div_add_mod x.size 2]
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * k + 1 ≥ 2 * (Subarray.size x / 2) + Subarray.size x % 2

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * k + 1 ≥ 2 * (Subarray.size x / 2) + Subarray.size x % 2
Tactic:
refine Nat.add_le_add ?_ ?_
State after:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * (Subarray.size x / 2) ≤ 2 * k

case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1

State before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * (Subarray.size x / 2) ≤ 2 * k

case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1
Tactic:
. exact Nat.mul_le_mul_left 2 hk
State after:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1

State before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1
Tactic:
. apply Nat.le_of_succ_le_succ
  exact show x.size % 2 < 2 from Nat.mod_lt x.size (by decide)
State after:
no goals

State before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * (Subarray.size x / 2) ≤ 2 * k
Tactic:
exact Nat.mul_le_mul_left 2 hk
State after:
no goals

State before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1
Tactic:
apply Nat.le_of_succ_le_succ
State after:
case refine_1.refine_2.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Nat.succ (Subarray.size x % 2) ≤ Nat.succ 1

State before:
case refine_1.refine_2.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Nat.succ (Subarray.size x % 2) ≤ Nat.succ 1
Tactic:
exact show x.size % 2 < 2 from Nat.mod_lt x.size (by decide)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 > 0
Tactic:
decide
State after:
no goals

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
Tactic:
show ∀ (n : Nat) (x : Subarray α), (∀ k, n+1 ≤ k → IsHeap lt x k) → ∀ k, n ≤ k → IsHeap lt (heapifyDown lt x n) k
State after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k
Tactic:
clear x
State after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k
Tactic:
intro n x IH k hk
State after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
⊢ IsHeap lt (heapifyDown lt x n) k

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
⊢ IsHeap lt (heapifyDown lt x n) k
Tactic:
if hk' : Descendant n k then
  suffices IsHeap lt (heapifyDown lt x n) n from
    this.descend hk'
  have : n ≤ 2 * n := by
    rewrite [Nat.two_mul]; exact Nat.le_add_left n n
  refine is_heap_heapifyDown lt x n ?_ ?_
  all_goals apply IH; apply Nat.succ_le_succ
  . exact this
  . exact .step this
else
  have : n < k := Nat.lt_of_not_le fun h => by
    cases Nat.le_antisymm hk h
    exact hk' (.refl _)
  refine .of_subext (IH k this) (Nat.le_of_eq <| size_heapifyDown lt x _) ?_
  intro i hi hki
  suffices ¬ Descendant n i from
    get_heapifyDown_not_descendant lt x n i this
  intro hni
  exact hk' <| Descendant.ascend_right hk hni hki
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ IsHeap lt (heapifyDown lt x n) k
Tactic:
suffices IsHeap lt (heapifyDown lt x n) n from
  this.descend hk'
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ IsHeap lt (heapifyDown lt x n) n

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ IsHeap lt (heapifyDown lt x n) n
Tactic:
have : n ≤ 2 * n := by
  rewrite [Nat.two_mul]; exact Nat.le_add_left n n
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt (heapifyDown lt x n) n

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt (heapifyDown lt x n) n
Tactic:
refine is_heap_heapifyDown lt x n ?_ ?_
State after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 1)

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 2)

State before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 1)

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 2)
Tactic:
all_goals apply IH; apply Nat.succ_le_succ
State after:
case refine_1.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n

case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1

State before:
case refine_1.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n

case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1
Tactic:
. exact this
State after:
case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1

State before:
case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1
Tactic:
. exact .step this
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ n ≤ 2 * n
Tactic:
rewrite [Nat.two_mul]
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ n ≤ n + n

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ n ≤ n + n
Tactic:
exact Nat.le_add_left n n
State after:
no goals

State before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 2)
Tactic:
apply IH
State after:
case refine_2.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n + 1 ≤ 2 * n + 2

State before:
case refine_2.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n + 1 ≤ 2 * n + 2
Tactic:
apply Nat.succ_le_succ
State after:
case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1

State before:
case refine_1.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n
Tactic:
exact this
State after:
no goals

State before:
case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1
Tactic:
exact .step this
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
⊢ IsHeap lt (heapifyDown lt x n) k
Tactic:
have : n < k := Nat.lt_of_not_le fun h => by
  cases Nat.le_antisymm hk h
  exact hk' (.refl _)
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
⊢ IsHeap lt (heapifyDown lt x n) k

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
⊢ IsHeap lt (heapifyDown lt x n) k
Tactic:
refine .of_subext (IH k this) (Nat.le_of_eq <| size_heapifyDown lt x _) ?_
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
⊢ ∀ (k_1 : Nat) (hk : k_1 < Subarray.size (heapifyDown lt x n)), Descendant k k_1 → (heapifyDown lt x n)[k_1] = x[k_1]

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
⊢ ∀ (k_1 : Nat) (hk : k_1 < Subarray.size (heapifyDown lt x n)), Descendant k k_1 → (heapifyDown lt x n)[k_1] = x[k_1]
Tactic:
intro i hi hki
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ (heapifyDown lt x n)[i] = x[i]

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ (heapifyDown lt x n)[i] = x[i]
Tactic:
suffices ¬ Descendant n i from
  get_heapifyDown_not_descendant lt x n i this
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ ¬Descendant n i

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ ¬Descendant n i
Tactic:
intro hni
State after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
hni : Descendant n i
⊢ False

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
hni : Descendant n i
⊢ False
Tactic:
exact hk' <| Descendant.ascend_right hk hni hki
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
h : k ≤ n
⊢ False
Tactic:
cases Nat.le_antisymm hk h
State after:
case refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
hk : n ≤ n
hk' : ¬Descendant n n
h : n ≤ n
⊢ False

State before:
case refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
hk : n ≤ n
hk' : ¬Descendant n n
h : n ≤ n
⊢ False
Tactic:
exact hk' (.refl _)
State after:
no goals