ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>c₀ : Batteries.RBColor<VAR>n₀ : Nat<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>t : Batteries.RBNode α<VAR>path : Batteries.RBNode.Path α<VAR>hp : Batteries.RBNode.Path.Balanced c₀ n₀ path c n<VAR>ht : Batteries.RBNode.RedRed (c = Batteries.RBColor.red) t n<GOAL>∃ n, (path.ins t).Balanced Batteries.RBColor.black n
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>v : α<VAR>path : Batteries.RBNode.Path α<VAR>H : Batteries.RBNode.Path.Balanced c n path Batteries.RBColor.black 0<GOAL>∃ n, (path.insertNew v).Balanced Batteries.RBColor.black n
<VAR>α : Type u_1<VAR>c₀ : Batteries.RBColor<VAR>n₀ : Nat<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>c' : Batteries.RBColor<VAR>t : Batteries.RBNode α<VAR>path : Batteries.RBNode.Path α<VAR>hp : Batteries.RBNode.Path.Balanced c₀ n₀ path c n<VAR>ht : Batteries.RBNode.DelProp c' t n<VAR>hc : c = Batteries.RBColor.black → c' ≠ Batteries.RBColor.red<GOAL>∃ n, (path.del t c').Balanced Batteries.RBColor.black n
<GOAL>∀ {α : Type u_1} {cut : α → Ordering} {t : Batteries.RBNode α} {path : Batteries.RBNode.Path α} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α}, Batteries.RBNode.zoom cut t path = (t', path') → Batteries.RBNode.Path.Zoomed cut path → Batteries.RBNode.Path.Zoomed cut path'
<VAR>α : Type u_1<VAR>a b : α<VAR>cmp : α → α → Ordering<VAR>h : Batteries.RBNode.cmpEq cmp a b<VAR>t : Batteries.RBNode.Path α<GOAL>Batteries.RBNode.Path.RootOrdered cmp t a ↔ Batteries.RBNode.Path.RootOrdered cmp t b
<VAR>α : Type u_1<VAR>v : α<VAR>cmp : α → α → Ordering<VAR>path : Batteries.RBNode.Path α<GOAL>Batteries.RBNode.Path.Zoomed (cmp v) path → Batteries.RBNode.Path.RootOrdered cmp path v
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>path : Batteries.RBNode.Path α<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Ordered cmp (path.fill t) ↔ Batteries.RBNode.Path.Ordered cmp path ∧ Batteries.RBNode.Ordered cmp t ∧ Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>t' : Batteries.RBNode α<VAR>path' : Batteries.RBNode.Path α<VAR>t : Batteries.RBNode α<VAR>path : Batteries.RBNode.Path α<VAR>ht : Batteries.RBNode.Ordered cmp t<VAR>hp : Batteries.RBNode.Path.Ordered cmp path<VAR>tp : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t<VAR>pz : Batteries.RBNode.Path.Zoomed cut path<VAR>eq : Batteries.RBNode.zoom cut t path = (t', path')<GOAL>Batteries.RBNode.Ordered cmp t' ∧ Batteries.RBNode.Path.Ordered cmp path' ∧ Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path') t' ∧ Batteries.RBNode.Path.Zoomed cut path'
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>t' : Batteries.RBNode α<VAR>path' : Batteries.RBNode.Path α<VAR>t : Batteries.RBNode α<VAR>ht : Batteries.RBNode.Ordered cmp t<VAR>eq : Batteries.RBNode.zoom cut t = (t', path')<GOAL>Batteries.RBNode.Ordered cmp t' ∧ Batteries.RBNode.Path.Ordered cmp path' ∧ Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path') t' ∧ Batteries.RBNode.Path.Zoomed cut path'
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>path : Batteries.RBNode.Path α<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Path.Ordered cmp path → Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t → Batteries.RBNode.Ordered cmp (path.ins t)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>v : α<VAR>path : Batteries.RBNode.Path α<VAR>hp : Batteries.RBNode.Path.Ordered cmp path<VAR>vp : Batteries.RBNode.Path.RootOrdered cmp path v<GOAL>Batteries.RBNode.Ordered cmp (path.insertNew v)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>path : Batteries.RBNode.Path α<VAR>t : Batteries.RBNode α<VAR>c : Batteries.RBColor<GOAL>Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Path.Ordered cmp path → Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t → Batteries.RBNode.Ordered cmp (path.del t c)
<VAR>α : Type u_1<VAR>cut : α → Ordering<VAR>f : Option α → Option α<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBNode α<VAR>H : ∀ {x : α} {t' : Batteries.RBNode α} {p : Batteries.RBNode.Path α}, Batteries.RBNode.zoom cut t = (t', p) → f t'.root? = some x → Batteries.RBNode.Path.RootOrdered cmp p x ∧ Batteries.RBNode.OnRoot (Batteries.RBNode.cmpEq cmp x) t'<VAR>h : Batteries.RBNode.Ordered cmp t<GOAL>Batteries.RBNode.Ordered cmp (Batteries.RBNode.alter cut f t)
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>cut : α → Ordering<VAR>f : Option α → Option α<VAR>t : Batteries.RBNode α<VAR>h : t.Balanced c n<GOAL>∃ c n, (Batteries.RBNode.alter cut f t).Balanced c n
<VAR>α : Type u_1<VAR>cut : α → Ordering<VAR>f : α → α<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.modify cut f t = Batteries.RBNode.alter cut (Option.map f) t
<VAR>α : Type u_1<VAR>cut : α → Ordering<VAR>cmp : α → α → Ordering<VAR>f : α → α<VAR>t : Batteries.RBNode α<VAR>H : Batteries.RBNode.OnRoot (fun x => Batteries.RBNode.cmpEq cmp (f x) x) (Batteries.RBNode.zoom cut t).fst<VAR>h : Batteries.RBNode.Ordered cmp t<GOAL>Batteries.RBNode.Ordered cmp (Batteries.RBNode.modify cut f t)
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>cut : α → Ordering<VAR>f : α → α<VAR>t : Batteries.RBNode α<VAR>h : t.Balanced c n<GOAL>∃ c n, (Batteries.RBNode.modify cut f t).Balanced c n
<VAR>α : Type u_1<VAR>cut : α → Ordering<VAR>f : Option α → Option α<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBNode α<VAR>H : ∀ {x : α} {t' : Batteries.RBNode α} {p : Batteries.RBNode.Path α}, Batteries.RBNode.zoom cut t = (t', p) → f t'.root? = some x → Batteries.RBNode.Path.RootOrdered cmp p x ∧ Batteries.RBNode.OnRoot (Batteries.RBNode.cmpEq cmp x) t'<VAR>h : Batteries.RBNode.WF cmp t<GOAL>Batteries.RBNode.WF cmp (Batteries.RBNode.alter cut f t)
<VAR>α : Type u_1<VAR>cut : α → Ordering<VAR>cmp : α → α → Ordering<VAR>f : α → α<VAR>t : Batteries.RBNode α<VAR>H : Batteries.RBNode.OnRoot (fun x => Batteries.RBNode.cmpEq cmp (f x) x) (Batteries.RBNode.zoom cut t).fst<VAR>h : Batteries.RBNode.WF cmp t<GOAL>Batteries.RBNode.WF cmp (Batteries.RBNode.modify cut f t)
<VAR>α : Type u_1<VAR>cut : α → Ordering<VAR>t : Batteries.RBNode α<VAR>p : Batteries.RBNode.Path α := Batteries.RBNode.Path.root<GOAL>Batteries.RBNode.find? cut t = (Batteries.RBNode.zoom cut t p).fst.root?
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>f : α → α<VAR>t : Batteries.RBSet α cmp<VAR>H : ∀ {x : α}, Batteries.RBNode.find? cut t.val = some x → Batteries.RBNode.cmpEq cmp (f x) x<GOAL>t.ModifyWF cut f
<GOAL>∀ {α : Type u_1} {a : α} {l : List α} {R : α → α → Prop}, List.Pairwise R (a :: l) → ∀ {a' : α}, a' ∈ l → R a a'
<GOAL>∀ {α : Type u_1} {a : α} {l : List α} {R : α → α → Prop}, List.Pairwise R (a :: l) → List.Pairwise R l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<VAR>_p : List.Pairwise R l<GOAL>List.Pairwise R l.tail
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<VAR>n : Nat<GOAL>List.Pairwise R l → List.Pairwise R (List.drop n l)
<VAR>α : Type u_1<VAR>l : List α<VAR>R S : α → α → Prop<VAR>H : ∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b<VAR>p : List.Pairwise R l<GOAL>List.Pairwise S l
<GOAL>∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {S : α → α → Prop}, List.Pairwise R l → List.Pairwise S l → List.Pairwise (fun a b => R a b ∧ S a b) l
<GOAL>∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {S : α → α → Prop}, List.Pairwise (fun a b => R a b ∧ S a b) l ↔ List.Pairwise R l ∧ List.Pairwise S l
<GOAL>∀ {α : Type u_1} {R S T : α → α → Prop} {l : List α}, (∀ (a b : α), R a b → S a b → T a b) → List.Pairwise R l → List.Pairwise S l → List.Pairwise T l
<VAR>α : Type u_1<VAR>R S : α → α → Prop<VAR>l : List α<VAR>H : ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ S a b)<GOAL>List.Pairwise R l ↔ List.Pairwise S l
<VAR>α : Type u_1<VAR>R S : α → α → Prop<VAR>H : ∀ (a b : α), R a b ↔ S a b<VAR>l : List α<GOAL>List.Pairwise R l ↔ List.Pairwise S l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<VAR>H : ∀ (x y : α), R x y<GOAL>List.Pairwise R l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Pairwise R l ↔ List.Pairwise (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Pairwise R l ↔ List.Pairwise (fun x y => x ∈ l → y ∈ l → R x y) l
<GOAL>∀ {α : Type u_1} {l : List α} {R : α → α → Prop}, (∀ (x : α), x ∈ l → R x x) → List.Pairwise R l → List.Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>a : α<GOAL>List.Pairwise R [a]
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>a b : α<GOAL>List.Pairwise R [a, b] ↔ R a b
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>s : ∀ {x y : α}, R x y → R y x<VAR>l₁ l₂ : List α<GOAL>List.Pairwise R (l₁ ++ l₂) ↔ List.Pairwise R (l₂ ++ l₁)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>s : ∀ {x y : α}, R x y → R y x<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>List.Pairwise R (l₁ ++ a :: l₂) ↔ List.Pairwise R (a :: (l₁ ++ l₂))
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : α → α → Prop<VAR>l : List α<VAR>S : β → β → Prop<VAR>f : α → β<VAR>H : ∀ (a b : α), S (f a) (f b) → R a b<VAR>p : List.Pairwise S (List.map f l)<GOAL>List.Pairwise R l
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : α → α → Prop<VAR>l : List α<VAR>S : β → β → Prop<VAR>f : α → β<VAR>H : ∀ (a b : α), R a b → S (f a) (f b)<VAR>p : List.Pairwise R l<GOAL>List.Pairwise S (List.map f l)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : α → α → Prop<VAR>f : β → Option α<VAR>l : List β<GOAL>List.Pairwise R (List.filterMap f l) ↔ List.Pairwise (fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : α → α → Prop<VAR>S : β → β → Prop<VAR>f : α → Option β<VAR>H : ∀ (a a' : α), R a a' → ∀ (b : β), b ∈ f a → ∀ (b' : β), b' ∈ f a' → S b b'<VAR>l : List α<VAR>p : List.Pairwise R l<GOAL>List.Pairwise S (List.filterMap f l)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<GOAL>List.Pairwise R (List.filter (fun b => decide (p b)) l) ↔ List.Pairwise (fun x y => p x → p y → R x y) l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<VAR>p : α → Bool<GOAL>List.Pairwise R l → List.Pairwise R (List.filter p l)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>L : List (List α)<GOAL>List.Pairwise R L.join ↔ (∀ (l : List α), l ∈ L → List.Pairwise R l) ∧ List.Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : β → β → Prop<VAR>l : List α<VAR>f : α → List β<GOAL>List.Pairwise R (l.bind f) ↔ (∀ (a : α), a ∈ l → List.Pairwise R (f a)) ∧ List.Pairwise (fun a₁ a₂ => ∀ (x : β), x ∈ f a₁ → ∀ (y : β), y ∈ f a₂ → R x y) l
<GOAL>∀ {α : Type u_1} {l : List α} {R : α → α → Prop}, List.Pairwise R l ↔ ∀ {a b : α}, [a, b] <+ l → R a b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>r : α → α → Prop<VAR>hr : ∀ (a : α), 1 < List.count a l → r a a<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b<GOAL>List.Pairwise r l
<VAR>α : Type u_1<VAR>l : List α<VAR>is : List (Fin l.length)<VAR>h : List.Pairwise (fun x x_1 => ↑x < ↑x_1) is<GOAL>List.map l.get is <+ l
<GOAL>∀ {α : Type u_1} {l' l : List α}, l' <+ l → ∃ is, l' = List.map l.get is ∧ List.Pairwise (fun x x_1 => x < x_1) is
<GOAL>∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l ↔ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
<GOAL>∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x : α<VAR>hx : r x x<VAR>n : Nat<GOAL>List.Pairwise r (List.replicate n x)
<GOAL>∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R], List.pwFilter R [] = []
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<VAR>l : List α<VAR>h : ∀ (b : α), b ∈ List.pwFilter R l → R a b<GOAL>List.pwFilter R (a :: l) = a :: List.pwFilter R l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<VAR>l : List α<VAR>h : ¬∀ (b : α), b ∈ List.pwFilter R l → R a b<GOAL>List.pwFilter R (a :: l) = List.pwFilter R l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>β : Type u_2<VAR>DecidableRel R<VAR>f : β → α<VAR>l : List β<GOAL>List.pwFilter R (List.map f l) = List.map f (List.pwFilter (fun x y => R (f x) (f y)) l)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>List.pwFilter R l <+ l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>List.pwFilter R l ⊆ l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>List.Pairwise R (List.pwFilter R l)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>List.pwFilter R l = l ↔ List.Pairwise R l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<VAR>DecidableRel R<GOAL>List.pwFilter R (List.pwFilter R l) = List.pwFilter R l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z<VAR>a : α<VAR>l : List α<GOAL>(∀ (b : α), b ∈ List.pwFilter R l → R a b) ↔ ∀ (b : α), b ∈ l → R a b
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∅ = Batteries.AssocList.nil
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Batteries.AssocList α β<GOAL>l.isEmpty = l.toList.isEmpty
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Batteries.AssocList.nil.length = 0
<GOAL>∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β} {t : Batteries.AssocList α β}, (Batteries.AssocList.cons a b t).length = t.length + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Batteries.AssocList α β<GOAL>l.toList.length = l.length
<VAR>m : Type u_1 → Type u_2<VAR>δ : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monad m<VAR>f : δ → α → β → m δ<VAR>init : δ<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.foldlM f init l = List.foldlM (fun d x => match x with | (a, b) => f d a b) init l.toList
<VAR>δ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : δ → α → β → δ<VAR>init : δ<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.foldl f init l = List.foldl (fun d x => match x with | (a, b) => f d a b) init l.toList
<GOAL>@Batteries.AssocList.toList = @Batteries.AssocList.toListTR
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monad m<VAR>f : α → β → m PUnit<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.forM f l = l.toList.forM fun x => match x with | (a, b) => f a b
<VAR>α : Type u_1<VAR>δ : Type u_2<VAR>β : Type u_3<VAR>f : α → δ<VAR>l : Batteries.AssocList α β<GOAL>(Batteries.AssocList.mapKey f l).toList = List.map (fun x => match x with | (a, b) => (f a, b)) l.toList
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {β : Type u_3} {l : Batteries.AssocList α β}, (Batteries.AssocList.mapKey f l).length = l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>f : α → β → δ<VAR>l : Batteries.AssocList α β<GOAL>(Batteries.AssocList.mapVal f l).toList = List.map (fun x => match x with | (a, b) => (a, f a b)) l.toList
<GOAL>∀ {α : Type u_1} {β : Type u_2} {β_1 : Type u_3} {f : α → β → β_1} {l : Batteries.AssocList α β}, (Batteries.AssocList.mapVal f l).length = l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → β → Bool<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.findEntryP? p l = List.find? (fun x => match x with | (a, b) => p a b) l.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>a : α<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.findEntry? a l = List.find? (fun x => x.fst == a) l.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>a : α<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.find? a l = Option.map (fun x => x.snd) (Batteries.AssocList.findEntry? a l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>a : α<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.find? a l = Option.map (fun x => x.snd) (List.find? (fun x => x.fst == a) l.toList)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → β → Bool<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.any p l = l.toList.any fun x => match x with | (a, b) => p a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → β → Bool<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.all p l = l.toList.all fun x => match x with | (a, b) => p a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>a : α<VAR>l : Batteries.AssocList α β<GOAL>Batteries.AssocList.contains a l = l.toList.any fun x => x.fst == a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>a : α<VAR>b : β<VAR>l : Batteries.AssocList α β<GOAL>(Batteries.AssocList.replace a b l).toList = List.replaceF (fun x => bif x.fst == a then some (a, b) else none) l.toList
<VAR>α : Type u_1<GOAL>∀ {β : Type u_2} {b : β} {l : Batteries.AssocList α β} [inst : BEq α] {a : α}, (Batteries.AssocList.replace a b l).length = l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → β → Bool<VAR>l : Batteries.AssocList α β<GOAL>(Batteries.AssocList.eraseP p l).toList = List.eraseP (fun x => match x with | (a, b) => p a b) l.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>a : α<VAR>l : Batteries.AssocList α β<GOAL>(Batteries.AssocList.erase a l).toList = List.eraseP (fun x => x.fst == a) l.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>BEq α<VAR>a : α<VAR>l : Batteries.AssocList α β<GOAL>(Batteries.AssocList.modify a f l).toList = List.replaceF (fun x => match x with | (k, v) => bif k == a then some (a, f k v) else none) l.toList
<VAR>α : Type u_1<GOAL>∀ {β : Type u_2} {f : α → β → β} {l : Batteries.AssocList α β} [inst : BEq α] {a : α}, (Batteries.AssocList.modify a f l).length = l.length
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>δ : Type u_1<VAR>Monad m<VAR>l : Batteries.AssocList α β<VAR>init : δ<VAR>f : α × β → δ → m (ForInStep δ)<GOAL>forIn l init f = forIn l.toList init f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (α × β)<GOAL>l.toAssocList.toList = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Batteries.AssocList α β<GOAL>l.toList.toAssocList = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (α × β)<GOAL>l.toAssocList.length = l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>BEq β<GOAL>(Batteries.AssocList.nil == Batteries.AssocList.nil) = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>t : Batteries.AssocList α β<VAR>BEq α<VAR>BEq β<GOAL>(Batteries.AssocList.nil == Batteries.AssocList.cons a b t) = false
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>t : Batteries.AssocList α β<VAR>BEq α<VAR>BEq β<GOAL>(Batteries.AssocList.cons a b t == Batteries.AssocList.nil) = false
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>t : Batteries.AssocList α β<VAR>a' : α<VAR>b' : β<VAR>t' : Batteries.AssocList α β<VAR>BEq α<VAR>BEq β<GOAL>(Batteries.AssocList.cons a b t == Batteries.AssocList.cons a' b' t') = (a == a' && b == b' && t == t')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>BEq α<VAR>BEq β<VAR>l m : Batteries.AssocList α β<GOAL>(l == m) = (l.toList == m.toList)
<VAR>self : Rat<GOAL>self.den ≠ 0
<VAR>self : Rat<GOAL>self.num.natAbs.Coprime self.den
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den ≠ 0<VAR>e : g = num.natAbs.gcd den<GOAL>den / g ≠ 0
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den ≠ 0<VAR>e : g = num.natAbs.gcd den<GOAL>(num.div ↑g).natAbs.Coprime (den / g)
<VAR>a b : Rat<VAR>g ad bd : Nat<VAR>hg : g = a.den.gcd b.den<VAR>had : ad = a.den / g<VAR>hbd : bd = b.den / g<GOAL>let den := ad * b.den;
let num := a.num * ↑bd + b.num * ↑ad;
let num := a.num * ↑bd - b.num * ↑ad;
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>as : Array α<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>h : i ≤ as.size<VAR>b : β<VAR>j : Nat<GOAL>j + i = as.size → Array.forIn.loop as f i h b = forIn (List.drop j as.data) b f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<GOAL>forIn as b f = forIn as.data b f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>as : Array α<VAR>bs : Array β<VAR>i : Nat<VAR>cs : Array γ<GOAL>i ≤ as.size → i ≤ bs.size → (Array.zipWithAux f as bs i cs).data = cs.data ++ List.zipWith f (List.drop i as.data) (List.drop i bs.data)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>as : Array α<VAR>bs : Array β<GOAL>(as.zipWith bs f).data = List.zipWith f as.data bs.data
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>bs : Array β<GOAL>(as.zip bs).data = as.data.zip bs.data
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : Array α<VAR>bs : Array β<GOAL>(as.zip bs).size = min as.size bs.size
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : Array α<GOAL>(Array.filter p l 0).size ≤ l.size
<VAR>α : Type u_1<VAR>l : Array (Array α)<GOAL>l.join.data = (List.map Array.data l.data).join
<VAR>α : Type u_1<VAR>a : α<VAR>L : Array (Array α)<GOAL>a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l
<VAR>α : Type u_1<VAR>a : Array α<VAR>n : Nat<GOAL>(Array.shrink.loop n a).size = a.size - n
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → m β<GOAL>Array.mapM f #[] = pure #[]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Array.map f #[] = #[]
<GOAL>∀ {α : Type u_1} {a b : α}, a ∈ #[b] ↔ a = b
<VAR>α : Type u_1<VAR>xs : LazyList α<GOAL>xs.append (Thunk.pure LazyList.nil) = xs
<VAR>α : Type u_1<VAR>x : α<GOAL>x ∈ LazyList.nil ↔ False
<VAR>α : Type u_1<VAR>x y : α<VAR>ys : Thunk (LazyList α)<GOAL>x ∈ LazyList.cons y ys ↔ x = y ∨ x ∈ ys.get
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>a : α<VAR>l : Thunk (LazyList α)<GOAL>(∀ (x : α), x ∈ LazyList.cons a l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l.get → p x
<VAR>α : Type u_1<VAR>a b : Set α<VAR>h : ∀ (x : α), x ∈ a ↔ x ∈ b<GOAL>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>as : Array α<VAR>motive : Nat → β → Prop<VAR>f : β → α → m β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (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>SatisfiesM (motive as.size) (Array.foldlM.loop f as as.size ⋯ i j b)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>as : Array α<VAR>motive : Nat → β → Prop<VAR>init : β<VAR>h0 : motive 0 init<VAR>f : β → α → m β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])<GOAL>SatisfiesM (motive as.size) (Array.foldlM f init as 0)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>as : Array α<VAR>f : α → m β<VAR>motive : Nat → Prop<VAR>h0 : motive 0<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])<GOAL>SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ arr[i]) (Array.mapM f as)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>as : Array α<VAR>f : α → m β<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), SatisfiesM (p i) (f as[i])<GOAL>SatisfiesM (fun arr => ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ arr[i]) (Array.mapM f as)
<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>as : Array α<GOAL>SatisfiesM (fun arr => arr.size = as.size) (Array.mapM f as)
<VAR>m : Type → Type u_1<VAR>α : Type u_2<VAR>Monad m<VAR>LawfulMonad m<VAR>p : α → m Bool<VAR>as : Array α<VAR>tru : Prop<VAR>fal : Nat → Prop<VAR>stop j : Nat<VAR>hj' : j ≤ stop<VAR>hstop : stop ≤ as.size<VAR>h0 : fal j<VAR>hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])<GOAL>SatisfiesM (fun res => bif res then tru else fal stop) (Array.anyM.loop p as stop hstop j)
<VAR>m : Type → Type u_1<VAR>α : Type u_2<VAR>Monad m<VAR>LawfulMonad m<VAR>p : α → m Bool<VAR>as : Array α<VAR>start stop : Nat<VAR>hstart : start ≤ min stop as.size<VAR>tru : Prop<VAR>fal : Nat → Prop<VAR>h0 : fal start<VAR>hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])<GOAL>SatisfiesM (fun res => bif res then tru else fal (min stop as.size)) (Array.anyM p as start stop)