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

State before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
h : IsHeap lt x i
j : Nat
hj : j < Subarray.size x
hd : Descendant i j
⊢ lt x[i] x[j] = false
Tactic:
induction hd with
| refl => exact LawfulLTBRel.irrefl _
| node_left i hd IH =>
  exact LawfulLTBRel.ntrans (h.not_lt_left _) (IH h.left)
| node_right i hd IH =>
  exact LawfulLTBRel.ntrans (h.not_lt_right _) (IH h.right)
State after:
no goals

State before:
case refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hj : j < Subarray.size x
h : IsHeap lt x j
⊢ lt x[j] x[j] = false
Tactic:
exact LawfulLTBRel.irrefl _
State after:
no goals

State before:
case node_left
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i✝ j : Nat
hj : j < Subarray.size x
i : Nat
hd : Descendant (2 * i + 1) j
IH : IsHeap lt x (2 * i + 1) → lt x[2 * i + 1] x[j] = false
h : IsHeap lt x i
⊢ lt x[i] x[j] = false
Tactic:
exact LawfulLTBRel.ntrans (h.not_lt_left _) (IH h.left)
State after:
no goals

State before:
case node_right
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i✝ j : Nat
hj : j < Subarray.size x
i : Nat
hd : Descendant (2 * i + 2) j
IH : IsHeap lt x (2 * i + 2) → lt x[2 * i + 2] x[j] = false
h : IsHeap lt x i
⊢ lt x[i] x[j] = false
Tactic:
exact LawfulLTBRel.ntrans (h.not_lt_right _) (IH h.right)
State after:
no goals