internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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
Proof 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
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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
Proof 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
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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)]
Proof 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
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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
Proof 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
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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
Proof 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
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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]
Proof 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
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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
Proof 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
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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]
Proof 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
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.sibling_not'
Proof state before:
i : Nat
⊢ ¬Descendant (2 * i + 2) (2 * i + 1)
Tactic:
intro h
Proof state after:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ False
Theorem: Algdata.BinaryHeap.Descendant.sibling_not'
Proof state before:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ False
Tactic:
apply absurd h.le
Proof state after:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ ¬2 * i + 2 ≤ 2 * i + 1
Theorem: Algdata.BinaryHeap.Descendant.sibling_not'
Proof state before:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ ¬2 * i + 2 ≤ 2 * i + 1
Tactic:
rewrite [Nat.add_le_add_iff_left]
Proof state after:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ ¬2 ≤ 1
Theorem: Algdata.BinaryHeap.Descendant.sibling_not'
Proof state before:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ ¬2 ≤ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
i j : Nat
h : Descendant i j
⊢ Descendant ((i - 1) / 2) ((j - 1) / 2)
Tactic:
induction h with
| refl => exact .refl _
| node_left i' _ IH =>
  rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at IH
  exact .trans (.parent i') IH
| node_right i' _ IH =>
  rewrite [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left _ _ (by decide)] at IH
  conv at IH =>
    lhs; change 0 + i'; rewrite [Nat.zero_add]
  exact .trans (.parent i') IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
case refl
i j : Nat
⊢ Descendant ((j - 1) / 2) ((j - 1) / 2)
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
case node_left
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant ((2 * i' + 1 - 1) / 2) ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at IH
Proof state after:
case node_left
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
case node_left
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
exact .trans (.parent i') IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant (2 * i' / 2) ((j - 1) / 2)
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant ((2 * i' + 2 - 1) / 2) ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
rewrite [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left _ _ (by decide)] at IH
Proof state after:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant (1 / 2 + i') ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant (1 / 2 + i') ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
conv at IH =>
  lhs; change 0 + i'; rewrite [Nat.zero_add]
Proof state after:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
case node_right
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
Tactic:
exact .trans (.parent i') IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend
Proof state before:
i j i' : Nat
h✝ : Descendant (2 * i' + 2) j
IH : Descendant ((1 + 2 * i') / 2) ((j - 1) / 2)
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
i j : Nat
h : Descendant i j
hij : i < j
⊢ Descendant i ((j - 1) / 2)
Tactic:
induction h with
| refl => exact absurd hij j.lt_irrefl
| node_left i h =>
  have := h.ascend
  rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at this
  exact this
| node_right i h =>
  have := h.ascend
  conv at this =>
    rw [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left _ _ (by decide)]
    lhs; change 0 + i; rw [Nat.zero_add]
  exact this
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
case refl
i j : Nat
hij : j < j
⊢ Descendant j ((j - 1) / 2)
Tactic:
exact absurd hij j.lt_irrefl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
case node_left
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
⊢ Descendant i ((j - 1) / 2)
Tactic:
have := h.ascend
Proof state after:
case node_left
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
this : Descendant ((2 * i + 1 - 1) / 2) ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
case node_left
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
this : Descendant ((2 * i + 1 - 1) / 2) ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Tactic:
rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at this
Proof state after:
case node_left
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
this : Descendant i ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
case node_left
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
this : Descendant i ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Tactic:
exact this
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
i✝ j i : Nat
h : Descendant (2 * i + 1) j
a✝ : 2 * i + 1 < j → Descendant (2 * i + 1) ((j - 1) / 2)
hij : i < j
this : Descendant (2 * i / 2) ((j - 1) / 2)
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
case node_right
i✝ j i : Nat
h : Descendant (2 * i + 2) j
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
⊢ Descendant i ((j - 1) / 2)
Tactic:
have := h.ascend
Proof state after:
case node_right
i✝ j i : Nat
h : Descendant (2 * i + 2) j
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
this : Descendant ((2 * i + 2 - 1) / 2) ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
case node_right
i✝ j i : Nat
h : Descendant (2 * i + 2) j
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
this : Descendant ((2 * i + 2 - 1) / 2) ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Tactic:
conv at this =>
  rw [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left _ _ (by decide)]
  lhs; change 0 + i; rw [Nat.zero_add]
Proof state after:
case node_right
i✝ j i : Nat
h : Descendant (2 * i + 2) j
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
this : Descendant i ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
case node_right
i✝ j i : Nat
h : Descendant (2 * i + 2) j
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
this : Descendant i ((j - 1) / 2)
⊢ Descendant i ((j - 1) / 2)
Tactic:
exact this
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right_parent
Proof state before:
i✝ j i : Nat
h : Descendant (2 * i + 2) j
a✝ : 2 * i + 2 < j → Descendant (2 * i + 2) ((j - 1) / 2)
hij : i < j
this : Descendant ((2 * i + 2 - 1) / 2) ((j - 1) / 2)
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
i j k : Nat
hij : i ≤ j
hik : Descendant i k
hjk : Descendant j k
⊢ Descendant i j
Tactic:
induction hjk with
| refl => exact hik
| node_left j _ IH =>
  specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_left j)))
  have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_left j))
  rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at this
  exact this
| node_right j _ IH =>
  specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_right j)))
  have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_right j))
  conv at this =>
    rhs; rw [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left 1 j (by decide)]
    change 0 + j; rw [Nat.zero_add]
  exact this
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case refl
i j k : Nat
hik : Descendant i k
hij : i ≤ k
⊢ Descendant i k
Tactic:
exact hik
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
IH : i ≤ 2 * j + 1 → Descendant i (2 * j + 1)
hij : i ≤ j
⊢ Descendant i j
Tactic:
specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_left j)))
Proof state after:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
⊢ Descendant i j
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
⊢ Descendant i j
Tactic:
have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_left j))
Proof state after:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
this : Descendant i ((2 * j + 1 - 1) / 2)
⊢ Descendant i j
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
this : Descendant i ((2 * j + 1 - 1) / 2)
⊢ Descendant i j
Tactic:
rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at this
Proof state after:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
this : Descendant i j
⊢ Descendant i j
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
this : Descendant i j
⊢ Descendant i j
Tactic:
exact this
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
this : Descendant i (2 * j / 2)
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
IH : i ≤ 2 * j + 2 → Descendant i (2 * j + 2)
hij : i ≤ j
⊢ Descendant i j
Tactic:
specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_right j)))
Proof state after:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
⊢ Descendant i j
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
⊢ Descendant i j
Tactic:
have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_right j))
Proof state after:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i ((2 * j + 2 - 1) / 2)
⊢ Descendant i j
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i ((2 * j + 2 - 1) / 2)
⊢ Descendant i j
Tactic:
conv at this =>
  rhs; rw [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left 1 j (by decide)]
  change 0 + j; rw [Nat.zero_add]
