internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
case succ
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ lt y✝[j] y✝[i] = false
Tactic:
refine @IH h.popMax ?_ ?_
Proof state after:
case succ.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ n ≤ Subarray.size (BinaryHeap.popMax lt x)

case succ.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
case succ.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ n ≤ Subarray.size (BinaryHeap.popMax lt x)

case succ.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i
Tactic:
. exact size_popMax lt x ▸ Nat.le_sub_of_add_le hn
Proof state after:
case succ.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
case succ.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i
Tactic:
. rewrite [stop_popMax lt x this, Nat.sub_sub, Nat.add_comm]
  exact hi
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
case succ.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ n ≤ Subarray.size (BinaryHeap.popMax lt x)
Tactic:
exact size_popMax lt x ▸ Nat.le_sub_of_add_le hn
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
case succ.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i
Tactic:
rewrite [stop_popMax lt x this, Nat.sub_sub, Nat.add_comm]
Proof state after:
case succ.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ x.stop - (n + 1) ≤ i
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
case succ.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ x.stop - (n + 1) ≤ i
Tactic:
exact hi
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort_spec
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ lt (heapSort lt x)[j] (heapSort lt x)[i] = false
Tactic:
refine (heapSort.Intermed.mkHeap lt x).of_spec (.mk lt (mkHeap lt x) _) .refl i j ?_ hij ?_
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ (mkHeap lt x).stop - Subarray.size (mkHeap lt x) ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < (mkHeap lt x).stop
Theorem: Algdata.BinaryHeap.heapSort_spec
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ (mkHeap lt x).stop - Subarray.size (mkHeap lt x) ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < (mkHeap lt x).stop
Tactic:
all_goals simp only [size_mkHeap, stop_mkHeap]
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.stop - Subarray.size x ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Theorem: Algdata.BinaryHeap.heapSort_spec
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.stop - Subarray.size x ≤ i

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Tactic:
. simp only [Subarray.size, Nat.sub_sub_self x.h₁]
  exact hi
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Theorem: Algdata.BinaryHeap.heapSort_spec
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Tactic:
. exact hj
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort_spec
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < (mkHeap lt x).stop
Tactic:
simp only [size_mkHeap, stop_mkHeap]
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Theorem: Algdata.BinaryHeap.heapSort_spec
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.stop - Subarray.size x ≤ i
Tactic:
simp only [Subarray.size, Nat.sub_sub_self x.h₁]
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.start ≤ i
Theorem: Algdata.BinaryHeap.heapSort_spec
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.start ≤ i
Tactic:
exact hi
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort_spec
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ j < x.stop
Tactic:
exact hj
Proof state after:
no goals
Theorem: Matrix.get_set_eq
Proof state before:
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j : Fin c
v : α
⊢ get (set a i j v) i j = v
Tactic:
dsimp [get, set, Fin.cast, Fin.lexFold]
Proof state after:
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j : Fin c
v : α
⊢ (Array.set a.entry
        { val := ↑i * c + ↑j,
          isLt := (_ : ↑{ val := ↑i * c + ↑j, isLt := (_ : ↑i * c + ↑j < r * c) } < Array.size a.entry) }
        v)[↑i * c + ↑j] =
    v
Theorem: Matrix.get_set_eq
Proof state before:
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j : Fin c
v : α
⊢ (Array.set a.entry
        { val := ↑i * c + ↑j,
          isLt := (_ : ↑{ val := ↑i * c + ↑j, isLt := (_ : ↑i * c + ↑j < r * c) } < Array.size a.entry) }
        v)[↑i * c + ↑j] =
    v
Tactic:
rw [Array.get_set_eq a.entry]
Proof state after:
no goals
Theorem: Matrix.get_set_ne_row
Proof state before:
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ get (set a i₁ j v) i₂ j = get a i₂ j
Tactic:
apply Array.get_set_ne a.entry
Proof state after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ ↑(Fin.cast (_ : r * c = Array.size a.entry) (Fin.lexFold i₁ j)) ≠
    ↑(Fin.cast (_ : r * c = Array.size (set a i₁ j v).entry) (Fin.lexFold i₂ j))
