ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>p : Quotient s₁ → Quotient s₂ → Prop<VAR>h : ∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)<VAR>q₁ : Quotient s₁<VAR>q₂ : Quotient s₂<GOAL>p q₁ q₂
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>p : Quotient s₁ → Prop<VAR>q : Quotient s₁<VAR>h : ∀ (a : α), p (Quotient.mk'' a)<GOAL>p q
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>p : Quotient s₁ → Quotient s₂ → Prop<VAR>q₁ : Quotient s₁<VAR>q₂ : Quotient s₂<VAR>h : ∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)<GOAL>p q₁ q₂
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>s₃ : Setoid γ<VAR>p : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop<VAR>q₁ : Quotient s₁<VAR>q₂ : Quotient s₂<VAR>q₃ : Quotient s₃<VAR>h : ∀ (a₁ : α) (a₂ : β) (a₃ : γ), p (Quotient.mk'' a₁) (Quotient.mk'' a₂) (Quotient.mk'' a₃)<GOAL>p q₁ q₂ q₃
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>φ : Quotient s₁ → Sort u_5<VAR>f : (a : α) → φ (Quotient.mk'' a)<VAR>c : ∀ (a₁ a₂ : α), a₁ ≈ a₂ → HEq (f a₁) (f a₂)<VAR>x : α<GOAL>(Quotient.mk'' x).hrecOn' f c = f x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>φ : Quotient s₁ → Quotient s₂ → Sort u_5<VAR>f : (a : α) → (b : β) → φ (Quotient.mk'' a) (Quotient.mk'' b)<VAR>c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → HEq (f a₁ b₁) (f a₂ b₂)<VAR>x : α<VAR>qb : Quotient s₂<GOAL>(Quotient.mk'' x).hrecOn₂' qb f c = qb.hrecOn' (f x) ⋯
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>f : α → β<VAR>h : (Setoid.r ⇒ Setoid.r) f f<VAR>x : α<GOAL>Quotient.map' f h (Quotient.mk'' x) = Quotient.mk'' (f x)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>s₃ : Setoid γ<VAR>f : α → β → γ<VAR>h : (Setoid.r ⇒ Setoid.r ⇒ Setoid.r) f f<VAR>x : α<GOAL>Quotient.map₂' f h (Quotient.mk'' x) = Quotient.map' (f x) ⋯
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>a b : α<GOAL>Quotient.mk'' a = Quotient.mk'' b → Setoid.r a b
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>a b : α<GOAL>Setoid.r a b → Quotient.mk'' a = Quotient.mk'' b
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>a b : α<GOAL>Quotient.mk' a = Quotient.mk' b ↔ Setoid.r a b
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>a b : α<GOAL>Quotient.mk'' a = Quotient.mk'' b ↔ Setoid.r a b
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>q : Quotient s₁<GOAL>Quotient.mk'' q.out' = q
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>a : α<GOAL>Setoid.r (Quotient.mk'' a).out' a
<VAR>α : Sort u_1<VAR>s : Setoid α<GOAL>Quotient.mk'' = Quotient.mk s
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>x : α<VAR>f : α → β<VAR>h : ∀ (a b : α), Setoid.r a b → f a = f b<GOAL>⟦x⟧.liftOn' f h = f x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>s : Setoid α<VAR>t : Setoid β<VAR>f : α → β → γ<VAR>h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), Setoid.r a₁ b₁ → Setoid.r a₂ b₂ → f a₁ a₂ = f b₁ b₂<VAR>a : α<VAR>b : β<GOAL>⟦a⟧.liftOn₂' ⟦b⟧ f h = f a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>t : Setoid β<VAR>f : α → β<VAR>h : (Setoid.r ⇒ Setoid.r) f f<VAR>x : α<GOAL>Quotient.map' f h ⟦x⟧ = ⟦f x⟧
<VAR>α : Type u_3<VAR>r : α → α → Prop<VAR>h : Equivalence r<VAR>x y : α<GOAL>Quot.mk r x = Quot.mk r y ↔ r x y
<VAR>n k : ℕ<GOAL>Fintype.card (Sym (Fin n) k) = n.multichoose k
<VAR>α : Type u_3<VAR>k : ℕ<VAR>Fintype α<VAR>Fintype (Sym α k)<GOAL>Fintype.card (Sym α k) = (Fintype.card α).multichoose k
<VAR>α : Type u_3<VAR>Fintype α<VAR>k : ℕ<VAR>Fintype (Sym α k)<GOAL>Fintype.card (Sym α k) = (Fintype.card α + k - 1).choose k
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(Finset.image Sym2.mk s.diag).card = s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>2 * (Finset.image Sym2.mk s.offDiag).card = s.offDiag.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(Finset.image Sym2.mk s.offDiag).card = s.card.choose 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<GOAL>Fintype.card { a // a.IsDiag } = Fintype.card α
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<GOAL>Fintype.card { a // ¬a.IsDiag } = (Fintype.card α).choose 2
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.card (Sym2 α) = (Fintype.card α + 1).choose 2
<VAR>α : Type u<VAR>s : Stream' α<GOAL>Stream'.cons s.head s.tail = s
<VAR>α : Type u<VAR>s₁ s₂ : Stream' α<GOAL>(∀ (n : ℕ), s₁.get n = s₂.get n) → s₁ = s₂
<VAR>α : Type u<VAR>a : α<VAR>s : Stream' α<GOAL>(Stream'.cons a s).get 0 = a
<VAR>α : Type u<VAR>a : α<VAR>s : Stream' α<GOAL>(Stream'.cons a s).head = a
<VAR>α : Type u<VAR>a : α<VAR>s : Stream' α<GOAL>(Stream'.cons a s).tail = s
<VAR>α : Type u<VAR>n m : ℕ<VAR>s : Stream' α<GOAL>(Stream'.drop m s).get n = s.get (n + m)
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.tail = Stream'.drop 1 s
<VAR>α : Type u<VAR>n m : ℕ<VAR>s : Stream' α<GOAL>Stream'.drop n (Stream'.drop m s) = Stream'.drop (n + m) s
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.tail.get n = s.get (n + 1)
<VAR>α : Type u<VAR>i : ℕ<VAR>s : Stream' α<GOAL>(Stream'.drop i s).tail = Stream'.drop (i + 1) s
<VAR>α : Type u<VAR>i : ℕ<VAR>s : Stream' α<GOAL>Stream'.drop i s.tail = Stream'.drop (i + 1) s
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>(Stream'.drop n s).tail = Stream'.drop n s.tail
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.get n.succ = s.tail.get n
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<VAR>x : α<GOAL>(Stream'.cons x s).get n.succ = s.get n
<VAR>α : Type u<VAR>s : Stream' α<GOAL>Stream'.drop 0 s = s
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>Stream'.drop n.succ s = Stream'.drop n s.tail
<VAR>α : Type u<VAR>a : Stream' α<VAR>n : ℕ<GOAL>(Stream'.drop n a).head = a.get n
<VAR>α : Type u<GOAL>Function.Injective2 Stream'.cons
<VAR>α : Type u<VAR>s : Stream' α<GOAL>Function.Injective fun x => Stream'.cons x s
<VAR>α : Type u<VAR>x : α<GOAL>Function.Injective (Stream'.cons x)
<VAR>α : Type u<VAR>p : α → Prop<VAR>s : Stream' α<GOAL>Stream'.All p s = ∀ (n : ℕ), p (s.get n)
<VAR>α : Type u<VAR>p : α → Prop<VAR>s : Stream' α<GOAL>Stream'.Any p s = ∃ n, p (s.get n)
<VAR>α : Type u<VAR>a : α<VAR>s : Stream' α<GOAL>a ∈ Stream'.cons a s
<VAR>α : Type u<VAR>a : α<VAR>s : Stream' α<VAR>b : α<GOAL>a ∈ s → a ∈ Stream'.cons b s
<VAR>α : Type u<VAR>a b : α<VAR>s : Stream' α<GOAL>a ∈ Stream'.cons b s → a = b ∨ a ∈ s
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<VAR>a : α<GOAL>a = s.get n → a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>n : ℕ<VAR>s : Stream' α<GOAL>Stream'.drop n (Stream'.map f s) = Stream'.map f (Stream'.drop n s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>n : ℕ<VAR>s : Stream' α<GOAL>(Stream'.map f s).get n = f (s.get n)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream' α<GOAL>(Stream'.map f s).tail = Stream'.map f s.tail
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream' α<GOAL>(Stream'.map f s).head = f s.head
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream' α<GOAL>Stream'.map f s = Stream'.cons (f s.head) (Stream'.map f s.tail)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Stream' α<GOAL>Stream'.map f (Stream'.cons a s) = Stream'.cons (f a) (Stream'.map f s)
<VAR>α : Type u<VAR>s : Stream' α<GOAL>Stream'.map id s = s
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>g : β → δ<VAR>f : α → β<VAR>s : Stream' α<GOAL>Stream'.map g (Stream'.map f s) = Stream'.map (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream' α<GOAL>Stream'.map f s.tail = (Stream'.map f s).tail
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Stream' α<GOAL>a ∈ s → f a ∈ Stream'.map f s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>b : β<VAR>s : Stream' α<GOAL>b ∈ Stream'.map f s → ∃ a, a ∈ s ∧ f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β → δ<VAR>n : ℕ<VAR>s₁ : Stream' α<VAR>s₂ : Stream' β<GOAL>Stream'.drop n (Stream'.zip f s₁ s₂) = Stream'.zip f (Stream'.drop n s₁) (Stream'.drop n s₂)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β → δ<VAR>n : ℕ<VAR>s₁ : Stream' α<VAR>s₂ : Stream' β<GOAL>(Stream'.zip f s₁ s₂).get n = f (s₁.get n) (s₂.get n)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β → δ<VAR>s₁ : Stream' α<VAR>s₂ : Stream' β<GOAL>(Stream'.zip f s₁ s₂).head = f s₁.head s₂.head
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β → δ<VAR>s₁ : Stream' α<VAR>s₂ : Stream' β<GOAL>(Stream'.zip f s₁ s₂).tail = Stream'.zip f s₁.tail s₂.tail
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β → δ<VAR>s₁ : Stream' α<VAR>s₂ : Stream' β<GOAL>Stream'.zip f s₁ s₂ = Stream'.cons (f s₁.head s₂.head) (Stream'.zip f s₁.tail s₂.tail)
<VAR>α : Type u<VAR>s : Stream' α<VAR>n : ℕ<GOAL>s.enum.get n = (n, s.get n)
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.enum = Stream'.zip Prod.mk Stream'.nats s
<VAR>α : Type u<VAR>a : α<GOAL>a ∈ Stream'.const a
<VAR>α : Type u<VAR>a : α<GOAL>Stream'.const a = Stream'.cons a (Stream'.const a)
<VAR>α : Type u<VAR>a : α<GOAL>(Stream'.const a).tail = Stream'.const a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>Stream'.map f (Stream'.const a) = Stream'.const (f a)
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<GOAL>(Stream'.const a).get n = a
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<GOAL>Stream'.drop n (Stream'.const a) = Stream'.const a
<VAR>α : Type u<VAR>f : α → α<VAR>a : α<GOAL>(Stream'.iterate f a).head = a
<VAR>α : Type u<VAR>n : ℕ<VAR>f : α → α<VAR>a : α<GOAL>(Stream'.iterate f a).get n.succ = f ((Stream'.iterate f a).get n)
<VAR>α : Type u<VAR>f : α → α<VAR>a : α<GOAL>(Stream'.iterate f a).tail = Stream'.iterate f (f a)
<VAR>α : Type u<VAR>f : α → α<VAR>a : α<GOAL>Stream'.iterate f a = Stream'.cons a (Stream'.iterate f (f a))
<VAR>α : Type u<VAR>f : α → α<VAR>a : α<GOAL>(Stream'.iterate f a).get 0 = a
<VAR>α : Type u<VAR>n : ℕ<VAR>f : α → α<VAR>a : α<GOAL>(Stream'.iterate f a).get n.succ = (Stream'.iterate f (f a)).get n
<VAR>α : Type u<VAR>R : Stream' α → Stream' α → Prop<VAR>bisim : Stream'.IsBisimulation R<VAR>s₁ s₂ : Stream' α<VAR>n : ℕ<GOAL>R s₁ s₂ → s₁.get n = s₂.get n ∧ R (Stream'.drop (n + 1) s₁) (Stream'.drop (n + 1) s₂)
<VAR>α : Type u<VAR>R : Stream' α → Stream' α → Prop<VAR>bisim : Stream'.IsBisimulation R<VAR>s₁ s₂ : Stream' α<GOAL>R s₁ s₂ → s₁ = s₂
<VAR>α : Type u<VAR>s₁ s₂ : Stream' α<GOAL>s₁.head = s₂.head → s₁ = s₁.tail → s₂ = s₂.tail → s₁ = s₂
<VAR>α : Type u<VAR>s₁ s₂ : Stream' α<GOAL>s₁.head = s₂.head → (∀ (β : Type u) (fr : Stream' α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂
<VAR>α : Type u<VAR>a : α<GOAL>Stream'.iterate id a = Stream'.const a
<VAR>α : Type u<VAR>f : α → α<VAR>a : α<GOAL>Stream'.iterate f (f a) = Stream'.map f (Stream'.iterate f a)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : α → α<VAR>a : α<GOAL>Stream'.corec f g a = Stream'.map f (Stream'.iterate g a)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : α → α<VAR>a : α<GOAL>Stream'.corec f g a = Stream'.cons (f a) (Stream'.corec f g (g a))
<VAR>α : Type u<VAR>a : α<GOAL>Stream'.corec id id a = Stream'.const a
<VAR>α : Type u<VAR>f : α → α<VAR>a : α<GOAL>Stream'.corec id f a = Stream'.iterate f a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β × α<VAR>a : α<GOAL>Stream'.corec' f a = Stream'.cons (f a).1 (Stream'.corec' f (f a).2)
<VAR>α : Type u<VAR>β : Type v<VAR>g : α → β<VAR>f : α → α<VAR>a : α<GOAL>Stream'.unfolds g f a = Stream'.cons (g a) (Stream'.unfolds g f (f a))
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>(Stream'.unfolds Stream'.head Stream'.tail s).get n = s.get n
<VAR>α : Type u<VAR>s : Stream' α<GOAL>Stream'.unfolds Stream'.head Stream'.tail s = s
<VAR>α : Type u<VAR>s₁ s₂ : Stream' α<GOAL>s₁ ⋈ s₂ = Stream'.cons s₁.head (Stream'.cons s₂.head (s₁.tail ⋈ s₂.tail))
<VAR>α : Type u<VAR>s₁ s₂ : Stream' α<GOAL>(s₁ ⋈ s₂).tail = s₂ ⋈ s₁.tail
<VAR>α : Type u<VAR>s₁ s₂ : Stream' α<GOAL>s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail
<VAR>α : Type u<VAR>n : ℕ<VAR>s₁ s₂ : Stream' α<GOAL>(s₁ ⋈ s₂).get (2 * n) = s₁.get n
<VAR>α : Type u<VAR>n : ℕ<VAR>s₁ s₂ : Stream' α<GOAL>(s₁ ⋈ s₂).get (2 * n + 1) = s₂.get n
<VAR>α : Type u<VAR>a : α<VAR>s₁ : Stream' α<VAR>s₂ : Stream' α<GOAL>a ∈ s₁ → a ∈ s₁ ⋈ s₂
<VAR>α : Type u<VAR>a : α<VAR>s₁ : Stream' α<VAR>s₂ : Stream' α<GOAL>a ∈ s₂ → a ∈ s₁ ⋈ s₂
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.odd = s.tail.even
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.even.head = s.head
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.even.tail = s.tail.tail.even
<VAR>α : Type u<VAR>a₁ a₂ : α<VAR>s : Stream' α<GOAL>(Stream'.cons a₁ (Stream'.cons a₂ s)).even = Stream'.cons a₁ s.even
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.tail.even = s.odd
<VAR>α : Type u<VAR>s₁ s₂ : Stream' α<GOAL>(s₁ ⋈ s₂).even = s₁
<VAR>α : Type u<VAR>s₁ : Stream' α<GOAL>s₁.even ⋈ s₁.odd = s₁
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.even.get n = s.get (2 * n)
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.odd.get n = s.get (2 * n + 1)
<VAR>α : Type u<VAR>a : α<VAR>s : Stream' α<GOAL>a ∈ s.even → a ∈ s
<VAR>α : Type u<VAR>a : α<VAR>s : Stream' α<GOAL>a ∈ s.odd → a ∈ s
<VAR>α : Type u<VAR>s : Stream' α<GOAL>[] ++ₛ s = s
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>s : Stream' α<GOAL>a :: l ++ₛ s = Stream'.cons a (l ++ₛ s)
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>s : Stream' α<GOAL>l₁ ++ l₂ ++ₛ s = l₁ ++ₛ (l₂ ++ₛ s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<VAR>s : Stream' α<GOAL>Stream'.map f (l ++ₛ s) = List.map f l ++ₛ Stream'.map f s
<VAR>α : Type u<VAR>l : List α<VAR>s : Stream' α<GOAL>Stream'.drop l.length (l ++ₛ s) = s
<VAR>α : Type u<VAR>s : Stream' α<GOAL>[s.head] ++ₛ s.tail = s
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>s : Stream' α<GOAL>a ∈ s → a ∈ l ++ₛ s
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>s : Stream' α<GOAL>a ∈ l → a ∈ l ++ₛ s
<VAR>α : Type u<VAR>s : Stream' α<GOAL>Stream'.take 0 s = []
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>Stream'.take n.succ s = s.head :: Stream'.take n s.tail
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<VAR>s : Stream' α<GOAL>Stream'.take (n + 1) (Stream'.cons a s) = a :: Stream'.take n s
<VAR>α : Type u<VAR>s : Stream' α<VAR>n : ℕ<GOAL>Stream'.take (n + 1) s = Stream'.take n s ++ [s.get n]
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>(Stream'.take n s).length = n
<VAR>α : Type u<VAR>s : Stream' α<VAR>m n : ℕ<GOAL>List.take m (Stream'.take n s) = Stream'.take (min n m) s
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>Stream'.take n s ++ [s.get n] = Stream'.take (n + 1) s
<VAR>α : Type u<VAR>s : Stream' α<VAR>k n : ℕ<GOAL>k < n → (Stream'.take n s).get? k = some (s.get k)
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>(Stream'.take n.succ s).get? n = some (s.get n)
<VAR>α : Type u<VAR>n : ℕ<VAR>xs : Stream' α<GOAL>(Stream'.take n xs).dropLast = Stream'.take (n - 1) xs
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>Stream'.take n s ++ₛ Stream'.drop n s = s
<VAR>α : Type u<VAR>s₁ s₂ : Stream' α<GOAL>(∀ (n : ℕ), Stream'.take n s₁ = Stream'.take n s₂) → s₁ = s₂
<VAR>α : Type u<VAR>a a₁ : α<VAR>l₁ : List α<VAR>a₀ : α<VAR>l₀ : List α<GOAL>Stream'.cycleG (a, a₁ :: l₁, a₀, l₀) = (a₁, l₁, a₀, l₀)
<VAR>α : Type u<VAR>l : List α<VAR>h : l ≠ []<GOAL>Stream'.cycle l h = l ++ₛ Stream'.cycle l h
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>h : l ≠ []<GOAL>a ∈ l → a ∈ Stream'.cycle l h
<VAR>α : Type u<VAR>a : α<GOAL>Stream'.cycle [a] ⋯ = Stream'.const a
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.tails = Stream'.cons s.tail s.tail.tails
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.tails.get n = Stream'.drop n s.tail
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.tails = Stream'.iterate Stream'.tail s.tail
<VAR>α : Type u<VAR>l : List α<VAR>s : Stream' α<GOAL>Stream'.initsCore l s = Stream'.cons l (Stream'.initsCore (l ++ [s.head]) s.tail)
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.inits.tail = Stream'.initsCore [s.head, s.tail.head] s.tail.tail
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.tail.inits = Stream'.initsCore [s.tail.head] s.tail.tail
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<VAR>l : List α<VAR>s : Stream' α<GOAL>a :: (Stream'.initsCore l s).get n = (Stream'.initsCore (a :: l) s).get n
<VAR>α : Type u<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.inits.get n = Stream'.take n.succ s
<VAR>α : Type u<VAR>s : Stream' α<GOAL>s.inits = Stream'.cons [s.head] (Stream'.map (List.cons s.head) s.tail.inits)
<VAR>α : Type u<VAR>s : Stream' α<GOAL>Stream'.zip Stream'.appendStream' s.inits s.tails = Stream'.const s
<VAR>α : Type u<VAR>s : Stream' α<GOAL>Stream'.pure id ⊛ s = s
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>g : Stream' (β → δ)<VAR>f : Stream' (α → β)<VAR>s : Stream' α<GOAL>Stream'.pure Function.comp ⊛ g ⊛ f ⊛ s = g ⊛ (f ⊛ s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>Stream'.pure f ⊛ Stream'.pure a = Stream'.pure (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>fs : Stream' (α → β)<VAR>a : α<GOAL>fs ⊛ Stream'.pure a = (Stream'.pure fun f => f a) ⊛ fs
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream' α<GOAL>Stream'.map f s = Stream'.pure f ⊛ s
<VAR>n : ℕ<GOAL>Stream'.nats.get n = n
<GOAL>Stream'.nats = Stream'.cons 0 (Stream'.map Nat.succ Stream'.nats)
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>Function.Injective Sym.toMultiset
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s₁ s₂ : Sym α n<GOAL>↑s₁ = ↑s₂ ↔ s₁ = s₂
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s₁ s₂ : Sym α n<VAR>h : ↑s₁ = ↑s₂<GOAL>s₁ = s₂
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<GOAL>↑s = ↑s
<VAR>α : Type u_1<GOAL>↑Sym.nil = 0
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>s s' : Sym α n<GOAL>a ::ₛ s = a ::ₛ s' ↔ s = s'
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a a' : α<VAR>s : Sym α n<GOAL>a ::ₛ s = a' ::ₛ s ↔ a = a'
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a b : α<VAR>s : Sym α n<GOAL>a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<VAR>a : α<GOAL>↑(a ::ₛ s) = a ::ₘ ↑s
<VAR>α : Type u_1<GOAL>Sym.ofVector Mathlib.Vector.nil = Sym.nil
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>Sym.ofVector (a ::ᵥ v) = a ::ₛ Sym.ofVector v
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<GOAL>Multiset.card ↑s = n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Multiset α<VAR>h : Multiset.card s = n<GOAL>↑(Sym.mk s h) = s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>s : Multiset α<VAR>h : Multiset.card s = n<GOAL>a ∈ Sym.mk s h ↔ a ∈ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>p : Sym α n → Prop<GOAL>(∀ (s : Sym α n), p s) ↔ ∀ (s : Multiset α) (hs : Multiset.card s = n), p (Sym.mk s hs)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>p : Sym α n → Prop<GOAL>(∃ s, p s) ↔ ∃ s, ∃ (hs : Multiset.card s = n), p (Sym.mk s hs)
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∉ Sym.nil
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<VAR>a b : α<GOAL>a ∈ b ::ₛ s ↔ a = b ∨ a ∈ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<VAR>a : α<GOAL>a ∈ ↑s ↔ a ∈ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<VAR>a b : α<VAR>h : a ∈ s<GOAL>a ∈ b ::ₛ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>s : Sym α n<GOAL>a ∈ a ::ₛ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>a ::ₛ Sym.ofVector v = Sym.ofVector (a ::ᵥ v)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a b : Mathlib.Vector α n<VAR>h : (↑a).Perm ↑b<GOAL>Sym.ofVector a = Sym.ofVector b
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>m : Multiset α<VAR>hc : Multiset.card m = n + 1<VAR>a : α<VAR>h : a ∈ m<GOAL>(Sym.mk m hc).erase a h = Sym.mk (m.erase a) ⋯
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>s : Sym α n.succ<VAR>a : α<VAR>h : a ∈ s<GOAL>↑(s.erase a h) = (↑s).erase a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>s : Sym α n.succ<VAR>a : α<VAR>h : a ∈ s<GOAL>a ::ₛ s.erase a h = s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>s : Sym α n<VAR>a : α<VAR>h : a ∈ a ::ₛ s := ⋯<GOAL>(a ::ₛ s).erase a h = s
<VAR>α : Type u_3<VAR>n : ℕ<VAR>a : α<VAR>s : Sym α n<GOAL>Sym.cons' a (Sym.symEquivSym' s) = Sym.symEquivSym' (a ::ₛ s)
<VAR>α : Type u_1<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>s : Sym α 0<GOAL>s = Sym.nil
<VAR>α : Type u_1<VAR>a : α<VAR>n : ℕ<GOAL>Sym.replicate n.succ a = a ::ₛ Sym.replicate n a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<GOAL>↑(Sym.replicate n a) = Multiset.replicate n a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a b : α<GOAL>b ∈ Sym.replicate n a ↔ n ≠ 0 ∧ b = a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<VAR>a : α<GOAL>s = Sym.replicate n a ↔ ∀ b ∈ s, b = a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n.succ<GOAL>∃ a, a ∈ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α (n + 1)<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ t, s = a ::ₛ t
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n.succ<GOAL>∃ a s', s = a ::ₛ s'
<VAR>α : Type u_1<VAR>a : α<VAR>n : ℕ<VAR>s : Sym α n<GOAL>s = Sym.replicate n a ↔ ∀ b ∈ s, b = a
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>a : α<VAR>n : ℕ<VAR>s : Sym α n<GOAL>s = Sym.replicate n a
<VAR>α : Type u_1<VAR>a b : α<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Sym.replicate n a = Sym.replicate n b ↔ a = b
<VAR>α : Type u_1<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Function.Injective (Sym.replicate n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>f : α → β<VAR>b : β<VAR>l : Sym α n<GOAL>b ∈ Sym.map f l ↔ ∃ a ∈ l, f a = b
<VAR>α : Type u_3<VAR>n : ℕ<VAR>s : Sym α n<GOAL>Sym.map (fun x => x) s = s
<VAR>α : Type u_3<VAR>n : ℕ<VAR>s : Sym α n<GOAL>Sym.map id s = s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>n : ℕ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Sym α n<GOAL>Sym.map g (Sym.map f s) = Sym.map (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Sym.map f 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>f : α → β<VAR>a : α<VAR>s : Sym α n<GOAL>Sym.map f (a ::ₛ s) = f a ::ₛ Sym.map f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>f g : α → β<VAR>s : Sym α n<VAR>h : ∀ x ∈ s, f x = g x<GOAL>Sym.map f s = Sym.map g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>f : α → β<VAR>m : Multiset α<VAR>hc : Multiset.card m = n<GOAL>Sym.map f (Sym.mk m hc) = Sym.mk (Multiset.map f m) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>s : Sym α n<VAR>f : α → β<GOAL>↑(Sym.map f s) = Multiset.map f ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>n : ℕ<GOAL>Function.Injective (Sym.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>e : α ≃ β<VAR>x : Sym β n<GOAL>(Sym.equivCongr e).symm x = Sym.map (⇑e.symm) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>e : α ≃ β<VAR>x : Sym α n<GOAL>(Sym.equivCongr e) x = Sym.map (⇑e) x
<VAR>α : Type u_1<VAR>n : ℕ<VAR>m : Multiset α<VAR>hc : Multiset.card m = n<GOAL>(Sym.mk m hc).attach = Sym.mk m.attach ⋯
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<GOAL>↑s.attach = (↑s).attach
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<GOAL>Sym.map Subtype.val s.attach = s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<VAR>x : { x // x ∈ s }<GOAL>x ∈ s.attach
<VAR>α : Type u_1<GOAL>Sym.nil.attach = Sym.nil
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>s : Sym α n<GOAL>(x ::ₛ s).attach = ⟨x, ⋯⟩ ::ₛ Sym.map (fun x_1 => ⟨↑x_1, ⋯⟩) s.attach
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n<GOAL>(Sym.cast ⋯) s = s
<VAR>α : Type u_1<VAR>n n' : ℕ<VAR>s : Sym α n<VAR>n'' : ℕ<VAR>h : n = n'<VAR>h' : n' = n''<GOAL>(Sym.cast h') ((Sym.cast h) s) = (Sym.cast ⋯) s
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>s : Sym α n<VAR>h : n = m<GOAL>↑((Sym.cast h) s) = ↑s
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>s : Sym α n<VAR>a : α<VAR>h : n = m<GOAL>a ∈ (Sym.cast h) s ↔ a ∈ s
<VAR>α : Type u_1<VAR>n n' : ℕ<VAR>s : Sym α n<VAR>t t' : Sym α n'<GOAL>s.append t = s.append t' ↔ t = t'
<VAR>α : Type u_1<VAR>n n' : ℕ<VAR>s s' : Sym α n<VAR>t : Sym α n'<GOAL>s.append t = s'.append t ↔ s = s'
<VAR>α : Type u_1<VAR>n' : ℕ<VAR>s s' : Sym α n'<GOAL>s.append s' = (Sym.cast ⋯) (s'.append s)
<VAR>α : Type u_1<VAR>n n' : ℕ<VAR>s : Sym α n<VAR>s' : Sym α n'<GOAL>↑(s.append s') = ↑s + ↑s'
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>s : Sym α n<VAR>a : α<VAR>s' : Sym α m<GOAL>a ∈ s.append s' ↔ a ∈ s ∨ a ∈ s'
<VAR>α : Type u_1<VAR>a : α<GOAL>Sym.oneEquiv a = ⟨{a}, ⋯⟩
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<GOAL>↑(Sym.fill a i m) = ↑m + ↑(Sym.replicate (↑i) a)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a b : α<VAR>i : Fin (n + 1)<VAR>s : Sym α (n - ↑i)<GOAL>a ∈ Sym.fill b i s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)<VAR>h : ↑m₁.snd = ↑m₂.snd<GOAL>m₁ = m₂
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>a : α<VAR>m : Sym α n<GOAL>Sym.fill a (Sym.filterNe a m).fst (Sym.filterNe a m).snd = m
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>a : α<VAR>m : (i : Fin (n + 1)) × Sym α (n - ↑i)<VAR>h : a ∉ m.snd<GOAL>Sym.filterNe a (Sym.fill a m.fst m.snd) = m
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>a : α<VAR>i : Fin (n + 1)<VAR>s : Sym α (n - ↑i)<VAR>hx : a ∉ s<GOAL>Multiset.count a ↑(Sym.fill a i s) = ↑i