ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>w : Nat<VAR>x : BitVec w<VAR>r i : Nat<GOAL>(x.rotateRight r).getLsb i = bif decide (i < w - r % w) then x.getLsb (r % w + i) else decide (i < w) && x.getLsb (i - (w - r % w))
<VAR>w i : Nat<GOAL>(BitVec.twoPow w i).toNat = 2 ^ i % 2 ^ w
<VAR>w : Nat<VAR>i j : Nat<GOAL>(BitVec.twoPow w i).getLsb j = (decide (i < w) && decide (i = j))
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<GOAL>x &&& BitVec.twoPow w i = if x.getLsb i = true then BitVec.twoPow w i else 0#w
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<GOAL>x * BitVec.twoPow w i = x <<< i
<VAR>p : Lean.Compiler.LCNF.Phase<GOAL>p ≤ p
<VAR>self : Lean.Compiler.LCNF.Pass<GOAL>self.phaseOut ≥ self.phase
<VAR>α : Type u_1<VAR>v : α<GOAL>Array.singleton v = #[v]
<VAR>α : Type u_1<VAR>a : Array α<GOAL>List.toArray a.data = a
<VAR>α : Type u_1<VAR>l : Array α<GOAL>l.data.length = l.size
<VAR>α : Type u_1<VAR>n : Nat<GOAL>Array.mkEmpty n = #[]
<VAR>α : Type u_1<VAR>as : List α<GOAL>(List.toArray as).size = as.length
<VAR>α : Type u_1<VAR>as : List α<GOAL>{ data := as }.size = as.length
<VAR>α : Type u_1<VAR>i : Nat<VAR>a : Array α<VAR>h : i < a.size<GOAL>a[i] = a.data[i]
<VAR>α : Type u_1<VAR>i : Nat<VAR>a : Array α<VAR>h : i < a.size<GOAL>a[i] = a.data.get ⟨i, h⟩
<VAR>m : Type u_1 → Type u_2<VAR>β : Type u_1<VAR>α : Type u_3<VAR>Monad m<VAR>f : β → α → m β<VAR>arr : Array α<VAR>i j : Nat<VAR>H : arr.size ≤ i + j<VAR>b : β<GOAL>Array.foldlM.loop f arr arr.size ⋯ i j b = List.foldlM f b (List.drop j arr.data)
<VAR>m : Type u_1 → Type u_2<VAR>β : Type u_1<VAR>α : Type u_3<VAR>Monad m<VAR>f : β → α → m β<VAR>init : β<VAR>arr : Array α<GOAL>Array.foldlM f init arr 0 = List.foldlM f init arr.data
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>f : β → α → β<VAR>init : β<VAR>arr : Array α<GOAL>Array.foldl f init arr 0 = List.foldl f init arr.data
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m β<VAR>arr : Array α<VAR>init : β<VAR>i : Nat<VAR>h : i ≤ arr.size<GOAL>List.foldlM (fun x y => f y x) init (List.take i arr.data).reverse = Array.foldrM.fold f arr 0 i h init
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m β<VAR>init : β<VAR>arr : Array α<GOAL>Array.foldrM f init arr arr.size = List.foldlM (fun x y => f y x) init arr.data.reverse
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m β<VAR>init : β<VAR>arr : Array α<GOAL>Array.foldrM f init arr arr.size = List.foldrM f init arr.data
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>init : β<VAR>arr : Array α<GOAL>Array.foldr f init arr arr.size = List.foldr f init arr.data
<VAR>α : Type u_1<VAR>arr : Array α<VAR>a : α<GOAL>(arr.push a).data = arr.data ++ [a]
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m β<VAR>init : β<VAR>arr : Array α<VAR>a : α<GOAL>Array.foldrM f init (arr.push a) (arr.push a).size = do let init ← f a init Array.foldrM f init arr arr.size
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m β<VAR>init : β<VAR>arr : Array α<VAR>a : α<GOAL>Array.foldrM f init (arr.push a) (arr.size + 1) = do let init ← f a init Array.foldrM f init arr arr.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>init : β<VAR>arr : Array α<VAR>a : α<GOAL>Array.foldr f init (arr.push a) (arr.push a).size = Array.foldr f (f a init) arr arr.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>init : β<VAR>arr : Array α<VAR>a : α<GOAL>Array.foldr f init (arr.push a) (arr.size + 1) = Array.foldr f (f a init) arr arr.size
<VAR>α : Type u_1<VAR>arr : Array α<VAR>l : List α<GOAL>arr.toListAppend l = arr.data ++ l
<VAR>α : Type u_1<VAR>arr : Array α<GOAL>arr.toList = arr.data
<VAR>α : Type u_1<VAR>arr : Array α<GOAL>arr.toListRev = arr.data.reverse
<VAR>α : Type u_1<VAR>a : Array α<VAR>x : α<VAR>i : Nat<VAR>h : i < a.size<GOAL>let_fun this := ⋯;
<VAR>α : Type u_1<VAR>a : Array α<VAR>x : α<GOAL>(a.push x)[a.size] = x
<VAR>α : Type u_1<VAR>a : Array α<VAR>x : α<VAR>i : Nat<VAR>h : i < (a.push x).size<GOAL>(a.push x)[i] = if h : i < a.size then a[i] else x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<VAR>arr : Array α<GOAL>Array.mapM f arr = Array.foldlM (fun bs a => bs.push <$> f a) #[] arr 0
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<VAR>arr : Array α<VAR>i : Nat<VAR>r : Array β<GOAL>Array.mapM.map f arr i r = List.foldlM (fun bs a => bs.push <$> f a) r (List.drop i arr.data)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>arr : Array α<GOAL>(Array.map f arr).data = List.map f arr.data
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>arr : Array α<GOAL>(Array.map f arr).size = arr.size
<VAR>α : Type u_1<VAR>arr : Array α<GOAL>arr.pop.data = arr.data.dropLast
<VAR>α : Type u_1<VAR>arr arr' : Array α<GOAL>arr.append arr' = arr ++ arr'
<VAR>α : Type u_1<VAR>arr arr' : Array α<GOAL>(arr ++ arr').data = arr.data ++ arr'.data
<VAR>α : Type u_1<VAR>arr : Array α<VAR>l : List α<GOAL>arr.appendList l = arr ++ l
<VAR>α : Type u_1<VAR>arr : Array α<VAR>l : List α<GOAL>(arr ++ l).data = arr.data ++ l
<VAR>α : Type u_1<VAR>arr : Array α<GOAL>arr ++ [] = arr
<VAR>α : Type u_1<VAR>arr : Array α<VAR>a : α<VAR>l : List α<GOAL>arr ++ a :: l = arr.push a ++ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>acc : Array β<VAR>F : Array β → α → Array β<VAR>G : α → List β<VAR>H : ∀ (acc : Array β) (a : α), (F acc a).data = acc.data ++ G a<GOAL>(List.foldl F acc l).data = acc.data ++ l.bind G
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>acc : Array β<VAR>G : α → β<GOAL>(List.foldl (fun acc a => acc.push (G a)) acc l).data = acc.data ++ List.map G l
<VAR>α : Type u_1<VAR>a : Array α<VAR>v : α<VAR>i : USize<VAR>h : i.toNat < a.size<GOAL>(a.uset i v h).size = a.size
<VAR>m : Type → Type u_1<VAR>α : Type u_2<VAR>Monad m<VAR>p : α → m Bool<VAR>as : Array α<VAR>start stop : Nat<GOAL>Array.anyM p as start stop = Array.anyM.loop p as (min stop as.size) ⋯ start
<VAR>m : Type → Type u_1<VAR>α : Type u_2<VAR>Monad m<VAR>p : α → m Bool<VAR>as : Array α<VAR>start stop : Nat<VAR>h : min stop as.size ≤ start<GOAL>Array.anyM p as start stop = pure false
<VAR>α : Type u_1<VAR>a : α<VAR>as : Array α<GOAL>a ∈ as ↔ a ∈ as.data
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<GOAL>a.get i = a[↑i]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>h : i < a.size<GOAL>a[i]? = some a[i]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>h : i ≥ a.size<GOAL>a[i]? = none
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<GOAL>a.get? i = a[i]?
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>h : a.size ≤ i<GOAL>a[i]? = none
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>d : α<GOAL>a[i]?.getD d = if p : i < a.size then a[i] else d
<VAR>α : Type u_1<VAR>a : Array α<VAR>n : Nat<VAR>d : α<GOAL>a.getD n d = a[n]?.getD d
<VAR>α : Type u_1<VAR>n : Nat<VAR>Inhabited α<VAR>a : Array α<GOAL>a.get! n = a.getD n default
<VAR>α : Type u_1<VAR>Inhabited α<VAR>a : Array α<VAR>i : Nat<GOAL>a.get! i = (a.get? i).getD default
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>v : α<VAR>j : Nat<VAR>eq : ↑i = j<VAR>p : j < (a.set i v).size<GOAL>(a.set i v)[j] = v
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>v : α<VAR>j : Nat<VAR>pj : j < (a.set i v).size<VAR>h : ↑i ≠ j<GOAL>(a.set i v)[j] = a[j]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>v : α<VAR>j : Nat<VAR>h : j < (a.set i v).size<GOAL>(a.set i v)[j] = if ↑i = j then v else a[j]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>v : α<GOAL>(a.set i v)[↑i]? = some v
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>j : Nat<VAR>v : α<VAR>ne : ↑i ≠ j<GOAL>(a.set i v)[j]? = a[j]?
<VAR>α : Type u_1<VAR>a : Array α<VAR>index : Nat<VAR>val : α<GOAL>(a.setD index val).size = a.size
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>v : α<VAR>h : i < (a.setD i v).size<GOAL>(a.setD i v)[i] = v
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>p : i < a.size<VAR>v : α<GOAL>(a.setD i v)[i]? = some v
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>v d : α<GOAL>(a.setD i v)[i]?.getD d = if i < a.size then v else d
<VAR>α : Type u_1<VAR>n : Nat<VAR>f : Fin n → α<VAR>i : Nat<VAR>acc : Array α<GOAL>(Array.ofFn.go f i acc).size = acc.size + (n - i)
<VAR>n : Nat<VAR>α : Type u_1<VAR>f : Fin n → α<GOAL>(Array.ofFn f).size = n
<VAR>n : Nat<VAR>α : Type u_1<VAR>f : Fin n → α<VAR>i : Nat<VAR>acc : Array α<VAR>k : Nat<VAR>hki : k < n<VAR>hin : i ≤ n<VAR>hi : i = acc.size<VAR>hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩<GOAL>(Array.ofFn.go f i acc)[k] = f ⟨k, hki⟩
<VAR>n : Nat<VAR>α : Type u_1<VAR>f : Fin n → α<VAR>i : Nat<VAR>h : i < (Array.ofFn f).size<GOAL>(Array.ofFn f)[i] = f ⟨i, ⋯⟩
<VAR>α : Type u_1<VAR>n : Nat<VAR>v : α<GOAL>(mkArray n v).data = List.replicate n v
<VAR>α : Type u_1<VAR>i : Nat<VAR>n : Nat<VAR>v : α<VAR>h : i < (mkArray n v).size<GOAL>(mkArray n v)[i] = v
<VAR>α : Type u_1<VAR>a : α<VAR>l : Array α<GOAL>a ∈ l.data ↔ a ∈ l
<VAR>α : Type u_1<VAR>a : α<GOAL>¬a ∈ #[]
<VAR>α : Type u_1<VAR>l : Array α<VAR>i : Fin l.size<GOAL>l[i] ∈ l
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.data.length<GOAL>a[i] = a.data.get i
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : USize<VAR>h : i.toNat < a.size<GOAL>a[i] = a[i.toNat]
<VAR>α : Type u_1<VAR>i : Nat<VAR>a : Array α<VAR>h : i < a.size<GOAL>a[i] ∈ a.data
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<GOAL>a[i]? = a.data.get? i
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<GOAL>a.get? i = a.data.get? i
<VAR>α : Type u_1<VAR>n : Nat<VAR>Inhabited α<VAR>a : Array α<GOAL>a.get! n = (a.get? n).getD default
<VAR>α : Type u_1<VAR>Inhabited α<VAR>a : Array α<GOAL>a.back = a.back?.getD default
<VAR>α : Type u_1<VAR>x : α<VAR>a : Array α<GOAL>(a.push x).back? = some x
<VAR>α : Type u_1<VAR>x : α<VAR>Inhabited α<VAR>a : Array α<GOAL>(a.push x).back = x
<VAR>α : Type u_1<VAR>a : Array α<VAR>x : α<VAR>i : Nat<VAR>h : i < a.size<GOAL>(a.push x)[i]? = some a[i]
<VAR>α : Type u_1<VAR>a : Array α<VAR>x : α<GOAL>(a.push x)[a.size]? = some x
<VAR>α : Type u_1<VAR>x : α<VAR>i : Nat<VAR>a : Array α<GOAL>(a.push x)[i]? = if i = a.size then some x else a[i]?
<VAR>α : Type u_1<VAR>a : Array α<GOAL>a[a.size]? = none
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>v : α<GOAL>(a.set i v).data = a.data.set (↑i) v
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>v : α<GOAL>(a.set i v)[↑i] = v
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>j : Nat<VAR>v : α<VAR>h : ↑i ≠ j<GOAL>(a.set i v)[j]? = a[j]?
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>j : Nat<VAR>v : α<GOAL>(a.set i v)[j]? = if ↑i = j then some v else a[j]?
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>j : Nat<VAR>hj : j < a.size<VAR>v : α<GOAL>(a.set i v)[j] = if ↑i = j then v else a[j]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>j : Nat<VAR>v : α<VAR>hj : j < a.size<VAR>h : ↑i ≠ j<GOAL>(a.set i v)[j] = a[j]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>v v' : α<GOAL>(a.set i v).set ⟨↑i, ⋯⟩ v' = a.set i v'
<VAR>n n' : Nat<VAR>e : n = n'<VAR>i : Fin n<GOAL>e ▸ i = ⟨↑i, ⋯⟩
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<GOAL>a.swap i j = (a.set i (a.get j)).set ⟨↑j, ⋯⟩ (a.get i)
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<GOAL>(a.swap i j).data = (a.data.set (↑i) (a.get j)).set (↑j) (a.get i)
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<VAR>k : Nat<GOAL>(a.swap i j)[k]? = if ↑j = k then some a[↑i] else if ↑i = k then some a[↑j] else a[k]?
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<VAR>v : α<GOAL>a.swapAt i v = (a[↑i], a.set i v)
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>v : α<VAR>h : i < a.size<GOAL>a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v)
<VAR>α : Type u_1<VAR>a : Array α<GOAL>a.pop.data = a.data.dropLast
<VAR>α : Type u_1<VAR>x : α<VAR>a : Array α<GOAL>(a.push x).pop = a
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>hi : i < a.pop.size<GOAL>a.pop[i] = a[i]
<VAR>α : Type u_1<VAR>as : Array α<VAR>h : as.size = 0<GOAL>as = #[]
<VAR>α : Type u_1<VAR>Inhabited α<VAR>as : Array α<VAR>h : as.size ≠ 0<GOAL>as = as.pop.push as.back
<VAR>α : Type u_1<VAR>as : Array α<VAR>h : as.size ≠ 0<GOAL>∃ bs c, as = bs.push c
<VAR>α : Type u_1<VAR>as : Array α<GOAL>as.size = as.data.length
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Nat<GOAL>(a.swap! i j).size = a.size
<VAR>α : Type u_1<VAR>as : Array α<VAR>i : Nat<VAR>j : Fin as.size<GOAL>(Array.reverse.loop as i j).size = as.size
<VAR>α : Type u_1<VAR>a : Array α<GOAL>a.reverse.size = a.size
<VAR>α : Type u_1<VAR>a as : Array α<VAR>i j : Nat<VAR>hj : j < as.size<VAR>h : i + j + 1 = a.size<VAR>h₂ : as.size = a.size<VAR>H : ∀ (k : Nat), as.data.get? k = if i ≤ k ∧ k ≤ j then a.data.get? k else a.data.reverse.get? k<VAR>k : Nat<GOAL>(Array.reverse.loop as i ⟨j, hj⟩).data.get? k = a.data.reverse.get? k
<VAR>α : Type u_1<VAR>a : Array α<GOAL>a.reverse.data = a.data.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>motive : Nat → β → Prop<VAR>f : β → α → β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])<VAR>i j : Nat<VAR>b : β<VAR>h₁ : j ≤ as.size<VAR>h₂ : as.size ≤ i + j<VAR>H : motive j b<GOAL>motive as.size (Array.foldlM.loop f as as.size ⋯ i j b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>motive : Nat → β → Prop<VAR>init : β<VAR>h0 : motive 0 init<VAR>f : β → α → β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])<GOAL>motive as.size (Array.foldl f init as 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>motive : Nat → β → Prop<VAR>f : α → β → β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)<VAR>i : Nat<VAR>b : β<VAR>hi : i ≤ as.size<VAR>H : motive i b<GOAL>motive 0 (Array.foldrM.fold f as 0 i hi b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>motive : Nat → β → Prop<VAR>init : β<VAR>h0 : motive as.size init<VAR>f : α → β → β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)<GOAL>motive 0 (Array.foldr f init as as.size)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>f : α → β<VAR>l : Array α<GOAL>b ∈ Array.map f l ↔ ∃ a, a ∈ l ∧ f a = b
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<VAR>arr : Array α<GOAL>Array.mapM f arr = do let __do_lift ← List.mapM f arr.data pure { data := __do_lift }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : Array β<VAR>as : Array α<VAR>f : α → β<VAR>i : Nat<GOAL>Array.mapM.map f as i b = Array.foldl (fun r a => r.push (f a)) b as i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>f : α → β<GOAL>Array.map f as = Array.foldl (fun r a => r.push (f a)) #[] as 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>f : α → β<VAR>motive : Nat → Prop<VAR>h0 : motive 0<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)<GOAL>motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (Array.map f as)[i]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>f : α → β<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), p i (f as[i])<GOAL>∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (Array.map f as)[i]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>as : Array α<VAR>i : Nat<VAR>h : i < (Array.map f as).size<GOAL>(Array.map f as)[i] = f as[i]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>f : Fin as.size → α → β<VAR>motive : Nat → Prop<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → p i (f i as[i]) ∧ motive (↑i + 1)<VAR>bs : Array β<VAR>i j : Nat<VAR>h : i + j = as.size<VAR>h₁ : j = bs.size<VAR>h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p ⟨i, h⟩ bs[i]<VAR>hm : motive j<GOAL>let arr := Array.mapIdxM.map as f i j h bs;
motive as.size ∧ ∃ eq, ∀ (i_1 : Nat) (h : i_1 < as.size), p ⟨i_1, h⟩ arr[i_1]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>f : Fin as.size → α → β<VAR>motive : Nat → Prop<VAR>h0 : motive 0<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → p i (f i as[i]) ∧ motive (↑i + 1)<GOAL>motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (as.mapIdx f)[i]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>f : Fin as.size → α → β<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), p i (f i as[i])<GOAL>∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (as.mapIdx f)[i]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : Array α<VAR>f : Fin a.size → α → β<GOAL>(a.mapIdx f).size = a.size
<VAR>α : Type u_1<VAR>as : Array α<GOAL>as.zipWithIndex.size = as.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : Array α<VAR>f : Fin a.size → α → β<VAR>i : Nat<VAR>h : i < (a.mapIdx f).size<GOAL>(a.mapIdx f)[i] = f ⟨i, ⋯⟩ a[i]
<VAR>α : Type u_1<VAR>f : α → α<VAR>arr : Array α<VAR>x i : Nat<VAR>h : i < arr.size<GOAL>(arr.modify x f).get ⟨i, ⋯⟩ = if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : Array α<GOAL>(Array.filter p l 0).data = List.filter p l.data
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>q : α → Bool<VAR>l : Array α<GOAL>Array.filter p (Array.filter q l 0) 0 = Array.filter (fun a => decide (p a = true ∧ q a = true)) l 0
<GOAL>∀ {α : Type u_1} {x : α} {p : α → Bool} {as : Array α}, x ∈ Array.filter p as 0 ↔ x ∈ as ∧ p x = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : Array α<VAR>h : a ∈ Array.filter p l 0<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>l : Array α<GOAL>(Array.filterMap f l 0).data = List.filterMap f l.data
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>l : Array α<VAR>b : β<GOAL>b ∈ Array.filterMap f l 0 ↔ ∃ a, a ∈ l ∧ f a = some b
<VAR>α : Type u_1<VAR>as : Array α<VAR>x : α<GOAL>as.push x = as ++ #[x]
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Array α<GOAL>a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>as bs : Array α<GOAL>(as ++ bs).size = as.size + bs.size
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : Array α<VAR>h : i < (as ++ bs).size<VAR>hlt : i < as.size<GOAL>(as ++ bs)[i] = as[i]
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : Array α<VAR>h : i < (as ++ bs).size<VAR>hle : as.size ≤ i<VAR>hlt : i - as.size < bs.size := ⋯<GOAL>(as ++ bs)[i] = bs[i - as.size]
<VAR>α : Type u_1<VAR>as : Array α<GOAL>as ++ #[] = as
<VAR>α : Type u_1<VAR>as : Array α<GOAL>#[] ++ as = as
<VAR>α : Type u_1<VAR>as bs cs : Array α<GOAL>as ++ bs ++ cs = as ++ (bs ++ cs)
<VAR>α : Type u_1<VAR>as bs : Array α<VAR>start : Nat<GOAL>Array.extract.loop as 0 start bs = bs
<VAR>α : Type u_1<VAR>as bs : Array α<VAR>size start : Nat<VAR>h : start < as.size<GOAL>Array.extract.loop as (size + 1) start bs = Array.extract.loop as size (start + 1) (bs.push as[start])
<VAR>α : Type u_1<VAR>as bs : Array α<VAR>size start : Nat<VAR>h : start ≥ as.size<GOAL>Array.extract.loop as size start bs = bs
<VAR>α : Type u_1<VAR>as bs : Array α<VAR>size start : Nat<GOAL>Array.extract.loop as size start bs = bs ++ Array.extract.loop as size start #[]
<VAR>α : Type u_1<VAR>as bs : Array α<VAR>size start : Nat<VAR>h : start + size ≤ as.size<GOAL>Array.extract.loop as size start bs = bs ++ as.extract start (start + size)
<VAR>α : Type u_1<VAR>as bs : Array α<VAR>size start : Nat<GOAL>(Array.extract.loop as size start bs).size = bs.size + min size (as.size - start)
<VAR>α : Type u_1<VAR>as : Array α<VAR>start stop : Nat<GOAL>(as.extract start stop).size = min stop as.size - start
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : Array α<VAR>size start : Nat<VAR>hlt : i < bs.size<GOAL>i < (Array.extract.loop as size start bs).size
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : Array α<VAR>size start : Nat<VAR>hlt : i < bs.size<VAR>h : i < (Array.extract.loop as size start bs).size := ⋯<GOAL>(Array.extract.loop as size start bs)[i] = bs[i]
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : Array α<VAR>size start : Nat<VAR>hge : i ≥ bs.size<VAR>h : i < (Array.extract.loop as size start bs).size<GOAL>start + i - bs.size < as.size
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : Array α<VAR>size start : Nat<VAR>hge : i ≥ bs.size<VAR>h : i < (Array.extract.loop as size start bs).size<VAR>h' : start + i - bs.size < as.size := ⋯<GOAL>(Array.extract.loop as size start bs)[i] = as[start + i - bs.size]
<VAR>α : Type u_1<VAR>i : Nat<VAR>as : Array α<VAR>start stop : Nat<VAR>h : i < (as.extract start stop).size<GOAL>start + i < as.size
<VAR>α : Type u_1<VAR>i : Nat<VAR>as : Array α<VAR>start stop : Nat<VAR>h : i < (as.extract start stop).size<GOAL>(as.extract start stop)[i] = as[start + i]
<VAR>α : Type u_1<VAR>as : Array α<GOAL>as.extract 0 as.size = as
<VAR>α : Type u_1<VAR>as : Array α<VAR>start stop : Nat<VAR>h : stop ≤ start<GOAL>as.extract start stop = #[]
<VAR>α : Type u_1<VAR>as : Array α<VAR>start stop : Nat<VAR>h : as.size ≤ start<GOAL>as.extract start stop = #[]
<VAR>α : Type u_1<VAR>start stop : Nat<GOAL>#[].extract start stop = #[]
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as : Array α<VAR>start stop : Nat<VAR>h : stop ≤ as.size<GOAL>Array.anyM.loop p as stop h start = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as : Array α<VAR>start stop : Nat<GOAL>as.any p start stop = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as : Array α<GOAL>as.any p 0 = true ↔ ∃ i, p as[i] = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as : Array α<GOAL>as.any p 0 = as.data.any p
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as : Array α<VAR>start stop : Nat<GOAL>as.all p start stop = !as.any (fun x => !p x) start stop
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as : Array α<VAR>start stop : Nat<GOAL>as.all p start stop = true ↔ ∀ (i : Fin as.size), start ≤ ↑i ∧ ↑i < stop → p as[i] = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as : Array α<GOAL>as.all p 0 = true ↔ ∀ (i : Fin as.size), p as[i] = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>as : Array α<GOAL>as.all p 0 = as.data.all p
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : Array α<GOAL>l.all p 0 = true ↔ ∀ (x : α), x ∈ l → p x = true
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>as : Array α<GOAL>as.contains a = true ↔ a ∈ as
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<GOAL>(a.swap i j)[↑j] = a[i]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<GOAL>(a.swap i j)[↑i] = a[j]
<VAR>α : Type u_1<VAR>p : Nat<VAR>a : Array α<VAR>i j : Fin a.size<VAR>hp : p < a.size<VAR>hi : p ≠ ↑i<VAR>hj : p ≠ ↑j<GOAL>(a.swap i j)[p] = a[p]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<VAR>k : Nat<VAR>hk : k < a.size<GOAL>(a.swap i j)[k] = if k = ↑i then a[j] else if k = ↑j then a[i] else a[k]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<VAR>k : Nat<VAR>hk' : k < (a.swap i j).size<GOAL>(a.swap i j)[k] = if k = ↑i then a[j] else if k = ↑j then a[i] else a[k]
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<GOAL>(a.swap i j).swap ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩ = a
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<GOAL>a.swap i j = a.swap j i
<VAR>α : Type u<VAR>lsize rsize : Nat<VAR>self : Lean.Diff.Histogram.Entry α lsize rsize<GOAL>self.leftCount = 0 ↔ self.leftIndex = none
<VAR>α : Type u<VAR>lsize rsize : Nat<VAR>self : Lean.Diff.Histogram.Entry α lsize rsize<GOAL>self.rightCount = 0 ↔ self.rightIndex = none
<VAR>α : Type u<VAR>β : Type v<VAR>data : Lean.HashMapBucket α β<VAR>i : USize<VAR>d : Lean.AssocList α β<VAR>h : i.toNat < data.val.size<GOAL>(data.update i d h).val.size = data.val.size
<VAR>α : Type u<VAR>data : Lean.HashSetBucket α<VAR>i : USize<VAR>d : List α<VAR>h : i.toNat < data.val.size<GOAL>(data.update i d h).val.size = data.val.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ks : Array α<VAR>vs : Array β<VAR>h : ks.size = vs.size<VAR>i : Fin ks.size<VAR>j : Fin vs.size<VAR>k : α<VAR>v : β<GOAL>(ks.set i k).size = (vs.set j v).size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ks : Array α<VAR>vs : Array β<VAR>h : ks.size = vs.size<VAR>k : α<VAR>v : β<GOAL>(ks.push k).size = (vs.push v).size
<VAR>α : Sort u_1<VAR>R : α → α → Prop<VAR>x y : α<VAR>hxy : x = y<VAR>h : R x x<GOAL>R x y
<VAR>xs : List Nat<GOAL>xs.nonzeroMinimum = 0 ↔ ∀ (x : Nat), x ∈ xs → x = 0
<VAR>xs : List Nat<VAR>w : xs.nonzeroMinimum ≠ 0<GOAL>xs.nonzeroMinimum ∈ xs
<VAR>a : Nat<VAR>xs : List Nat<VAR>m : a ∈ xs<VAR>h : a ≠ 0<GOAL>0 < xs.nonzeroMinimum
<VAR>a : Nat<VAR>xs : List Nat<VAR>m : a ∈ xs<VAR>h : a ≠ 0<GOAL>xs.nonzeroMinimum ≤ a