Proof state after:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i j
⊢ Descendant i j
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i j
⊢ Descendant i j
Tactic:
exact this
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascend_right
Proof state before:
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i ((2 * j + 2 - 1) / 2)
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascendants_total
Proof state before:
i j k : Nat
hik : Descendant i k
hjk : Descendant j k
⊢ Descendant i j ∨ Descendant j i
Tactic:
cases Nat.lt_or_ge i j with
| inl hlt => exact Or.inl <| ascend_right (Nat.le_of_lt hlt) hik hjk
| inr hge => exact Or.inr <| ascend_right hge hjk hik
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascendants_total
Proof state before:
case inl
i j k : Nat
hik : Descendant i k
hjk : Descendant j k
hlt : i < j
⊢ Descendant i j ∨ Descendant j i
Tactic:
exact Or.inl <| ascend_right (Nat.le_of_lt hlt) hik hjk
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.ascendants_total
Proof state before:
case inr
i j k : Nat
hik : Descendant i k
hjk : Descendant j k
hge : i ≥ j
⊢ Descendant i j ∨ Descendant j i
Tactic:
exact Or.inr <| ascend_right hge hjk hik
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.root
Proof state before:
i : Nat
⊢ Descendant 0 i
Tactic:
induction i using Nat.strongInductionOn
Proof state after:
case ind
n✝ : Nat
a✝ : ∀ (m : Nat), m < n✝ → Descendant 0 m
⊢ Descendant 0 n✝
Theorem: Algdata.BinaryHeap.Descendant.root
Proof state before:
case ind
n✝ : Nat
a✝ : ∀ (m : Nat), m < n✝ → Descendant 0 m
⊢ Descendant 0 n✝
Tactic:
rename_i i IH
Proof state after:
case ind
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
⊢ Descendant 0 i
Theorem: Algdata.BinaryHeap.Descendant.root
Proof state before:
case ind
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
⊢ Descendant 0 i
Tactic:
cases Nat.eq_zero_or_pos i with
| inl hz => cases hz; exact .refl 0
| inr hpos =>
  specialize IH ((i-1)/2) (gt_parent hpos)
  exact .trans IH (.parent i)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.root
