Theorem: Algdata.BinaryHeap.IsHeap.of_subext (Algdata/Data/BinaryHeap/Lemmas.lean)

State before:
α : Type u
lt : α → α → Bool
x y : Subarray α
i : Nat
h : IsHeap lt x i
hsize : Subarray.size y ≤ Subarray.size x
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
⊢ IsHeap lt y i
Tactic:
induction h with
| out_of_range i hi =>
  exact .out_of_range i <| Nat.le_trans hsize hi
| node' i _ lt_left lt_right _ _ IH₁ IH₂ =>
  specialize IH₁ fun k hk h => hext k hk (.node_left _ h)
  specialize IH₂ fun k hk h => hext k hk (.node_right _ h)
  if hiy : i < y.size then
    refine .node' i hiy ?_ ?_ IH₁ IH₂
    . intro hl
      rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
      exact lt_left <| Nat.lt_of_lt_of_le hl hsize
    . intro hr
      rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
      exact lt_right <| Nat.lt_of_lt_of_le hr hsize
  else
    exact .out_of_range i (Nat.le_of_not_lt hiy)
State after:
no goals

State before:
case out_of_range
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
hi : i ≥ Subarray.size x
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
⊢ IsHeap lt y i
Tactic:
exact .out_of_range i <| Nat.le_trans hsize hi
State after:
no goals

State before:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IH₁ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 1) k → y[k] = x[k]) → IsHeap lt y (2 * i + 1)
IH₂ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]) → IsHeap lt y (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
⊢ IsHeap lt y i
Tactic:
specialize IH₁ fun k hk h => hext k hk (.node_left _ h)
State after:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IH₂ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]) → IsHeap lt y (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
⊢ IsHeap lt y i

State before:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IH₂ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]) → IsHeap lt y (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
⊢ IsHeap lt y i
Tactic:
specialize IH₂ fun k hk h => hext k hk (.node_right _ h)
State after:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
⊢ IsHeap lt y i

State before:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
⊢ IsHeap lt y i
Tactic:
if hiy : i < y.size then
  refine .node' i hiy ?_ ?_ IH₁ IH₂
  . intro hl
    rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
    exact lt_left <| Nat.lt_of_lt_of_le hl hsize
  . intro hr
    rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
    exact lt_right <| Nat.lt_of_lt_of_le hr hsize
else
  exact .out_of_range i (Nat.le_of_not_lt hiy)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ IsHeap lt y i
Tactic:
refine .node' i hiy ?_ ?_ IH₁ IH₂
State after:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 1 < Subarray.size y), lt y[i] y[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false

State before:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 1 < Subarray.size y), lt y[i] y[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false
Tactic:
. intro hl
  rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
  exact lt_left <| Nat.lt_of_lt_of_le hl hsize
State after:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false

State before:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false
Tactic:
. intro hr
  rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
  exact lt_right <| Nat.lt_of_lt_of_le hr hsize
State after:
no goals

State before:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 1 < Subarray.size y), lt y[i] y[2 * i + 1] = false
Tactic:
intro hl
State after:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hl : 2 * i + 1 < Subarray.size y
⊢ lt y[i] y[2 * i + 1] = false

State before:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hl : 2 * i + 1 < Subarray.size y
⊢ lt y[i] y[2 * i + 1] = false
Tactic:
rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
State after:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hl : 2 * i + 1 < Subarray.size y
⊢ lt x[i] x[2 * i + 1] = false

State before:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hl : 2 * i + 1 < Subarray.size y
⊢ lt x[i] x[2 * i + 1] = false
Tactic:
exact lt_left <| Nat.lt_of_lt_of_le hl hsize
State after:
no goals

State before:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false
Tactic:
intro hr
State after:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hr : 2 * i + 2 < Subarray.size y
⊢ lt y[i] y[2 * i + 2] = false

State before:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hr : 2 * i + 2 < Subarray.size y
⊢ lt y[i] y[2 * i + 2] = false
Tactic:
rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
State after:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hr : 2 * i + 2 < Subarray.size y
⊢ lt x[i] x[2 * i + 2] = false

State before:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hr : 2 * i + 2 < Subarray.size y
⊢ lt x[i] x[2 * i + 2] = false
Tactic:
exact lt_right <| Nat.lt_of_lt_of_le hr hsize
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : ¬i < Subarray.size y
⊢ IsHeap lt y i
Tactic:
exact .out_of_range i (Nat.le_of_not_lt hiy)
State after:
no goals