internlm/Lean-Github huggingface dataset:
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < bif p x[i] then i else findIdx.loop x p stop h (i + 1)
hpi : p x[i] = true
⊢ p x[k] = false
Tactic:
rewrite [hpi, cond_true] at hk'
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < i
hpi : p x[i] = true
⊢ p x[k] = false
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < i
hpi : p x[i] = true
⊢ p x[k] = false
Tactic:
exact absurd hk' <| Nat.not_lt_of_le hk
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < bif p x[i] then i else findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
⊢ p x[k] = false
Tactic:
rewrite [hpi, cond_false] at hk'
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
⊢ p x[k] = false
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
⊢ p x[k] = false
Tactic:
cases Nat.eq_or_lt_of_le hk with
| inl heq => exact heq ▸ hpi
| inr hlt => exact get_findIdx_loop_of_lt x p stop h (i+1) k hlt hk'
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
case inl
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
heq : i = k
⊢ p x[k] = false
Tactic:
exact heq ▸ hpi
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
case inr
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
hlt : i < k
⊢ p x[k] = false
Tactic:
exact get_findIdx_loop_of_lt x p stop h (i+1) k hlt hk'
Proof state after:
no goals
Theorem: SizedArray.findIdx_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ findIdx x p start stop ≤ n
Tactic:
dsimp [findIdx]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ n
Theorem: SizedArray.findIdx_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ n
Tactic:
if h : stop ≤ n then
  rewrite [dif_pos h]
  refine trans (r:=LE.le) ?_ h
  exact findIdx_loop_le x p stop h start
else
  rewrite [dif_neg h]
  exact findIdx_loop_le x p n .refl start
Proof state after:
no goals
Theorem: SizedArray.findIdx_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ n
Tactic:
rewrite [dif_pos h]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ n
Theorem: SizedArray.findIdx_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ n
Tactic:
refine trans (r:=LE.le) ?_ h
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ stop
Theorem: SizedArray.findIdx_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ stop
Tactic:
exact findIdx_loop_le x p stop h start
Proof state after:
no goals
Theorem: SizedArray.findIdx_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ n
Tactic:
rewrite [dif_neg h]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ findIdx.loop x p n (_ : Nat.le n n) start ≤ n
Theorem: SizedArray.findIdx_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ findIdx.loop x p n (_ : Nat.le n n) start ≤ n
Tactic:
exact findIdx_loop_le x p n .refl start
Proof state after:
no goals
Theorem: SizedArray.findIdx_le'
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ findIdx x p start stop ≤ stop
Tactic:
dsimp [findIdx]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ stop
Theorem: SizedArray.findIdx_le'
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ stop
Tactic:
if h : stop ≤ n then
  rewrite [dif_pos h]
  exact findIdx_loop_le x p stop h start
else
  rewrite [dif_neg h]
  refine trans (r:=LE.le) (s:=LE.le) ?_ <| Nat.le_of_lt <| Nat.lt_of_not_le h
  exact findIdx_loop_le x p n .refl start