Theorem: Matrix.get_set_ne_row
Proof state before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ ↑(Fin.cast (_ : r * c = Array.size a.entry) (Fin.lexFold i₁ j)) ≠
    ↑(Fin.cast (_ : r * c = Array.size (set a i₁ j v).entry) (Fin.lexFold i₂ j))
Tactic:
dsimp
Proof state after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ ¬↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
Theorem: Matrix.get_set_ne_row
Proof state before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
⊢ ¬↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
Tactic:
intro hcontra
Proof state after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
hcontra : ↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
⊢ False
Theorem: Matrix.get_set_ne_row
Proof state before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
hcontra : ↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
⊢ False
Tactic:
have := Fin.lexFold_inj (Fin.eq_of_val_eq hcontra)
Proof state after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
hcontra : ↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
this : i₁ = i₂ ∧ j = j
⊢ False
Theorem: Matrix.get_set_ne_row
Proof state before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i₁ i₂ : Fin r
h : i₁ ≠ i₂
j : Fin c
v : α
hcontra : ↑(Fin.lexFold i₁ j) = ↑(Fin.lexFold i₂ j)
this : i₁ = i₂ ∧ j = j
⊢ False
Tactic:
exact absurd this.left h
Proof state after:
no goals
Theorem: Matrix.get_set_ne_col
Proof state before:
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
⊢ get (set a i j₁ v) i j₂ = get a i j₂
Tactic:
apply Array.get_set_ne a.entry
Proof state after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
⊢ ↑(Fin.cast (_ : r * c = Array.size a.entry) (Fin.lexFold i j₁)) ≠
    ↑(Fin.cast (_ : r * c = Array.size (set a i j₁ v).entry) (Fin.lexFold i j₂))
Theorem: Matrix.get_set_ne_col
Proof state before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
⊢ ↑(Fin.cast (_ : r * c = Array.size a.entry) (Fin.lexFold i j₁)) ≠
    ↑(Fin.cast (_ : r * c = Array.size (set a i j₁ v).entry) (Fin.lexFold i j₂))
Tactic:
dsimp
Proof state after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
⊢ ¬↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
Theorem: Matrix.get_set_ne_col
Proof state before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
⊢ ¬↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
Tactic:
intro hcontra
Proof state after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
hcontra : ↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
⊢ False
Theorem: Matrix.get_set_ne_col
Proof state before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
hcontra : ↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
⊢ False
Tactic:
have := Fin.lexFold_inj (Fin.eq_of_val_eq hcontra)
Proof state after:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
hcontra : ↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
this : i = i ∧ j₁ = j₂
⊢ False
Theorem: Matrix.get_set_ne_col
Proof state before:
case h
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j₁ j₂ : Fin c
h : j₁ ≠ j₂
v : α
hcontra : ↑(Fin.lexFold i j₁) = ↑(Fin.lexFold i j₂)
this : i = i ∧ j₁ = j₂
⊢ False
Tactic:
exact absurd this.right h
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.lt_child_left
Proof state before:
i : Nat
⊢ i < 2 * i + 1
Tactic:
rewrite [Nat.two_mul]
Proof state after:
i : Nat
⊢ i < i + i + 1
Theorem: Algdata.BinaryHeap.lt_child_left
Proof state before:
i : Nat
⊢ i < i + i + 1
Tactic:
exact Nat.succ_le_succ (i.le_add_left i)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.induction_on
Proof state before:
k : Nat
motive : (i : Nat) → Descendant i k → Prop
i : Nat
h : Descendant i k
refl : motive k (_ : Descendant k k)
node_left : ∀ (i : Nat) (h : Descendant (2 * i + 1) k), motive (2 * i + 1) h → motive i (_ : Descendant i k)
node_right : ∀ (i : Nat) (h : Descendant (2 * i + 2) k), motive (2 * i + 2) h → motive i (_ : Descendant i k)
⊢ motive i h
Tactic:
induction h with
| refl i => exact refl
| node_left i h IH =>
  exact node_left i h <| IH refl node_left node_right