Proof state before:
case ind.inl
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
hz : i = 0
⊢ Descendant 0 i
Tactic:
cases hz
Proof state after:
case ind.inl.refl
IH : ∀ (m : Nat), m < 0 → Descendant 0 m
⊢ Descendant 0 0
Theorem: Algdata.BinaryHeap.Descendant.root
Proof state before:
case ind.inl.refl
IH : ∀ (m : Nat), m < 0 → Descendant 0 m
⊢ Descendant 0 0
Tactic:
exact .refl 0
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.root
Proof state before:
case ind.inr
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
hpos : i > 0
⊢ Descendant 0 i
Tactic:
specialize IH ((i-1)/2) (gt_parent hpos)
Proof state after:
case ind.inr
i : Nat
hpos : i > 0
IH : Descendant 0 ((i - 1) / 2)
⊢ Descendant 0 i
Theorem: Algdata.BinaryHeap.Descendant.root
Proof state before:
case ind.inr
i : Nat
hpos : i > 0
IH : Descendant 0 ((i - 1) / 2)
⊢ Descendant 0 i
Tactic:
exact .trans IH (.parent i)
Proof state after:
no goals
Theorem: Subsemigroup.Prod.associated_iff
Proof state before:
M✝ : Type ?u.2605
N✝ : Type ?u.2608
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x z : M × N
⊢ Associated x z ↔ Associated x.1 z.1 ∧ Associated x.2 z.2
Tactic:
refine' ⟨fun ⟨u, hu⟩ => ⟨⟨(MulEquiv.prodUnits.toFun u).1, (Prod.eq_iff_fst_eq_snd_eq.1 hu).1⟩,
  ⟨(MulEquiv.prodUnits.toFun u).2, (Prod.eq_iff_fst_eq_snd_eq.1 hu).2⟩⟩, fun ⟨⟨u₁, h₁⟩, ⟨u₂, h₂⟩⟩ =>
    ⟨MulEquiv.prodUnits.invFun (u₁, u₂), Prod.eq_iff_fst_eq_snd_eq.2 ⟨h₁, h₂⟩⟩⟩
Proof state after:
no goals
Theorem: Subsemigroup.prod_of_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
⊢ ProdProperty s ∧ ProdProperty t → ProdProperty (prod s t)
Tactic:
rintro ⟨hs, ht⟩ x y hxy
Proof state after:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Theorem: Subsemigroup.prod_of_prodProperty
Proof state before:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Tactic:
obtain ⟨⟨z, hz, hz₂⟩, z', hz', hz'₂⟩ := hs x.1 y.1 hxy.1
Proof state after:
case intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
z : M
hz : z ∈ s
hz₂ : Associated x.1 z
z' : M
hz' : z' ∈ s
hz'₂ : Associated y.1 z'
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Theorem: Subsemigroup.prod_of_prodProperty
Proof state before:
case intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
z : M
hz : z ∈ s
hz₂ : Associated x.1 z
z' : M
hz' : z' ∈ s
hz'₂ : Associated y.1 z'
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Tactic:
obtain ⟨⟨w, hw, hw₂⟩, w', hw', hw'₂⟩ := ht x.2 y.2 hxy.2
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
z : M
hz : z ∈ s
hz₂ : Associated x.1 z
z' : M
hz' : z' ∈ s
hz'₂ : Associated y.1 z'
w : N
hw : w ∈ t
hw₂ : Associated x.2 w
w' : N
hw' : w' ∈ t
hw'₂ : Associated y.2 w'
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Theorem: Subsemigroup.prod_of_prodProperty
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Subsemigroup M
t : Subsemigroup N
hs : ProdProperty s
ht : ProdProperty t
x y : M × N
hxy : x * y ∈ prod s t
z : M
hz : z ∈ s
hz₂ : Associated x.1 z
z' : M
hz' : z' ∈ s
hz'₂ : Associated y.1 z'
w : N
hw : w ∈ t
hw₂ : Associated x.2 w
w' : N
hw' : w' ∈ t
hw'₂ : Associated y.2 w'
⊢ (∃ z ∈ prod s t, Associated x z) ∧ ∃ z ∈ prod s t, Associated y z
Tactic:
exact ⟨⟨(z, w), Subsemigroup.mem_prod.2 ⟨hz, hw⟩, Prod.associated_iff.2 ⟨hz₂, hw₂⟩⟩,
(z', w'), Subsemigroup.mem_prod.2 ⟨hz', hw'⟩, Prod.associated_iff.2 ⟨hz'₂, hw'₂⟩⟩
Proof state after:
no goals