Proof state after:
no goals
Theorem: SizedArray.findIdx_le'
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ stop
Tactic:
rewrite [dif_pos h]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ stop
Theorem: SizedArray.findIdx_le'
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ stop
Tactic:
exact findIdx_loop_le x p stop h start
Proof state after:
no goals
Theorem: SizedArray.findIdx_le'
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ stop
Tactic:
rewrite [dif_neg h]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ findIdx.loop x p n (_ : Nat.le n n) start ≤ stop
Theorem: SizedArray.findIdx_le'
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ findIdx.loop x p n (_ : Nat.le n n) start ≤ stop
Tactic:
refine trans (r:=LE.le) (s:=LE.le) ?_ <| Nat.le_of_lt <| Nat.lt_of_not_le h
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ findIdx.loop x p n (_ : Nat.le n n) start ≤ n
Theorem: SizedArray.findIdx_le'
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ findIdx.loop x p n (_ : Nat.le n n) start ≤ n
Tactic:
exact findIdx_loop_le x p n .refl start
Proof state after:
no goals
Theorem: SizedArray.findIdx_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ findIdx x p start stop ≥ start
Tactic:
dsimp [findIdx]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≥ start
Theorem: SizedArray.findIdx_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≥ start
Tactic:
rewrite [dif_pos h']
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ findIdx.loop x p stop h' start ≥ start
Theorem: SizedArray.findIdx_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ findIdx.loop x p stop h' start ≥ start
Tactic:
exact findIdx_loop_ge x p stop h' start h
Proof state after:
no goals
Theorem: SizedArray.get_findIdx
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : findIdx x p start stop < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
⊢ p x[findIdx x p start stop] = true
Tactic:
dsimp [findIdx] at h ⊢
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
⊢ p x[if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start] = true
Theorem: SizedArray.get_findIdx
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
⊢ p x[if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start] = true
Tactic:
if hstop : stop ≤ n then
  rewrite [getElem_eq rfl (dif_pos hstop)]
  rewrite [dif_pos hstop] at h
  exact get_findIdx_loop x p stop h' start h
else
  rewrite [getElem_eq rfl (dif_neg hstop)]
  rewrite [dif_neg hstop] at h
  exact get_findIdx_loop x p n .refl start <|
    trans (r:=LT.lt) (s:=LE.le) h h'
Proof state after:
no goals
Theorem: SizedArray.get_findIdx
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
⊢ p x[if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start] = true
Tactic:
rewrite [getElem_eq rfl (dif_pos hstop)]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
⊢ p x[findIdx.loop x p stop hstop start] = true
Theorem: SizedArray.get_findIdx
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
⊢ p x[findIdx.loop x p stop hstop start] = true
Tactic:
rewrite [dif_pos hstop] at h
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
h : findIdx.loop x p stop hstop start < stop
⊢ p x[findIdx.loop x p stop hstop start] = true
Theorem: SizedArray.get_findIdx
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
h : findIdx.loop x p stop hstop start < stop
⊢ p x[findIdx.loop x p stop hstop start] = true
Tactic:
exact get_findIdx_loop x p stop h' start h
Proof state after:
no goals
Theorem: SizedArray.get_findIdx
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : ¬stop ≤ n
⊢ p x[if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start] = true
Tactic:
rewrite [getElem_eq rfl (dif_neg hstop)]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : ¬stop ≤ n
⊢ p x[findIdx.loop x p n (_ : Nat.le n n) start] = true
Theorem: SizedArray.get_findIdx
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : ¬stop ≤ n
⊢ p x[findIdx.loop x p n (_ : Nat.le n n) start] = true
Tactic:
rewrite [dif_neg hstop] at h
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : findIdx.loop x p n (_ : Nat.le n n) start < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : ¬stop ≤ n
⊢ p x[findIdx.loop x p n (_ : Nat.le n n) start] = true
Theorem: SizedArray.get_findIdx
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : findIdx.loop x p n (_ : Nat.le n n) start < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : ¬stop ≤ n
⊢ p x[findIdx.loop x p n (_ : Nat.le n n) start] = true
Tactic:
exact get_findIdx_loop x p n .refl start <|
  trans (r:=LT.lt) (s:=LE.le) h h'
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < findIdx x p start stop
x✝ : k < n
⊢ p x[k] = false
Tactic:
dsimp [findIdx] at hk'
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
⊢ p x[k] = false
Theorem: SizedArray.get_findIdx_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
⊢ p x[k] = false
Tactic:
if hstop : stop ≤ n then
  rewrite [dif_pos hstop] at hk'
  exact get_findIdx_loop_of_lt x p stop hstop start k hk hk'
else
  rewrite [dif_neg hstop] at hk'
  exact get_findIdx_loop_of_lt x p n .refl start k hk hk'
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
hstop : stop ≤ n
⊢ p x[k] = false
Tactic:
rewrite [dif_pos hstop] at hk'
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
x✝ : k < n
hstop : stop ≤ n
hk' : k < findIdx.loop x p stop hstop start
⊢ p x[k] = false
Theorem: SizedArray.get_findIdx_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
x✝ : k < n
hstop : stop ≤ n
hk' : k < findIdx.loop x p stop hstop start
⊢ p x[k] = false
Tactic:
exact get_findIdx_loop_of_lt x p stop hstop start k hk hk'
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
hstop : ¬stop ≤ n
⊢ p x[k] = false
Tactic:
rewrite [dif_neg hstop] at hk'
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
hstop : ¬stop ≤ n
⊢ p x[k] = false
Theorem: SizedArray.get_findIdx_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
hstop : ¬stop ≤ n
⊢ p x[k] = false
Tactic:
exact get_findIdx_loop_of_lt x p n .refl start k hk hk'
Proof state after:
no goals
Theorem: SizedArray.findIdx_get_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
⊢ findIdx x p 0 n ≤ i
Tactic:
apply Nat.le_of_not_lt
Proof state after:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
⊢ ¬i < findIdx x p 0 n
Theorem: SizedArray.findIdx_get_le
Proof state before:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
⊢ ¬i < findIdx x p 0 n
Tactic:
intro h
Proof state after:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
h : i < findIdx x p 0 n
⊢ False
Theorem: SizedArray.findIdx_get_le
Proof state before:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
h : i < findIdx x p 0 n
⊢ False
Tactic:
have : p x[i] = false := get_findIdx_of_lt x p i i.zero_le h
Proof state after:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
h : i < findIdx x p 0 n
this : p x[i] = false
⊢ False
Theorem: SizedArray.findIdx_get_le
Proof state before:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
h : i < findIdx x p 0 n
this : p x[i] = false
⊢ False
Tactic:
rewrite [this] at hp
Proof state after:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : false = true
h : i < findIdx x p 0 n
this : p x[i] = false
⊢ False
Theorem: SizedArray.findIdx_get_le
Proof state before:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : false = true
h : i < findIdx x p 0 n
this : p x[i] = false
⊢ False
Tactic:
cases hp
Proof state after:
no goals
Theorem: SizedArray.zipWith_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ zipWith (cons a x) (cons b y) f = cons (f a b) (zipWith x y f)
Tactic:
unfold zipWith
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx (fun i => f (cons a x)[i]) (cons b y) = cons (f a b) (mapIdx (fun i => f x[i]) y)
Theorem: SizedArray.zipWith_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx (fun i => f (cons a x)[i]) (cons b y) = cons (f a b) (mapIdx (fun i => f x[i]) y)
Tactic:
rw [mapIdx_cons]
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ cons (f (cons a x)[{ val := 0, isLt := (_ : 0 < Nat.succ n) }] b) (mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) y) =
    cons (f a b) (mapIdx (fun i => f x[i]) y)