| node_right i h IH =>
  exact node_right i h <| IH refl node_left node_right
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.induction_on
Proof state before:
case refl
k i✝ i : Nat
motive : (i_1 : Nat) → Descendant i_1 i → Prop
refl : motive i (_ : Descendant i i)
node_left : ∀ (i_1 : Nat) (h : Descendant (2 * i_1 + 1) i), motive (2 * i_1 + 1) h → motive i_1 (_ : Descendant i_1 i)
node_right : ∀ (i_1 : Nat) (h : Descendant (2 * i_1 + 2) i), motive (2 * i_1 + 2) h → motive i_1 (_ : Descendant i_1 i)
⊢ motive i (_ : Descendant i i)
Tactic:
exact refl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.induction_on
Proof state before:
case node_left
k i✝ i k✝ : Nat
h : Descendant (2 * i + 1) k✝
IH :
  ∀ {motive : (i : Nat) → Descendant i k✝ → Prop},
    motive k✝ (_ : Descendant k✝ k✝) →
      (∀ (i : Nat) (h : Descendant (2 * i + 1) k✝), motive (2 * i + 1) h → motive i (_ : Descendant i k✝)) →
        (∀ (i : Nat) (h : Descendant (2 * i + 2) k✝), motive (2 * i + 2) h → motive i (_ : Descendant i k✝)) →
          motive (2 * i + 1) h
motive : (i : Nat) → Descendant i k✝ → Prop
refl : motive k✝ (_ : Descendant k✝ k✝)
node_left : ∀ (i : Nat) (h : Descendant (2 * i + 1) k✝), motive (2 * i + 1) h → motive i (_ : Descendant i k✝)
node_right : ∀ (i : Nat) (h : Descendant (2 * i + 2) k✝), motive (2 * i + 2) h → motive i (_ : Descendant i k✝)
⊢ motive i (_ : Descendant i k✝)
Tactic:
exact node_left i h <| IH refl node_left node_right
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.induction_on
Proof state before:
case node_right
k i✝ i k✝ : Nat
h : Descendant (2 * i + 2) k✝
IH :
  ∀ {motive : (i : Nat) → Descendant i k✝ → Prop},
    motive k✝ (_ : Descendant k✝ k✝) →
      (∀ (i : Nat) (h : Descendant (2 * i + 1) k✝), motive (2 * i + 1) h → motive i (_ : Descendant i k✝)) →
        (∀ (i : Nat) (h : Descendant (2 * i + 2) k✝), motive (2 * i + 2) h → motive i (_ : Descendant i k✝)) →
          motive (2 * i + 2) h
motive : (i : Nat) → Descendant i k✝ → Prop
refl : motive k✝ (_ : Descendant k✝ k✝)
node_left : ∀ (i : Nat) (h : Descendant (2 * i + 1) k✝), motive (2 * i + 1) h → motive i (_ : Descendant i k✝)
node_right : ∀ (i : Nat) (h : Descendant (2 * i + 2) k✝), motive (2 * i + 2) h → motive i (_ : Descendant i k✝)
⊢ motive i (_ : Descendant i k✝)
Tactic:
exact node_right i h <| IH refl node_left node_right
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
i : Nat
⊢ Descendant ((i - 1) / 2) i
Tactic:
cases i with
| zero => exact .refl 0
| succ i =>
  rewrite [Nat.succ_sub_one, Nat.succ_eq_add_one]
  conv => rhs; rewrite [← Nat.div_add_mod i 2]
  cases i.mod_two_eq_zero_or_one with
  | inl hi_even =>
    rewrite [hi_even, Nat.add_zero]; exact .child_left _
  | inr hi_odd =>
    rewrite [hi_odd]; exact .child_right _
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
case zero

