ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Multiset α<GOAL>(Multiset.sort r s).length = Multiset.card s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<GOAL>Multiset.sort r 0 = []
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>a : α<GOAL>Multiset.sort r {a} = [a]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>Multiset.ndinsert a ↑l = ↑(insert a l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Multiset.ndinsert a 0 = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s → Multiset.ndinsert a s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∉ s → Multiset.ndinsert a s = a ::ₘ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Multiset α<GOAL>a ∈ Multiset.ndinsert b s ↔ a = b ∨ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>s ≤ Multiset.ndinsert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ Multiset.ndinsert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Multiset α<VAR>h : a ∈ s<GOAL>a ∈ Multiset.ndinsert b s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>h : a ∈ s<GOAL>Multiset.card (Multiset.ndinsert a s) = Multiset.card s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>h : a ∉ s<GOAL>Multiset.card (Multiset.ndinsert a s) = Multiset.card s + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).dedup = Multiset.ndinsert a s.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>s.Nodup → (Multiset.ndinsert a s).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>Multiset.ndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(Multiset.ndinsert a s).attach = Multiset.ndinsert ⟨a, ⋯⟩ (Multiset.map (fun p => ⟨↑p, ⋯⟩) s.attach)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>(Multiset.ndinsert a s).Disjoint t ↔ a ∉ t ∧ s.Disjoint t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<GOAL>s.Disjoint (Multiset.ndinsert a t) ↔ a ∉ s ∧ s.Disjoint t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>(↑l₁).ndunion ↑l₂ = ↑(l₁ ∪ l₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>Multiset.ndunion 0 s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>(a ::ₘ s).ndunion t = Multiset.ndinsert a (s.ndunion t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>a ∈ s.ndunion t ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>t ≤ s.ndunion t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>t ⊆ s.ndunion t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.ndunion t ≤ s + t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s.ndunion t ≤ u ↔ s ⊆ u ∧ t ≤ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ⊆ s.ndunion t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>t : Multiset α<VAR>d : s.Nodup<GOAL>s ≤ s.ndunion t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.ndunion t ≤ s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>t : Multiset α<GOAL>t.Nodup → (s.ndunion t).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>d : s.Nodup<GOAL>s.ndunion t = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(s + t).dedup = s.ndunion t.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : s.Disjoint t<GOAL>s.ndunion t = s.dedup + t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : s ⊆ t<GOAL>s.ndunion t = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>(↑l₁).ndinter ↑l₂ = ↑(l₁ ∩ l₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>Multiset.ndinter 0 s = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset α<VAR>h : a ∈ t<GOAL>(a ::ₘ s).ndinter t = a ::ₘ s.ndinter t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset α<VAR>h : a ∉ t<GOAL>(a ::ₘ s).ndinter t = s.ndinter t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>t : Multiset α<GOAL>s.Nodup → (s.ndinter t).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Multiset α<GOAL>s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.ndinter t ≤ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.ndinter t ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.ndinter t ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>t : Multiset α<VAR>d : s.Nodup<GOAL>s.ndinter t ≤ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s ∩ t ≤ s.ndinter t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>d : s.Nodup<GOAL>s.ndinter t = s ∩ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.ndinter t = 0 ↔ s.Disjoint t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>h : s ⊆ t<GOAL>s.ndinter t = s
<VAR>n : ℕ<VAR>α : Type u_1<GOAL>Function.Injective Mathlib.Vector.toList
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v w : Mathlib.Vector α n<GOAL>(∀ (m : Fin n), v.get m = w.get m) → v = w
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>↑(a ::ᵥ v) = a :: ↑v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Mathlib.Vector α n.succ<VAR>v' : Mathlib.Vector α n<GOAL>v = a ::ᵥ v' ↔ v.head = a ∧ v.tail = v'
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Mathlib.Vector α n.succ<VAR>v' : Mathlib.Vector α n<GOAL>v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n.succ<GOAL>∃ a as, v = a ::ᵥ as
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(Mathlib.Vector.ofFn f).toList = List.ofFn f
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<VAR>h : v.toList.length = n<GOAL>⟨v.toList, h⟩ = v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<GOAL>(↑v).length = n
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>v : Mathlib.Vector α n<VAR>f : α → β<GOAL>(Mathlib.Vector.map f v).toList = List.map f v.toList
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>v : Mathlib.Vector α (n + 1)<VAR>f : α → β<GOAL>(Mathlib.Vector.map f v).head = f v.head
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>v : Mathlib.Vector α (n + 1)<VAR>f : α → β<GOAL>(Mathlib.Vector.map f v).tail = Mathlib.Vector.map f v.tail
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<GOAL>v.get i = v.toList.get (Fin.cast ⋯ i)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>i : Fin n<GOAL>(Mathlib.Vector.replicate n a).get i = a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>v : Mathlib.Vector α n<VAR>f : α → β<VAR>i : Fin n<GOAL>(Mathlib.Vector.map f v).get i = f (v.get i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<GOAL>Mathlib.Vector.map₂ f Mathlib.Vector.nil Mathlib.Vector.nil = Mathlib.Vector.nil
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>hd₁ : α<VAR>tl₁ : Mathlib.Vector α n<VAR>hd₂ : β<VAR>tl₂ : Mathlib.Vector β n<VAR>f : α → β → γ<GOAL>Mathlib.Vector.map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ Mathlib.Vector.map₂ f tl₁ tl₂
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : Fin n<GOAL>(Mathlib.Vector.ofFn f).get i = f i
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<GOAL>Mathlib.Vector.ofFn v.get = v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>x : Mathlib.Vector α n<VAR>i : Fin (n - 1)<GOAL>x.tail.get i = x.get ⟨↑i + 1, ⋯⟩
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n.succ<VAR>i : Fin n<GOAL>v.tail.get i = v.get i.succ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n.succ<GOAL>↑v.tail = (↑v).tail
<VAR>α : Type u_1<GOAL>Mathlib.Vector.nil.tail = Mathlib.Vector.nil
<VAR>α : Type u_1<VAR>v : Mathlib.Vector α 1<GOAL>v.tail = Mathlib.Vector.nil
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n.succ → α<GOAL>(Mathlib.Vector.ofFn f).tail = Mathlib.Vector.ofFn fun i => f i.succ
<VAR>α : Type u_1<VAR>v : Mathlib.Vector α 0<GOAL>v.toList = []
<VAR>α : Type u_1<VAR>v : Mathlib.Vector α 1<GOAL>v.toList = [v.head]
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α (n + 1)<GOAL>v.toList.isEmpty = false
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α (n + 1)<GOAL>¬v.toList.isEmpty = true
<VAR>α : Type u_1<VAR>n : ℕ<VAR>v : Mathlib.Vector α n<GOAL>Mathlib.Vector.map id v = v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<GOAL>v.toList.Nodup ↔ Function.Injective v.get
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n.succ<GOAL>v.toList.head? = some v.head
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<GOAL>v.reverse.toList = v.toList.reverse
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<GOAL>v.reverse.reverse = v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n.succ<GOAL>v.get 0 = v.head
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n.succ → α<GOAL>(Mathlib.Vector.ofFn f).head = f 0
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>(a ::ᵥ v).get 0 = a
<VAR>α : Type u_1<VAR>ix : Fin 1<VAR>x : α<GOAL>(x ::ᵥ Mathlib.Vector.nil).get ix = x
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<GOAL>(a ::ᵥ v).get i.succ = v.get i
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α (n + 1)<GOAL>v.last = v.get (Fin.last n)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α (n + 1)<GOAL>v.reverse.head = v.last
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<GOAL>Mathlib.Vector.scanl f b Mathlib.Vector.nil = b ::ᵥ Mathlib.Vector.nil
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v : Mathlib.Vector α n<VAR>x : α<GOAL>Mathlib.Vector.scanl f b (x ::ᵥ v) = b ::ᵥ Mathlib.Vector.scanl f (f b x) v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v : Mathlib.Vector α n<GOAL>↑(Mathlib.Vector.scanl f b v) = List.scanl f b ↑v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v : Mathlib.Vector α n<GOAL>(Mathlib.Vector.scanl f b v).toList = List.scanl f b v.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v : Mathlib.Vector α 1<GOAL>Mathlib.Vector.scanl f b v = b ::ᵥ f b v.head ::ᵥ Mathlib.Vector.nil
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v : Mathlib.Vector α n<GOAL>(Mathlib.Vector.scanl f b v).head = b
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<GOAL>(Mathlib.Vector.scanl f b v).get i.succ = f ((Mathlib.Vector.scanl f b v).get i.castSucc) (v.get i)
<VAR>m : Type u_2 → Type u_3<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u_2<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(Mathlib.Vector.mOfFn fun i => pure (f i)) = pure (Mathlib.Vector.ofFn f)
<VAR>m : Type u_2 → Type u_3<VAR>Monad m<VAR>α : Type u_4<VAR>β : Type u_2<VAR>f : α → m β<GOAL>Mathlib.Vector.mmap f Mathlib.Vector.nil = pure Mathlib.Vector.nil
<VAR>m : Type u_2 → Type u_3<VAR>Monad m<VAR>α : Type u_4<VAR>β : Type u_2<VAR>f : α → m β<VAR>a : α<VAR>n : ℕ<VAR>v : Mathlib.Vector α n<GOAL>Mathlib.Vector.mmap f (a ::ᵥ v) = do let h' ← f a let t' ← Mathlib.Vector.mmap f v pure (h' ::ᵥ t')
<VAR>α : Type u_1<VAR>C : {n : ℕ} → Mathlib.Vector α n → Sort u_2<VAR>nil : C Mathlib.Vector.nil<VAR>cons : {n : ℕ} → {x : α} → {w : Mathlib.Vector α n} → C w → C (x ::ᵥ w)<GOAL>(Mathlib.Vector.nil.inductionOn nil fun {n} {x} {w} => cons) = nil
<VAR>α : Type u_1<VAR>C : {n : ℕ} → Mathlib.Vector α n → Sort u_2<VAR>n : ℕ<VAR>x : α<VAR>v : Mathlib.Vector α n<VAR>nil : C Mathlib.Vector.nil<VAR>cons : {n : ℕ} → {x : α} → {w : Mathlib.Vector α n} → C w → C (x ::ᵥ w)<GOAL>((x ::ᵥ v).inductionOn nil fun {n} {x} {w} => cons) = cons (v.inductionOn nil fun {n} {x} {w} => cons)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>i : Fin (n + 1)<VAR>v : Mathlib.Vector α n<GOAL>↑(Mathlib.Vector.insertNth a i v) = List.insertNth (↑i) a ↑v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>i : Fin n<VAR>v : Mathlib.Vector α n<GOAL>↑(Mathlib.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Mathlib.Vector α n<VAR>i : Fin (n + 1)<GOAL>Mathlib.Vector.eraseIdx i (Mathlib.Vector.insertNth a i v) = v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Mathlib.Vector α (n + 1)<VAR>i : Fin (n + 1)<VAR>j : Fin (n + 2)<GOAL>Mathlib.Vector.eraseIdx (j.succAbove i) (Mathlib.Vector.insertNth a j v) = Mathlib.Vector.insertNth a (i.predAbove j) (Mathlib.Vector.eraseIdx i v)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a b : α<VAR>i j : Fin (n + 1)<VAR>h : i ≤ j<VAR>v : Mathlib.Vector α n<GOAL>Mathlib.Vector.insertNth b j.succ (Mathlib.Vector.insertNth a i v) = Mathlib.Vector.insertNth a i.castSucc (Mathlib.Vector.insertNth b j v)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.set i a).toList = v.toList.set (↑i) a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.set i a).get i = a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<VAR>i j : Fin n<VAR>h : i ≠ j<VAR>a : α<GOAL>(v.set i a).get j = v.get j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Mathlib.Vector α n<VAR>i j : Fin n<VAR>a : α<GOAL>(v.set i a).get j = if i = j then a else v.get j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>AddMonoid α<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.set i a).toList.sum = (Mathlib.Vector.take (↑i) v).toList.sum + a + (Mathlib.Vector.drop (↑i + 1) v).toList.sum
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Monoid α<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.set i a).toList.prod = (Mathlib.Vector.take (↑i) v).toList.prod * a * (Mathlib.Vector.drop (↑i + 1) v).toList.prod
<VAR>n : ℕ<VAR>α : Type u_1<VAR>CommGroup α<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>v : Mathlib.Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.set i a).toList.sum = v.toList.sum + -v.get i + a
<VAR>n : ℕ<VAR>F : Type u → Type u<VAR>Applicative F<VAR>α β : Type u<VAR>f : α → F β<VAR>x : α<VAR>xs : Mathlib.Vector α n<GOAL>Mathlib.Vector.traverse f (x ::ᵥ xs) = Seq.seq (Mathlib.Vector.cons <$> f x) fun x => Mathlib.Vector.traverse f xs
<VAR>n : ℕ<VAR>α : Type u<VAR>x : Mathlib.Vector α n<GOAL>Mathlib.Vector.traverse pure x = x
<VAR>n : ℕ<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : Mathlib.Vector α n<GOAL>Mathlib.Vector.traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (Mathlib.Vector.traverse f <$> Mathlib.Vector.traverse g x)
<VAR>n : ℕ<VAR>α β : Type u_1<VAR>f : α → β<VAR>x : Mathlib.Vector α n<GOAL>Mathlib.Vector.traverse (pure ∘ f) x = pure (Mathlib.Vector.map f x)
<VAR>n : ℕ<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>LawfulApplicative F<VAR>η : ApplicativeTransformation F G<VAR>α β : Type u<VAR>f : α → F β<VAR>x : Mathlib.Vector α n<GOAL>(fun {α} => η.app α) (Mathlib.Vector.traverse f x) = Mathlib.Vector.traverse ((fun {α} => η.app α) ∘ f) x
<VAR>α : Type u_1<VAR>n : ℕ<VAR>val : α<GOAL>Mathlib.Vector.replicate (n + 1) val = val ::ᵥ Mathlib.Vector.replicate n val
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector α m<VAR>x : α<GOAL>((x ::ᵥ xs).append ys).get ⟨0, ⋯⟩ = x
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector α m<VAR>x : α<VAR>i : Fin (n + m)<VAR>h : ↑i + 1 < n.succ + m<GOAL>((x ::ᵥ xs).append ys).get ⟨↑i + 1, h⟩ = (xs.append ys).get i
<VAR>α : Type u_1<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<GOAL>xs.append Mathlib.Vector.nil = xs
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>n : ℕ<VAR>γ : Type u_1<VAR>v₁ : Mathlib.Vector α n<VAR>v₂ : Mathlib.Vector β n<VAR>f : α → β → γ<VAR>i : Fin n<GOAL>(Mathlib.Vector.map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<GOAL>∀ {α_1 : Type} {β : Type u_1} {f : α → α_1 → α_1 × β} {x : α} {s : α_1}, Mathlib.Vector.mapAccumr f (x ::ᵥ xs) s = let r := Mathlib.Vector.mapAccumr f xs s; let q := f x r.1; (q.1, q.2 ::ᵥ r.2)
<VAR>α β : Type<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<GOAL>∀ {α_1 β_1 : Type} {f : α → β → α_1 → α_1 × β_1} {x : α} {y : β} {s : α_1}, Mathlib.Vector.mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s = let r := Mathlib.Vector.mapAccumr₂ f xs ys s; let q := f x y r.1; (q.1, q.2 ::ᵥ r.2)
<VAR>α : Type u_1<GOAL>Multiset.Nodup 0
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).Nodup ↔ a ∉ s ∧ s.Nodup
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<VAR>m : a ∉ s<VAR>n : s.Nodup<GOAL>(a ::ₘ s).Nodup
<VAR>α : Type u_1<VAR>a : α<GOAL>{a}.Nodup
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<VAR>h : (a ::ₘ s).Nodup<GOAL>s.Nodup
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<VAR>h : (a ::ₘ s).Nodup<GOAL>a ∉ s
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>t.Nodup → s.Nodup
<VAR>α : Type u_1<VAR>a : α<GOAL>¬(a ::ₘ a ::ₘ 0).Nodup
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s.Nodup ↔ ∀ (a : α), ¬a ::ₘ a ::ₘ 0 ≤ s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s.Nodup ↔ ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.Nodup ↔ ∀ (a : α), Multiset.count a s ≤ 1
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>DecidableEq α<GOAL>s.Nodup ↔ ∀ a ∈ s, Multiset.count a s = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>d : s.Nodup<VAR>h : a ∈ s<GOAL>Multiset.count a s = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>d : s.Nodup<GOAL>Multiset.count a s = if a ∈ s then 1 else 0
<VAR>α : Type u_4<VAR>s : Multiset α<GOAL>s.Nodup ↔ Multiset.Pairwise (fun x x_1 => x ≠ x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Multiset α<GOAL>(∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) → s.Nodup → Multiset.Pairwise r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Multiset α<VAR>H : Symmetric r<VAR>hs : Multiset.Pairwise r s<VAR>a : α<GOAL>a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≠ b → r a b
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>(s + t).Nodup ↔ s.Nodup ∧ t.Nodup ∧ s.Disjoint t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>d : (s + t).Nodup<GOAL>s.Disjoint t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>d₁ : s.Nodup<VAR>d₂ : t.Nodup<GOAL>(s + t).Nodup ↔ s.Disjoint t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>f : α → β<GOAL>(Multiset.map f s).Nodup → s.Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>f : α → β<GOAL>(∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → s.Nodup → (Multiset.map f s).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Multiset α<VAR>hf : Function.Injective f<GOAL>s.Nodup → (Multiset.map f s).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>f : α → β<VAR>d : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y<GOAL>(Multiset.map f s).Nodup ↔ s.Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>f : α → β<VAR>d : Function.Injective f<GOAL>(Multiset.map f s).Nodup ↔ s.Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Multiset α<GOAL>(Multiset.map f s).Nodup → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Multiset α<VAR>d : s.Nodup<GOAL>(Multiset.map f s).Nodup ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Multiset α<GOAL>s.Nodup → (Multiset.filter p s).Nodup
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s.attach.Nodup ↔ s.Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>s : Multiset α<VAR>H : ∀ a ∈ s, p a<VAR>hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b<GOAL>s.Nodup → (Multiset.pmap f s H).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>s.Nodup → s.erase a = Multiset.filter (fun x => x ≠ a) s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : Multiset α<GOAL>l.Nodup → (l.erase a).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>l : Multiset α<VAR>d : l.Nodup<GOAL>a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>h : s.Nodup<GOAL>a ∉ s.erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>f : α → Option β<VAR>H : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<GOAL>s.Nodup → (Multiset.filterMap f s).Nodup
<VAR>n : ℕ<GOAL>(Multiset.range n).Nodup
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>DecidableEq α<VAR>t : Multiset α<GOAL>s.Nodup → (s ∩ t).Nodup
<VAR>α : Type u_1<VAR>t : Multiset α<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>t.Nodup → (s ∩ t).Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(s ∪ t).Nodup ↔ s.Nodup ∧ t.Nodup
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s.Nodup → t.Nodup → (s = t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t)
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s.Nodup → (s ≤ t ↔ s ⊆ t)
<VAR>m n : ℕ<GOAL>Multiset.range m ≤ Multiset.range n ↔ m ≤ n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Multiset α<VAR>d : s.Nodup<GOAL>a ∈ s - t ↔ a ∈ s ∧ a ∉ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>s : Multiset α<VAR>t : Multiset β<VAR>hs : s.Nodup<VAR>ht : t.Nodup<VAR>i : (a : α) → a ∈ s → β<VAR>hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t<VAR>i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂<VAR>i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b<VAR>h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)<GOAL>Multiset.map f s = Multiset.map g t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>xs : List α<GOAL>(List.map f xs).sym2 = List.map (Sym2.map f) xs.sym2
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>z : Sym2 α<GOAL>z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
<VAR>α : Type u_1<VAR>xs : List α<GOAL>xs.sym2 = [] ↔ xs = []
<VAR>α : Type u_1<VAR>xs : List α<VAR>a b : α<VAR>h : s(a, b) ∈ xs.sym2<GOAL>a ∈ xs
<VAR>α : Type u_1<VAR>xs : List α<VAR>a b : α<VAR>h : s(a, b) ∈ xs.sym2<GOAL>b ∈ xs
<VAR>α : Type u_1<VAR>xs : List α<VAR>a b : α<VAR>ha : a ∈ xs<VAR>hb : b ∈ xs<GOAL>s(a, b) ∈ xs.sym2
<VAR>α : Type u_1<VAR>xs : List α<VAR>a b : α<GOAL>s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs
<VAR>α : Type u_1<VAR>xs : List α<VAR>z : Sym2 α<GOAL>z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs
<VAR>α : Type u_1<VAR>xs : List α<VAR>h : xs.Nodup<GOAL>xs.sym2.Nodup
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>h : x ∈ xs<GOAL>(List.map (fun y => s(x, y)) xs).Sublist xs.sym2
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>h : x ∉ xs<GOAL>(List.map (fun y => s(x, y)) xs).Disjoint xs.sym2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<GOAL>xs.sym2.dedup = xs.dedup.sym2
<VAR>α : Type u_1<VAR>xs ys : List α<VAR>h : xs.Perm ys<GOAL>xs.sym2.Perm ys.sym2
<VAR>α : Type u_1<VAR>xs ys : List α<VAR>h : xs.Sublist ys<GOAL>xs.sym2.Sublist ys.sym2
<VAR>α : Type u_1<VAR>xs ys : List α<VAR>h : xs.Subperm ys<GOAL>xs.sym2.Subperm ys.sym2
<VAR>α : Type u_1<VAR>xs : List α<GOAL>xs.sym2.length = (xs.length + 1).choose 2
<VAR>α : Type u_1<VAR>xs : List α<GOAL>List.sym 1 xs = List.map (fun x => x ::ₛ Sym.nil) xs
<VAR>α : Type u_1<VAR>xs : List α<GOAL>List.map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β<VAR>n : ℕ<VAR>xs : List α<GOAL>List.sym n (List.map f xs) = List.map (Sym.map f) (List.sym n xs)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>xs ys : List α<VAR>h : xs.Sublist ys<GOAL>(List.sym n xs).Sublist (List.sym n ys)
<VAR>α : Type u_1<VAR>xs : List α<VAR>n : ℕ<VAR>a : α<GOAL>(List.sym n xs).Sublist (List.sym n (a :: xs))
<VAR>α : Type u_1<VAR>n : ℕ<VAR>xs : List α<VAR>a : α<VAR>z : Sym α n<VAR>ha : a ∈ z<VAR>hz : z ∈ List.sym n xs<GOAL>a ∈ xs
<VAR>α : Type u_1<VAR>xs : List α<VAR>n : ℕ<VAR>a : α<VAR>z : Sym α n<VAR>h : a ::ₛ z ∈ List.sym (n + 1) xs<GOAL>a ∈ xs
<VAR>α : Type u_1<VAR>n : ℕ<VAR>xs : List α<VAR>h : xs.Nodup<GOAL>(List.sym n xs).Nodup
<VAR>α : Type u_1<VAR>n : ℕ<VAR>xs : List α<GOAL>(List.sym n xs).length = xs.length.multichoose n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>x : α<VAR>i : Fin (Multiset.count x m)<GOAL>(m.mkToType x i).fst = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>x : m.ToType<GOAL>x.fst ∈ m