ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<GOAL>∀ {α : Type u_1} {l₂ l l₁ : List α}, l₂ ⊆ l → l₁.Disjoint l → l₁.Disjoint l₂
<GOAL>∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Disjoint l₂ → l₁.Disjoint l₂
<GOAL>∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₁.Disjoint (a :: l₂) → l₁.Disjoint l₂
<GOAL>∀ {α : Type u_1} {a : α} {l : List α}, [a].Disjoint l ↔ ¬a ∈ l
<GOAL>∀ {α : Type u_1} {l : List α} {a : α}, l.Disjoint [a] ↔ ¬a ∈ l
<GOAL>∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l ↔ l₁.Disjoint l ∧ l₂.Disjoint l
<GOAL>∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) ↔ l.Disjoint l₁ ∧ l.Disjoint l₂
<GOAL>∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Disjoint l₂ ↔ ¬a ∈ l₂ ∧ l₁.Disjoint l₂
<GOAL>∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁.Disjoint (a :: l₂) ↔ ¬a ∈ l₁ ∧ l₁.Disjoint l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l → l₁.Disjoint l
<GOAL>∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l → l₂.Disjoint l
<GOAL>∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) → l.Disjoint l₁
<GOAL>∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) → l.Disjoint l₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β : Type u_3<VAR>f : α₁ → α₂<VAR>g₁ : α₁ → β → α₁<VAR>g₂ : α₂ → β → α₂<VAR>l : List β<VAR>init : α₁<VAR>H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)<GOAL>List.foldl g₂ (f init) l = f (List.foldl g₁ init l)
<VAR>β₁ : Type u_1<VAR>β₂ : Type u_2<VAR>α : Type u_3<VAR>f : β₁ → β₂<VAR>g₁ : α → β₁ → β₁<VAR>g₂ : α → β₂ → β₂<VAR>l : List α<VAR>init : β₁<VAR>H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)<GOAL>List.foldr g₂ (f init) l = f (List.foldr g₁ init l)
<VAR>α : Type u_1<VAR>BEq α<VAR>l₁ l₂ : List α<GOAL>l₁ ∪ l₂ = List.foldr List.insert l₂ l₁
<VAR>α : Type u_1<VAR>BEq α<VAR>l : List α<GOAL>[] ∪ l = l
<VAR>α : Type u_1<VAR>BEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a :: l₁ ∪ l₂ = List.insert a (l₁ ∪ l₂)
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>x : α<VAR>l₁ l₂ : List α<GOAL>x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>l₁ l₂ : List α<GOAL>l₁ ∩ l₂ = List.filter (fun x => List.elem x l₂) l₁
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>x : α<VAR>l₁ l₂ : List α<GOAL>x ∈ l₁ ∩ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs : List α<VAR>ys : List β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ xs.product ys ↔ x ∈ xs ∧ y ∈ ys
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>(List.leftpad n a l).length = max n l.length
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>List.replicate (n - l.length) a <+: List.leftpad n a l
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>l <:+ List.leftpad n a l
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<GOAL>List.forIn = forIn
<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 (ForInStep β)<VAR>l : List α<VAR>init : β<GOAL>forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>Monad m<VAR>LawfulMonad m<VAR>l₁ l₂ : List α<VAR>f : α → m PUnit<GOAL>(l₁ ++ l₂).forM f = do l₁.forM f l₂.forM f
<VAR>α : Type u_1<VAR>BEq α<VAR>l : List α<GOAL>l.diff [] = l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>l₁.diff (a :: l₂) = (l₁.erase a).diff l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>l₁.diff (a :: l₂) = (l₁.diff l₂).erase a
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>(l₁.diff l₂).erase a = (l₁.erase a).diff l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l : List α<GOAL>[].diff l = []
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l₂ : List α<VAR>h : a ∈ l₂<VAR>l₁ : List α<GOAL>(a :: l₁).diff l₂ = l₁.diff (l₂.erase a)
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l₂ : List α<VAR>h : ¬a ∈ l₂<VAR>l₁ : List α<GOAL>(a :: l₁).diff l₂ = a :: l₁.diff l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ : List α<GOAL>l₁.diff l₂ = List.foldl List.erase l₁ l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ l₃ : List α<GOAL>l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ : List α<GOAL>l₁.diff l₂ <+ l₁
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ : List α<GOAL>l₁.diff l₂ ⊆ l₁
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a ∈ l₁ → ¬a ∈ l₂ → a ∈ l₁.diff l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ l₃ : List α<GOAL>l₁ <+ l₂ → l₁.diff l₃ <+ l₂.diff l₃
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>l₁ <+ l₂ → (l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <+: l₁ ++ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₂ <:+ l₁ ++ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁ <:+: l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁ <:+: l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>[] <+: l
<VAR>α : Type u_1<VAR>l : List α<GOAL>[] <:+ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>[] <:+: l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l <+: l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l <:+ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l <:+: l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>l <:+ a :: l
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂ → l₁ <:+: a :: l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂ → l₁ <:+: l₂.concat a
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<GOAL>l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<GOAL>l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<GOAL>l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁ <+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁ ⊆ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁ <+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁ ⊆ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁ <+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁ ⊆ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <:+ l₂.reverse ↔ l₁ <+: l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <:+: l₂.reverse ↔ l₁ <:+: l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.length ≤ l₂.length
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.length ≤ l₂.length
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.length ≤ l₂.length
<GOAL>∀ {α : Type u_1} {l : List α}, l <:+: [] ↔ l = []
<GOAL>∀ {α : Type u_1} {l : List α}, l <+: [] ↔ l = []
<GOAL>∀ {α : Type u_1} {l : List α}, l <:+ [] ↔ l = []
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.length = l₂.length → l₁ = l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.length = l₂.length → l₁ = l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.length = l₂.length → l₁ = l₂
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<GOAL>l₁ <+: l₃ → l₂ <+: l₃ → l₁.length ≤ l₂.length → l₁ <+: l₂
<GOAL>∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → l₁ <+: l₂ ∨ l₂ <+: l₁
<GOAL>∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃ → l₂ <:+ l₃ → l₁.length ≤ l₂.length → l₁ <:+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃ → l₂ <:+ l₃ → l₁ <:+ l₂ ∨ l₂ <:+ l₁
<GOAL>∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂
<GOAL>∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂
<VAR>α : Type u_1<VAR>l : List α<VAR>L : List (List α)<GOAL>l ∈ L → l <:+: L.join
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.take n l <+: l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.drop n l <:+ l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.take n l <+ l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.drop n l <+ l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.take n l ⊆ l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.drop n l ⊆ l
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<VAR>h : a ∈ List.take n l<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>h : l₁ <+: l₂<GOAL>List.filter p l₁ <+: List.filter p l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>h : l₁ <:+ l₂<GOAL>List.filter p l₁ <:+ List.filter p l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>h : l₁ <:+: l₂<GOAL>List.filter p l₁ <:+: List.filter p l₂
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<VAR>h : a ∈ List.drop n l<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>m n : Nat<VAR>l : List α<GOAL>l.Nodup → m ≤ n → (List.take m l).Disjoint (List.drop n l)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>a b : α<VAR>l : List α<GOAL>List.Chain R a (b :: l) ↔ R a b ∧ List.Chain R b l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>p : List.Chain R a (b :: l)<GOAL>R a b
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>p : List.Chain R a (b :: l)<GOAL>List.Chain R b l
<VAR>α : Type u_1<VAR>R S : α → α → Prop<VAR>HRS : ∀ ⦃a b : α⦄, R a b → S a b<VAR>a b : α<VAR>Hab : ∀ ⦃c : α⦄, R a c → S b c<VAR>l : List α<VAR>p : List.Chain R a l<GOAL>List.Chain S b l
<VAR>α : Type u_1<VAR>R S : α → α → Prop<VAR>H : ∀ (a b : α), R a b → S a b<VAR>a : α<VAR>l : List α<VAR>p : List.Chain R a l<GOAL>List.Chain S a l
<GOAL>∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α}, List.Pairwise R (a :: l) → List.Chain R a l
<VAR>s n step : Nat<GOAL>List.range' s (n + 1) step = s :: List.range' (s + step) n step
<VAR>s step n : Nat<GOAL>(List.range' s n step).length = n
<VAR>s n step : Nat<GOAL>List.range' s n step = [] ↔ n = 0
<VAR>m s step n : Nat<GOAL>m ∈ List.range' s n step ↔ ∃ i, i < n ∧ m = s + step * i
<VAR>m s n : Nat<GOAL>m ∈ List.range' s n ↔ s ≤ m ∧ m < s + n
<VAR>a s n step : Nat<GOAL>List.map (fun x => a + x) (List.range' s n step) = List.range' (a + s) n step
<VAR>step : Nat<VAR>a s n : Nat<VAR>h : a ≤ s<GOAL>List.map (fun x => x - a) (List.range' s n step) = List.range' (s - a) n step
<VAR>s n step : Nat<GOAL>List.Chain (fun a b => b = a + step) s (List.range' (s + step) n step)
<VAR>s n : Nat<VAR>step : Nat<VAR>h : 0 < step<GOAL>List.Chain (fun x x_1 => x < x_1) s (List.range' (s + step) n step)
<VAR>s m n step : Nat<GOAL>List.range' s m step ++ List.range' (s + step * m) n step = List.range' s (n + m) step
<VAR>s m n : Nat<GOAL>List.range' s m ++ List.range' (s + m) n = List.range' s (n + m)
<VAR>step s m n : Nat<GOAL>List.range' s m step <+ List.range' s n step ↔ m ≤ n
<VAR>step s m n : Nat<VAR>step0 : 0 < step<GOAL>List.range' s m step ⊆ List.range' s n step ↔ m ≤ n
<VAR>s m n : Nat<GOAL>List.range' s m ⊆ List.range' s n ↔ m ≤ n
<VAR>s step : Nat<VAR>m n : Nat<GOAL>m < n → (List.range' s n step)[m]? = some (s + step * m)
<VAR>n m step : Nat<VAR>i : Nat<VAR>H : i < (List.range' n m step).length<GOAL>(List.range' n m step)[i] = n + step * i
<VAR>s step : Nat<VAR>m n : Nat<VAR>h : m < n<GOAL>(List.range' s n step).get? m = some (s + step * m)
<VAR>n m step : Nat<VAR>i : Nat<VAR>H : i < (List.range' n m step).length<GOAL>(List.range' n m step).get ⟨i, H⟩ = n + step * i
<VAR>step : Nat<VAR>s n : Nat<GOAL>List.range' s (n + 1) step = List.range' s n step ++ [s + step * n]
<VAR>s n : Nat<GOAL>List.range' s (n + 1) = List.range' s n ++ [s + n]
<VAR>s n : Nat<GOAL>List.range.loop s (List.range' s n) = List.range' 0 (n + s)
<VAR>n : Nat<GOAL>List.range n = List.range' 0 n
<VAR>n : Nat<GOAL>List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)
<VAR>s n : Nat<GOAL>List.range' s n = List.map (fun x => s + x) (List.range n)
<VAR>n : Nat<GOAL>List.range n = [] ↔ n = 0
<VAR>m n : Nat<GOAL>List.range m <+ List.range n ↔ m ≤ n
<VAR>m n : Nat<GOAL>List.range m ⊆ List.range n ↔ m ≤ n
<VAR>m n : Nat<GOAL>m ∈ List.range n ↔ m < n
<VAR>n : Nat<GOAL>¬n ∈ List.range n
<VAR>n : Nat<GOAL>n ∈ List.range (n + 1)
<VAR>m n : Nat<VAR>h : m < n<GOAL>(List.range n)[m]? = some m
<VAR>n : Nat<VAR>m : Nat<VAR>h : m < (List.range n).length<GOAL>(List.range n)[m] = m
<VAR>m n : Nat<VAR>h : m < n<GOAL>(List.range n).get? m = some m
<VAR>n : Nat<VAR>i : Nat<VAR>H : i < (List.range n).length<GOAL>(List.range n).get ⟨i, H⟩ = i
<VAR>n : Nat<GOAL>List.range n.succ = List.range n ++ [n]
<VAR>a b : Nat<GOAL>List.range (a + b) = List.range a ++ List.map (fun x => a + x) (List.range b)
<VAR>n : Nat<GOAL>List.iota n = (List.range' 1 n).reverse
<VAR>n : Nat<GOAL>(List.iota n).length = n
<VAR>m n : Nat<GOAL>m ∈ List.iota n ↔ 1 ≤ m ∧ m ≤ n
<VAR>s n : Nat<GOAL>(List.range' s n).reverse = List.map (fun x => s + n - 1 - x) (List.range n)
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.map Prod.fst (List.enumFrom n l) = List.range' n l.length
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.map Prod.fst l.enum = List.range l.length
<VAR>α : Type u_1<VAR>xs : List α<GOAL>∀ {α_1 : Sort u_2} {f : Nat → α → α_1 → α_1} {i : α_1} {s : Nat}, List.foldrIdx f i xs s = List.foldrIdx (fun i => f (i + s)) i xs
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<GOAL>∀ {α_1 : Sort u_2} {f : Nat → α → α_1 → α_1} {i : α_1} {s : Nat}, List.foldrIdx f i (x :: xs) s = f s x (List.foldrIdx f i xs (s + 1))
<VAR>α : Type u_1<VAR>xs : List α<VAR>s : Nat<VAR>p : α → Bool<GOAL>List.foldrIdx (fun i a is => if p a = true then (i + 1) :: is else is) [] xs s = List.map (fun x => x + 1) (List.foldrIdx (fun i a is => if p a = true then i :: is else is) [] xs s)
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>p : α → Bool<GOAL>List.findIdxs p (x :: xs) = bif p x then 0 :: List.map (fun x => x + 1) (List.findIdxs p xs) else List.map (fun x => x + 1) (List.findIdxs p xs)
<VAR>α : Type u_1<VAR>x : α<VAR>BEq α<GOAL>List.indexesOf x [] = []
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>y : α<VAR>BEq α<GOAL>List.indexesOf y (x :: xs) = bif x == y then 0 :: List.map (fun x => x + 1) (List.indexesOf y xs) else List.map (fun x => x + 1) (List.indexesOf y xs)
<VAR>α : Type u_1<VAR>x : α<VAR>BEq α<GOAL>List.indexOf x [] = 0
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>y : α<VAR>BEq α<GOAL>List.indexOf y (x :: xs) = bif x == y then 0 else List.indexOf y xs + 1
<VAR>α : Type u_1<VAR>x : α<VAR>BEq α<VAR>LawfulBEq α<VAR>xs : List α<VAR>m : x ∈ xs<GOAL>List.indexOf x xs ∈ List.indexesOf x xs
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>r t : List α<GOAL>List.merge.loop s [] r t = t.reverseAux r
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>l t : List α<GOAL>List.merge.loop s l [] t = t.reverseAux l
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>l r t : List α<GOAL>List.merge.loop s l r t = t.reverseAux (List.merge s l r)
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>l : List α<GOAL>List.merge s l [] = l
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>r : List α<GOAL>List.merge s [] r = r
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>a b : α<VAR>l r : List α<GOAL>List.merge s (a :: l) (b :: r) = if s a b = true then a :: List.merge s l (b :: r) else b :: List.merge s (a :: l) r
<VAR>α : Type u_1<VAR>a b : α<VAR>s : α → α → Bool<VAR>l r : List α<VAR>h : s a b = true<GOAL>List.merge s (a :: l) (b :: r) = a :: List.merge s l (b :: r)
<VAR>α : Type u_1<VAR>a b : α<VAR>s : α → α → Bool<VAR>l r : List α<VAR>h : ¬s a b = true<GOAL>List.merge s (a :: l) (b :: r) = b :: List.merge s (a :: l) r
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>l r : List α<GOAL>(List.merge s l r).length = l.length + r.length
<VAR>α : Type u_1<VAR>x : α<VAR>l r : List α<VAR>s : α → α → Bool<GOAL>x ∈ List.merge s l r ↔ x ∈ l ∨ x ∈ r
<VAR>α : Type u_1<VAR>x : α<VAR>l r : List α<VAR>s : α → α → Bool<VAR>h : x ∈ l<GOAL>x ∈ List.merge s l r
<VAR>α : Type u_1<VAR>x : α<VAR>r l : List α<VAR>s : α → α → Bool<VAR>h : x ∈ r<GOAL>x ∈ List.merge s l r
<VAR>α : Type<VAR>self : IO.PromiseImpl α<GOAL>Nonempty α
<VAR>i : Nat<GOAL>Lean.Omega.IntList.get [] i = 0
<VAR>x : Int<VAR>xs : List Int<GOAL>Lean.Omega.IntList.get (x :: xs) 0 = x
<VAR>x : Int<VAR>xs : List Int<VAR>i : Nat<GOAL>Lean.Omega.IntList.get (x :: xs) (i + 1) = Lean.Omega.IntList.get xs i
<VAR>f : Int → Int<VAR>i : Nat<VAR>xs : Lean.Omega.IntList<VAR>h : f 0 = 0<GOAL>Lean.Omega.IntList.get (List.map f xs) i = f (xs.get i)
<VAR>i : Nat<VAR>xs : Lean.Omega.IntList<VAR>h : List.length xs ≤ i<GOAL>xs.get i = 0
<VAR>y : Int<GOAL>Lean.Omega.IntList.set [] 0 y = [y]
<VAR>i : Nat<VAR>y : Int<GOAL>Lean.Omega.IntList.set [] (i + 1) y = 0 :: Lean.Omega.IntList.set [] i y
<VAR>x : Int<VAR>xs : List Int<VAR>y : Int<GOAL>Lean.Omega.IntList.set (x :: xs) 0 y = y :: xs
<VAR>x : Int<VAR>xs : List Int<VAR>i : Nat<VAR>y : Int<GOAL>Lean.Omega.IntList.set (x :: xs) (i + 1) y = x :: Lean.Omega.IntList.set xs i y
<VAR>xs ys : Lean.Omega.IntList<GOAL>xs + ys = List.zipWithAll (fun x y => x.getD 0 + y.getD 0) xs ys
<VAR>xs ys : Lean.Omega.IntList<VAR>i : Nat<GOAL>(xs + ys).get i = xs.get i + ys.get i
<VAR>xs : Lean.Omega.IntList<GOAL>xs + [] = xs
<VAR>xs : Lean.Omega.IntList<GOAL>[] + xs = xs
<VAR>x : Int<VAR>xs : Lean.Omega.IntList<VAR>y : Int<VAR>ys : Lean.Omega.IntList<GOAL>x :: xs + y :: ys = (x + y) :: (xs + ys)
<VAR>xs ys : Lean.Omega.IntList<GOAL>xs * ys = List.zipWith (fun x x_1 => x * x_1) xs ys
<VAR>xs ys : Lean.Omega.IntList<VAR>i : Nat<GOAL>(xs * ys).get i = xs.get i * ys.get i
<VAR>x : Int<VAR>xs : List Int<VAR>y : Int<VAR>ys : List Int<GOAL>(x :: xs) * (y :: ys) = x * y :: xs * ys
<VAR>xs : Lean.Omega.IntList<GOAL>-xs = List.map (fun x => -x) xs
<VAR>xs : Lean.Omega.IntList<VAR>i : Nat<GOAL>(-xs).get i = -xs.get i
<VAR>x : Int<VAR>xs : List Int<GOAL>-(x :: xs) = -x :: -xs
<VAR>xs ys : Lean.Omega.IntList<GOAL>xs - ys = List.zipWithAll (fun x y => x.getD 0 - y.getD 0) xs ys
<VAR>xs : Lean.Omega.IntList<VAR>i : Int<GOAL>i * xs = List.map (fun x => i * x) xs
<VAR>xs : Lean.Omega.IntList<VAR>a : Int<VAR>i : Nat<GOAL>(a * xs).get i = a * xs.get i
<VAR>x : Int<VAR>xs : List Int<VAR>i : Int<GOAL>i * (x :: xs) = i * x :: i * xs
<VAR>a : Int<VAR>xs : Lean.Omega.IntList<VAR>b : Int<VAR>ys : Lean.Omega.IntList<GOAL>Lean.Omega.IntList.combo a xs b ys = a * xs + b * ys
<VAR>xs ys zs : Lean.Omega.IntList<GOAL>(xs + ys) * zs = xs * zs + ys * zs
<VAR>xs ys : Lean.Omega.IntList<GOAL>-xs * ys = -(xs * ys)
<VAR>xs ys : Lean.Omega.IntList<GOAL>xs - ys = xs + -ys
<VAR>i : Int<VAR>xs ys : Lean.Omega.IntList<GOAL>i * xs * ys = i * (xs * ys)
<VAR>x : Int<VAR>xs : List Int<GOAL>Lean.Omega.IntList.sum (x :: xs) = x + Lean.Omega.IntList.sum xs
<VAR>xs ys : Lean.Omega.IntList<GOAL>(xs + ys).sum = xs.sum + ys.sum
<VAR>xs : Lean.Omega.IntList<GOAL>(-xs).sum = -xs.sum
<VAR>i : Int<VAR>xs : Lean.Omega.IntList<GOAL>(i * xs).sum = i * xs.sum
<VAR>ys : Lean.Omega.IntList<GOAL>Lean.Omega.IntList.dot [] ys = 0
<VAR>xs : Lean.Omega.IntList<GOAL>xs.dot [] = 0
<VAR>x : Int<VAR>xs : List Int<VAR>y : Int<VAR>ys : List Int<GOAL>Lean.Omega.IntList.dot (x :: xs) (y :: ys) = x * y + Lean.Omega.IntList.dot xs ys
<VAR>xs ys : Lean.Omega.IntList<VAR>i : Nat<VAR>z : Int<GOAL>(xs.set i z).dot ys = xs.dot ys + (z - xs.get i) * ys.get i
<VAR>xs ys zs : Lean.Omega.IntList<GOAL>(xs + ys).dot zs = xs.dot zs + ys.dot zs
<VAR>xs ys : Lean.Omega.IntList<GOAL>(-xs).dot ys = -xs.dot ys
<VAR>xs ys : Lean.Omega.IntList<VAR>i : Int<GOAL>(i * xs).dot ys = i * xs.dot ys
<VAR>xs ys : Lean.Omega.IntList<VAR>w : ∀ (x : Int), x ∈ xs → x = 0<GOAL>xs.dot ys = 0
<VAR>g : Int<GOAL>Lean.Omega.IntList.sdiv [] g = []
<VAR>x : Int<VAR>xs : List Int<VAR>g : Int<GOAL>Lean.Omega.IntList.sdiv (x :: xs) g = x / g :: Lean.Omega.IntList.sdiv xs g
<VAR>x : Int<VAR>xs : List Int<GOAL>Lean.Omega.IntList.gcd (x :: xs) = x.natAbs.gcd (Lean.Omega.IntList.gcd xs)
<VAR>x : Int<VAR>xs : List Int<GOAL>↑(Lean.Omega.IntList.gcd (x :: xs)) ∣ x
<VAR>x : Int<VAR>xs : List Int<GOAL>Lean.Omega.IntList.gcd (x :: xs) ∣ Lean.Omega.IntList.gcd xs
<VAR>x : Int<VAR>xs : List Int<GOAL>↑(Lean.Omega.IntList.gcd (x :: xs)) ∣ ↑(Lean.Omega.IntList.gcd xs)
<VAR>xs : Lean.Omega.IntList<VAR>a : Int<VAR>m : a ∈ xs<GOAL>↑xs.gcd ∣ a
<VAR>xs : Lean.Omega.IntList<VAR>c : Nat<VAR>w : ∀ {a : Int}, a ∈ xs → ↑c ∣ a<GOAL>c ∣ xs.gcd
<VAR>xs : Lean.Omega.IntList<VAR>g : Nat<GOAL>xs.gcd = g ↔ (∀ {a : Int}, a ∈ xs → ↑g ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
<VAR>xs : Lean.Omega.IntList<GOAL>xs.gcd = 0 ↔ ∀ (x : Int), x ∈ xs → x = 0
<VAR>xs ys : Lean.Omega.IntList<GOAL>xs.dot ys % ↑xs.gcd = 0
<VAR>xs ys : Lean.Omega.IntList<GOAL>↑xs.gcd ∣ xs.dot ys
<VAR>xs ys : Lean.Omega.IntList<VAR>h : ∀ (x : Int), x ∈ xs → x = 0<GOAL>xs.dot ys = 0
<VAR>xs ys : Lean.Omega.IntList<VAR>d : Int<VAR>h : d ∣ ↑xs.gcd<GOAL>(xs.sdiv d).dot ys = xs.dot ys / d
<VAR>x : Lean.Omega.IntList<VAR>m : Nat<GOAL>List.length (x.bmod m) ≤ List.length x
<VAR>m : Nat<VAR>xs ys : Lean.Omega.IntList<GOAL>↑m ∣ Lean.Omega.IntList.bmod_dot_sub_dot_bmod m xs ys
<VAR>p p' q : Prop<VAR>he : p = p'<VAR>h : p' → q<GOAL>p → q
<VAR>σ α : Type<VAR>self : ST.Ref σ α<GOAL>Nonempty α
<VAR>α : Sort u<VAR>a : α<GOAL>id a = a
<VAR>β : Sort u_1<VAR>α : Sort u_2<VAR>y : β<VAR>x : α<GOAL>Function.const α y x = y
<VAR>β : Sort u_1<VAR>δ : Sort u_2<VAR>α : Sort u_3<VAR>f : β → δ<VAR>g : α → β<VAR>x : α<GOAL>(f ∘ g) x = f (g x)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>δ : Sort u_3<VAR>f : β → δ<VAR>g : α → β<GOAL>f ∘ g = fun x => f (g x)
<VAR>α : Type u_1<VAR>SizeOf α<VAR>a : Thunk α<GOAL>sizeOf a = 1 + sizeOf a.get
<VAR>a b : Prop<VAR>self : a ↔ b<GOAL>a → b
<VAR>a b : Prop<VAR>self : a ↔ b<GOAL>b → a
<VAR>α : Type u<VAR>β : Type v<VAR>EmptyCollection β<VAR>Insert α β<VAR>Singleton α β<VAR>self : LawfulSingleton α β<VAR>x : α<GOAL>insert x ∅ = singleton x
<VAR>α : Sort u<VAR>default : α<GOAL>optParam α default = α
<VAR>α : Type u<VAR>BEq α<VAR>self : LawfulBEq α<VAR>a : α<GOAL>(a == a) = true
<VAR>α : Type u<VAR>BEq α<VAR>self : LawfulBEq α<VAR>a b : α<GOAL>(a == b) = true → a = b
<VAR>a b : Prop<VAR>h₁ : a → b<VAR>h₂ : ¬b<GOAL>¬a
<VAR>p : Prop<VAR>h : p<GOAL>¬¬p
<VAR>a : Prop<VAR>h₁ h₂ : a<GOAL>h₁ = h₂
<VAR>α : Sort u<VAR>p : α → Prop<VAR>a b : α<VAR>h₁ : b = a<VAR>h₂ : p a<GOAL>p b
<VAR>α : Sort u<VAR>h : α = α<VAR>a : α<GOAL>cast h a = a
<VAR>α : Sort u<VAR>a b : α<VAR>h : a = b → False<GOAL>a ≠ b
<VAR>α : Sort u<VAR>a b : α<VAR>h : a ≠ b<GOAL>a = b → False
<VAR>α : Sort u<VAR>a : α<VAR>h : a ≠ a<GOAL>False
<VAR>α : Sort u<VAR>a b : α<VAR>h : a ≠ b<GOAL>b ≠ a
<VAR>α : Sort u_1<VAR>a b : α<GOAL>a ≠ b ↔ b ≠ a
<VAR>α : Sort u<VAR>a : α<GOAL>a ≠ a → False
<VAR>p : Prop<GOAL>¬p → p ≠ True
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>h : (a == b) = false<GOAL>a ≠ b
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>h : a ≠ b<GOAL>(a == b) = false
<VAR>α β : Sort u<VAR>a : α<VAR>b : β<VAR>p : (T : Sort u) → T → Prop<VAR>h₁ : HEq a b<VAR>h₂ : p α a<GOAL>p β b
<VAR>α β : Sort u<VAR>a : α<VAR>b : β<VAR>h : HEq a b<GOAL>HEq b a
<VAR>α : Sort u<VAR>a a' : α<VAR>h : a = a'<GOAL>HEq a a'
<VAR>α β φ : Sort u<VAR>a : α<VAR>b : β<VAR>c : φ<VAR>h₁ : HEq a b<VAR>h₂ : HEq b c<GOAL>HEq a c
<VAR>α β : Sort u<VAR>a : α<VAR>b b' : β<VAR>h₁ : HEq a b<VAR>h₂ : b = b'<GOAL>HEq a b'
<VAR>α β : Sort u<VAR>a a' : α<VAR>b : β<VAR>h₁ : a = a'<VAR>h₂ : HEq a' b<GOAL>HEq a b
<VAR>α β : Sort u<VAR>a : α<VAR>b : β<VAR>h : HEq a b<GOAL>α = β
<VAR>α : Sort u<VAR>φ : α → Sort v<VAR>a a' : α<VAR>h : a = a'<VAR>p : φ a<GOAL>HEq (Eq.recOn h p) p
<VAR>α β : Sort u<VAR>a : α<VAR>b : β<VAR>h₁ : α = β<VAR>h₂ : Eq.rec a h₁ = b<GOAL>HEq a b
<VAR>α β : Sort u<VAR>h : α = β<VAR>a : α<GOAL>HEq (cast h a) a
<VAR>a b : Prop<GOAL>(a ↔ b) ↔ (a → b) ∧ (b → a)
<VAR>a b : Prop<VAR>h : a = b<GOAL>a ↔ b
<VAR>a b c : Prop<VAR>h₁ : a ↔ b<VAR>h₂ : b ↔ c<GOAL>a ↔ c
<VAR>α : Sort u_1<VAR>a b : α<GOAL>a = b ↔ b = a
<VAR>a b : Prop<VAR>h : a ↔ b<GOAL>b ↔ a
<VAR>a b : Prop<GOAL>(a ↔ b) ↔ (b ↔ a)
<VAR>a b : Prop<GOAL>a ∧ b → b ∧ a
<VAR>a b : Prop<GOAL>a ∧ b ↔ b ∧ a
<VAR>a b : Prop<GOAL>a ∨ b → b ∨ a
<VAR>a b : Prop<GOAL>a ∨ b ↔ b ∨ a
<VAR>α : Sort u<VAR>p : α → Prop<VAR>b : Prop<VAR>h₁ : Exists fun x => p x<VAR>h₂ : ∀ (a : α), p a → b<GOAL>b
<VAR>p : Prop<VAR>d : Decidable p<VAR>h : p<GOAL>toBoolUsing d = true
<VAR>p : Prop<VAR>d : Decidable p<VAR>h : toBoolUsing d = true<GOAL>p
<VAR>p : Prop<VAR>d : Decidable p<VAR>h : toBoolUsing d = false<GOAL>¬p