⊢ Descendant ((Nat.zero - 1) / 2) Nat.zero
Tactic:
exact .refl 0
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
case succ
i : Nat
⊢ Descendant ((Nat.succ i - 1) / 2) (Nat.succ i)
Tactic:
rewrite [Nat.succ_sub_one, Nat.succ_eq_add_one]
Proof state after:
case succ
i : Nat
⊢ Descendant (i / 2) (i + 1)
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
case succ
i : Nat
⊢ Descendant (i / 2) (i + 1)
Tactic:
conv => rhs; rewrite [← Nat.div_add_mod i 2]
Proof state after:
case succ
i : Nat
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
case succ
i : Nat
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)
Tactic:
cases i.mod_two_eq_zero_or_one with
| inl hi_even =>
  rewrite [hi_even, Nat.add_zero]; exact .child_left _
| inr hi_odd =>
  rewrite [hi_odd]; exact .child_right _
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
case succ.inl
i : Nat
hi_even : i % 2 = 0
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)
Tactic:
rewrite [hi_even, Nat.add_zero]
Proof state after:
case succ.inl
i : Nat
hi_even : i % 2 = 0
⊢ Descendant (i / 2) (2 * (i / 2) + 1)
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
case succ.inl
i : Nat
hi_even : i % 2 = 0
⊢ Descendant (i / 2) (2 * (i / 2) + 1)
Tactic:
exact .child_left _
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
case succ.inr
i : Nat
hi_odd : i % 2 = 1
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)
Tactic:
rewrite [hi_odd]
Proof state after:
case succ.inr
i : Nat
hi_odd : i % 2 = 1
⊢ Descendant (i / 2) (2 * (i / 2) + 1 + 1)
Theorem: Algdata.BinaryHeap.Descendant.parent
Proof state before:
case succ.inr
i : Nat
hi_odd : i % 2 = 1
⊢ Descendant (i / 2) (2 * (i / 2) + 1 + 1)
Tactic:
exact .child_right _
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.trans
Proof state before:
i j k : Nat
hij : Descendant i j
hjk : Descendant j k
⊢ Descendant i k
Tactic:
induction hij with
| refl => exact hjk
| node_left i _ IH => exact .node_left i IH
| node_right i _ IH => exact .node_right i IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.trans
Proof state before:
case refl
i j k : Nat
hjk : Descendant j k
⊢ Descendant j k
Tactic:
exact hjk
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.trans
Proof state before:
case node_left
i✝ j k : Nat
hjk : Descendant j k
i : Nat
h✝ : Descendant (2 * i + 1) j
IH : Descendant (2 * i + 1) k
⊢ Descendant i k
Tactic:
exact .node_left i IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.trans
Proof state before:
case node_right
i✝ j k : Nat
hjk : Descendant j k
i : Nat
h✝ : Descendant (2 * i + 2) j
IH : Descendant (2 * i + 2) k
⊢ Descendant i k
Tactic:
exact .node_right i IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof state before:
i : Nat
⊢ ¬Descendant (2 * i + 1) (2 * i + 2)
Tactic:
intro h
Proof state after:
i : Nat
h : Descendant (2 * i + 1) (2 * i + 2)
⊢ False
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof state before:
i : Nat
h : Descendant (2 * i + 1) (2 * i + 2)
⊢ False
Tactic:
generalize hn : 2*i+1 = n at h
Proof state after:
i n : Nat
hn : 2 * i + 1 = n
h : Descendant n (2 * i + 2)
⊢ False
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof 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
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.Descendant.sibling_not
Proof state before:
case refl
i : Nat
hn : 2 * i + 1 = 2 * i + 2
⊢ False
Tactic:
cases Nat.add_left_cancel hn
Proof state after:
no goals