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

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
⊢ IsHeap lt x i
Tactic:
if hi : i < x.size then
  have hr : 2*i+2 ≥ x.size := .step hl
  refine .node' i hi ?_ ?_ (.out_of_range _ hl) (.out_of_range _ hr)
  . intro hl'; exact absurd hl' (Nat.not_lt_of_le hl)
  . intro hr'; exact absurd hr' (Nat.not_lt_of_le hr)
else
  exact .out_of_range i (Nat.ge_of_not_lt hi)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
⊢ IsHeap lt x i
Tactic:
have hr : 2*i+2 ≥ x.size := .step hl
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ IsHeap lt x i

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ IsHeap lt x i
Tactic:
refine .node' i hi ?_ ?_ (.out_of_range _ hl) (.out_of_range _ hr)
State after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false

State before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
. intro hl'; exact absurd hl' (Nat.not_lt_of_le hl)
State after:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false

State before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
. intro hr'; exact absurd hr' (Nat.not_lt_of_le hr)
State after:
no goals

State before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
Tactic:
intro hl'
State after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hl' : 2 * i + 1 < Subarray.size x
⊢ lt x[i] x[2 * i + 1] = false

State before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hl' : 2 * i + 1 < Subarray.size x
⊢ lt x[i] x[2 * i + 1] = false
Tactic:
exact absurd hl' (Nat.not_lt_of_le hl)
State after:
no goals

State before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
intro hr'
State after:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hr' : 2 * i + 2 < Subarray.size x
⊢ lt x[i] x[2 * i + 2] = false

State before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hr' : 2 * i + 2 < Subarray.size x
⊢ lt x[i] x[2 * i + 2] = false
Tactic:
exact absurd hr' (Nat.not_lt_of_le hr)
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : ¬i < Subarray.size x
⊢ IsHeap lt x i
Tactic:
exact .out_of_range i (Nat.ge_of_not_lt hi)
State after:
no goals