Theorem: Algdata.BinaryHeap.Descendant.sibling_not (Algdata/Data/BinaryHeap/Index.lean)

State before:
i : Nat
⊢ ¬Descendant (2 * i + 1) (2 * i + 2)
Tactic:
intro h
State after:
i : Nat
h : Descendant (2 * i + 1) (2 * i + 2)
⊢ False

State before:
i : Nat
h : Descendant (2 * i + 1) (2 * i + 2)
⊢ False
Tactic:
generalize hn : 2*i+1 = n at h
State after:
i n : Nat
hn : 2 * i + 1 = n
h : Descendant n (2 * i + 2)
⊢ False

State before:
i n : Nat
hn : 2 * i + 1 = n
h : Descendant n (2 * i + 2)
⊢ False
Tactic:
cases h with
| refl => cases Nat.add_left_cancel hn
| node_left _ h =>
  cases hn; apply absurd h.le
  rewrite [Nat.two_mul (2*i+1), Nat.succ_le_succ_iff, Nat.add_le_add_iff_left (m:=0)]
  exact (2*i).not_lt_zero
| node_right _ h =>
  cases hn; apply absurd h.le
  rewrite [Nat.two_mul (2*i+1), Nat.add_le_add_iff_right]
  conv => rhs; rhs; change 2*i+0
  rewrite [Nat.add_assoc, Nat.add_le_add_iff_left, Nat.add_comm 1]
  exact (2*i+1).not_lt_zero
State after:
no goals

State before:
case refl
i : Nat
hn : 2 * i + 1 = 2 * i + 2
⊢ False
Tactic:
cases Nat.add_left_cancel hn
State after:
no goals

State before:
case node_left
i n : Nat
hn : 2 * i + 1 = n
h : Descendant (2 * n + 1) (2 * i + 2)
a✝ : n = 2 * n + 1 → HEq (_ : Descendant n (2 * i + 2)) h → False
⊢ False
Tactic:
cases hn
State after:
case node_left.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 1) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 1 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ False

State before:
case node_left.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 1) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 1 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ False
Tactic:
apply absurd h.le
State after:
case node_left.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 1) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 1 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * (2 * i + 1) + 1 ≤ 2 * i + 2

State before:
case node_left.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 1) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 1 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * (2 * i + 1) + 1 ≤ 2 * i + 2
Tactic:
rewrite [Nat.two_mul (2*i+1), Nat.succ_le_succ_iff, Nat.add_le_add_iff_left (m:=0)]
State after:
case node_left.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 1) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 1 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 ≤ 0

State before:
case node_left.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 1) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 1 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 ≤ 0
Tactic:
exact (2*i).not_lt_zero
State after:
no goals

State before:
case node_right
i n : Nat
hn : 2 * i + 1 = n
h : Descendant (2 * n + 2) (2 * i + 2)
a✝ : n = 2 * n + 2 → HEq (_ : Descendant n (2 * i + 2)) h → False
⊢ False
Tactic:
cases hn
State after:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ False

State before:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ False
Tactic:
apply absurd h.le
State after:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * (2 * i + 1) + 2 ≤ 2 * i + 2

State before:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * (2 * i + 1) + 2 ≤ 2 * i + 2
Tactic:
rewrite [Nat.two_mul (2*i+1), Nat.add_le_add_iff_right]
State after:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 + (2 * i + 1) ≤ 2 * i

State before:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 + (2 * i + 1) ≤ 2 * i
Tactic:
conv => rhs; rhs; change 2*i+0
State after:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 + (2 * i + 1) ≤ 2 * i + 0

State before:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 + (2 * i + 1) ≤ 2 * i + 0
Tactic:
rewrite [Nat.add_assoc, Nat.add_le_add_iff_left, Nat.add_comm 1]
State after:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 + 1 ≤ 0

State before:
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 + 1 ≤ 0
Tactic:
exact (2*i+1).not_lt_zero
State after:
no goals