Theorem: SizedArray.zipWith_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ cons (f (cons a x)[{ val := 0, isLt := (_ : 0 < Nat.succ n) }] b) (mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) y) =
    cons (f a b) (mapIdx (fun i => f x[i]) y)
Tactic:
apply congrArg (cons (f a b))
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) y = mapIdx (fun i => f x[i]) y
Theorem: SizedArray.zipWith_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) y = mapIdx (fun i => f x[i]) y
Tactic:
apply congrFun
Proof state after:
case h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) = fun y => mapIdx (fun i => f x[i]) y
Theorem: SizedArray.zipWith_cons
Proof state before:
case h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ mapIdx ((fun i => f (cons a x)[i]) ∘ Fin.succ) = fun y => mapIdx (fun i => f x[i]) y
Tactic:
apply congrArg
Proof state after:
case h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ (fun i => f (cons a x)[i]) ∘ Fin.succ = fun i => f x[i]
Theorem: SizedArray.zipWith_cons
Proof state before:
case h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
⊢ (fun i => f (cons a x)[i]) ∘ Fin.succ = fun i => f x[i]
Tactic:
funext i
Proof state after:
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
i : Fin n
⊢ ((fun i => f (cons a x)[i]) ∘ Fin.succ) i = f x[i]
Theorem: SizedArray.zipWith_cons
Proof state before:
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
i : Fin n
⊢ ((fun i => f (cons a x)[i]) ∘ Fin.succ) i = f x[i]
Tactic:
cases i with | mk i h => rfl
Proof state after:
no goals
Theorem: SizedArray.zipWith_cons
Proof state before:
case h.h.h.mk
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
a : α
x : SizedArray α n
b : β
y : SizedArray β n
f : α → β → γ
i : Nat
h : i < n
⊢ ((fun i => f (cons a x)[i]) ∘ Fin.succ) { val := i, isLt := h } = f x[{ val := i, isLt := h }]
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.zipWith_push
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ zipWith (push x a) (push y b) f = push (zipWith x y f) (f a b)
Tactic:
unfold zipWith
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[i]) (push y b) = push (mapIdx (fun i => f x[i]) y) (f a b)
Theorem: SizedArray.zipWith_push
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[i]) (push y b) = push (mapIdx (fun i => f x[i]) y) (f a b)
Tactic:
rw [mapIdx_push]
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y)
      (f (push x a)[{ val := n, isLt := (_ : n < Nat.succ n) }] b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)
Theorem: SizedArray.zipWith_push
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y)
      (f (push x a)[{ val := n, isLt := (_ : n < Nat.succ n) }] b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)
Tactic:
conv =>
  lhs; arg 2
  change f ((push x a)[n]'n.lt_succ_self) b
  rw [get_push, dif_neg n.lt_irrefl]
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) (f a b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)