ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>R : Type u_11<VAR>AddMonoid M<VAR>DistribSMul R M<VAR>AddCommMonoid N<VAR>g : α →₀ M<VAR>b : R<VAR>h : α → M → N<VAR>h0 : ∀ (i : α), h i 0 = 0<GOAL>(b • g).sum h = g.sum fun i c => h i (b • c)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>R : Type u_11<VAR>AddMonoid M<VAR>AddCommMonoid N<VAR>DistribSMul R M<VAR>g : α →₀ M<VAR>b : R<VAR>h : α → M →+ N<GOAL>((b • g).sum fun a => ⇑(h a)) = g.sum fun i c => (h i) (b • c)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>R : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>DistribMulAction R M<VAR>DistribMulAction R N<VAR>f g : (α →₀ M) →+[R] N<VAR>h : ∀ (a : α) (m : M), f (Finsupp.single a m) = g (Finsupp.single a m)<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>R : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>DistribMulAction R M<VAR>DistribMulAction R N<VAR>f g : (α →₀ M) →+[R] N<VAR>h : ∀ (a : α), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<VAR>g : { a // ¬P a } →₀ M<GOAL>(f.piecewise g).support = (Finset.map (Function.Embedding.subtype P) f.support).disjUnion (Finset.map (Function.Embedding.subtype fun a => ¬P a) g.support) ⋯
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<VAR>g : { a // ¬P a } →₀ M<VAR>a : α<GOAL>(f.piecewise g) a = if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<VAR>g : { a // ¬P a } →₀ M<GOAL>Finsupp.subtypeDomain P (f.piecewise g) = f
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<VAR>g : { a // ¬P a } →₀ M<GOAL>Finsupp.subtypeDomain (fun x => ¬P x) (f.piecewise g) = g
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<VAR>a : α<GOAL>f.extendDomain a = if h : P a then f ⟨a, h⟩ else 0
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<GOAL>f.extendDomain.support = Finset.map (Function.Embedding.subtype P) f.support
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<GOAL>f.extendDomain = Finsupp.embDomain (Function.Embedding.subtype P) f
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<GOAL>↑f.extendDomain.support ⊆ {x | P x}
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : Subtype P →₀ M<GOAL>Finsupp.subtypeDomain P f.extendDomain = f
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>f : α →₀ M<VAR>hf : ∀ a ∈ f.support, P a<GOAL>(Finsupp.subtypeDomain P f).extendDomain = f
<VAR>α : Type u_1<VAR>M : Type u_13<VAR>Zero M<VAR>P : α → Prop<VAR>DecidablePred P<VAR>a : Subtype P<VAR>m : M<GOAL>(Finsupp.single a m).extendDomain = Finsupp.single (↑a) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>e : α ≃ β<VAR>l : α →₀ M<GOAL>(Finsupp.domCongr e) l = Finsupp.equivMapDomain e l
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<GOAL>Finsupp.domCongr (Equiv.refl α) = AddEquiv.refl (α →₀ M)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>e : α ≃ β<GOAL>(Finsupp.domCongr e).symm = Finsupp.domCongr e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>e : α ≃ β<VAR>f : β ≃ γ<GOAL>(Finsupp.domCongr e).trans (Finsupp.domCongr f) = Finsupp.domCongr (e.trans f)
<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>αs : ι → Type u_13<VAR>Zero M<VAR>l : (i : ι) × αs i →₀ M<VAR>i : ι<VAR>x : αs i<GOAL>(l.split i) x = l ⟨i, x⟩
<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>αs : ι → Type u_13<VAR>Zero M<VAR>l : (i : ι) × αs i →₀ M<VAR>i : ι<GOAL>i ∈ l.splitSupport ↔ l.split i ≠ 0
<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>αs : ι → Type u_13<VAR>Zero M<VAR>l : (i : ι) × αs i →₀ M<GOAL>l.support = l.splitSupport.sigma fun i => (l.split i).support
<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>N : Type u_7<VAR>αs : ι → Type u_13<VAR>Zero M<VAR>l : (i : ι) × αs i →₀ M<VAR>AddCommMonoid N<VAR>f : (i : ι) × αs i → M → N<GOAL>l.sum f = ∑ i ∈ l.splitSupport, (l.split i).sum fun a b => f ⟨i, a⟩ b
<VAR>α : Type u_1<VAR>η : Type u_14<VAR>Fintype η<VAR>ιs : η → Type u_15<VAR>Zero α<VAR>f : (j : η) × ιs j →₀ α<VAR>j : η<VAR>i : ιs j<GOAL>(Finsupp.sigmaFinsuppEquivPiFinsupp f j) i = f ⟨j, i⟩
<VAR>η : Type u_14<VAR>Fintype η<VAR>α : Type u_16<VAR>ιs : η → Type u_17<VAR>AddMonoid α<VAR>f : (j : η) × ιs j →₀ α<VAR>j : η<VAR>i : ιs j<GOAL>(Finsupp.sigmaFinsuppAddEquivPiFinsupp f j) i = f ⟨j, i⟩
<VAR>α : Type u<VAR>a : α<GOAL>¬a ∈ Stream'.WSeq.nil
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>self : s.IsFinite<GOAL>s.toList.Terminates
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>self : s.Productive<VAR>n : ℕ<GOAL>(s.get? n).Terminates
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.Productive ↔ ∀ (n : ℕ), (s.get? n).Terminates
<VAR>α : Type u<VAR>β : Type v<VAR>R S : α → β → Prop<VAR>C D : Stream'.WSeq α → Stream'.WSeq β → Prop<VAR>H1 : ∀ (a : α) (b : β), R a b → S a b<VAR>H2 : ∀ (s : Stream'.WSeq α) (t : Stream'.WSeq β), C s t → D s t<VAR>o : Option (α × Stream'.WSeq α)<VAR>p : Option (β × Stream'.WSeq β)<GOAL>Stream'.WSeq.LiftRelO R C o p → Stream'.WSeq.LiftRelO S D o p
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C D : Stream'.WSeq α → Stream'.WSeq β → Prop<VAR>H : ∀ (s : Stream'.WSeq α) (t : Stream'.WSeq β), C s t → D s t<VAR>o : Option (α × Stream'.WSeq α)<VAR>p : Option (β × Stream'.WSeq β)<GOAL>Stream'.WSeq.LiftRelO R C o p → Stream'.WSeq.LiftRelO R D o p
<VAR>α : Type u<VAR>R S : Stream'.WSeq α → Stream'.WSeq α → Prop<VAR>H : ∀ (s t : Stream'.WSeq α), R s t → S s t<VAR>o p : Option (α × Stream'.WSeq α)<GOAL>Stream'.WSeq.BisimO R o p → Stream'.WSeq.BisimO S o p
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s : Stream'.WSeq α<VAR>t : Stream'.WSeq β<GOAL>Stream'.WSeq.LiftRel R s t → Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) s.destruct t.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s : Stream'.WSeq α<VAR>t : Stream'.WSeq β<GOAL>Stream'.WSeq.LiftRel R s t ↔ Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) s.destruct t.destruct
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<GOAL>s ~ʷ t → Computation.LiftRel (Stream'.WSeq.BisimO fun x x_1 => x ~ʷ x_1) s.destruct t.destruct
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<GOAL>s ~ʷ t ↔ Computation.LiftRel (Stream'.WSeq.BisimO fun x x_1 => x ~ʷ x_1) s.destruct t.destruct
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>H : Reflexive R<GOAL>Reflexive (Stream'.WSeq.LiftRel R)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>C : Stream'.WSeq α → Stream'.WSeq β → Prop<GOAL>Function.swap (Stream'.WSeq.LiftRelO R C) = Stream'.WSeq.LiftRelO (Function.swap R) (Function.swap C)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s1 : Stream'.WSeq α<VAR>s2 : Stream'.WSeq β<VAR>h : Stream'.WSeq.LiftRel R s1 s2<GOAL>Stream'.WSeq.LiftRel (Function.swap R) s2 s1
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<GOAL>Function.swap (Stream'.WSeq.LiftRel R) = Stream'.WSeq.LiftRel (Function.swap R)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>H : Symmetric R<GOAL>Symmetric (Stream'.WSeq.LiftRel R)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>H : Transitive R<GOAL>Transitive (Stream'.WSeq.LiftRel R)
<VAR>α : Type u<VAR>R : α → α → Prop<GOAL>Equivalence R → Equivalence (Stream'.WSeq.LiftRel R)
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s ~ʷ s
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<GOAL>s ~ʷ t → t ~ʷ s
<VAR>α : Type u<VAR>s t u : Stream'.WSeq α<GOAL>s ~ʷ t → t ~ʷ u → s ~ʷ u
<VAR>α : Type u<GOAL>Equivalence Stream'.WSeq.Equiv
<VAR>α : Type u<GOAL>Stream'.WSeq.nil.destruct = Computation.pure none
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.WSeq α<GOAL>(Stream'.WSeq.cons a s).destruct = Computation.pure (some (a, s))
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.think.destruct = s.destruct.think
<VAR>α : Type u<GOAL>Stream'.Seq.destruct Stream'.WSeq.nil = none
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.WSeq α<GOAL>Stream'.Seq.destruct (Stream'.WSeq.cons a s) = some (some a, s)
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>Stream'.Seq.destruct s.think = some (none, s)
<VAR>α : Type u<GOAL>Stream'.WSeq.nil.head = Computation.pure none
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.WSeq α<GOAL>(Stream'.WSeq.cons a s).head = Computation.pure (some a)
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.think.head = s.head.think
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>Stream'.WSeq.flatten (Computation.pure s) = s
<VAR>α : Type u<VAR>c : Computation (Stream'.WSeq α)<GOAL>Stream'.WSeq.flatten c.think = (Stream'.WSeq.flatten c).think
<VAR>α : Type u<VAR>c : Computation (Stream'.WSeq α)<GOAL>(Stream'.WSeq.flatten c).destruct = c >>= Stream'.WSeq.destruct
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.head.Terminates ↔ s.destruct.Terminates
<VAR>α : Type u<GOAL>Stream'.WSeq.nil.tail = Stream'.WSeq.nil
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.WSeq α<GOAL>(Stream'.WSeq.cons a s).tail = s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.think.tail = s.tail.think
<VAR>α : Type u<VAR>n : ℕ<GOAL>Stream'.WSeq.nil.drop n = Stream'.WSeq.nil
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.WSeq α<VAR>n : ℕ<GOAL>(Stream'.WSeq.cons a s).drop (n + 1) = s.drop n
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>n : ℕ<GOAL>s.think.drop n = (s.drop n).think
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>m n : ℕ<GOAL>s.drop (m + n) = (s.drop m).drop n
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>n : ℕ<GOAL>s.tail.drop n = s.drop (n + 1)
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>m n : ℕ<GOAL>s.get? (m + n) = (s.drop m).get? n
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>n : ℕ<GOAL>s.tail.get? n = s.get? (n + 1)
<VAR>α : Type u<GOAL>Stream'.WSeq.nil.join = Stream'.WSeq.nil
<VAR>α : Type u<VAR>S : Stream'.WSeq (Stream'.WSeq α)<GOAL>S.think.join = S.join.think
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>S : Stream'.WSeq (Stream'.WSeq α)<GOAL>(Stream'.WSeq.cons s S).join = (s.append S.join).think
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>Stream'.WSeq.nil.append s = s
<VAR>α : Type u<VAR>a : α<VAR>s t : Stream'.WSeq α<GOAL>(Stream'.WSeq.cons a s).append t = Stream'.WSeq.cons a (s.append t)
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<GOAL>s.think.append t = (s.append t).think
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.append Stream'.WSeq.nil = s
<VAR>α : Type u<VAR>s t u : Stream'.WSeq α<GOAL>(s.append t).append u = s.append (t.append u)
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.tail.destruct = s.destruct >>= Stream'.WSeq.tail.aux
<VAR>α : Type u<VAR>n : ℕ<GOAL>Stream'.WSeq.drop.aux n none = Computation.pure none
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>n : ℕ<GOAL>(s.drop n).destruct = s.destruct >>= Stream'.WSeq.drop.aux n
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>T : s.tail.head.Terminates<GOAL>s.head.Terminates
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α × Stream'.WSeq α<VAR>h : some a ∈ s.tail.destruct<GOAL>∃ a', some a' ∈ s.destruct
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<VAR>h : some a ∈ s.tail.head<GOAL>∃ a', some a' ∈ s.head
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<VAR>n : ℕ<VAR>h : some a ∈ s.get? n<GOAL>∃ a', some a' ∈ s.head
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(s.get? n).Terminates → (s.get? m).Terminates
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>n : ℕ<GOAL>(s.get? n).Terminates → s.head.Terminates
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>n : ℕ<VAR>T : (s.get? n).Terminates<GOAL>s.destruct.Terminates
<VAR>α : Type u<VAR>C : Stream'.WSeq α → Prop<VAR>a : α<VAR>s : Stream'.WSeq α<VAR>M : a ∈ s<VAR>h1 : ∀ (b : α) (s' : Stream'.WSeq α), a = b ∨ C s' → C (Stream'.WSeq.cons b s')<VAR>h2 : ∀ (s : Stream'.WSeq α), C s → C s.think<GOAL>C s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<GOAL>a ∈ s.think ↔ a ∈ s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a a' : α<VAR>s' : Stream'.WSeq α<GOAL>some (a', s') ∈ s.destruct → (a ∈ s ↔ a = a' ∨ a ∈ s')
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>b : α<VAR>a : α<GOAL>a ∈ Stream'.WSeq.cons b s ↔ a = b ∨ a ∈ s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>b : α<VAR>a : α<VAR>h : a ∈ s<GOAL>a ∈ Stream'.WSeq.cons b s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<GOAL>a ∈ Stream'.WSeq.cons a s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<GOAL>a ∈ s.tail → a ∈ s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ s.drop n → a ∈ s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<VAR>n : ℕ<GOAL>some a ∈ s.get? n → a ∈ s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ n, some a ∈ s.get? n
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ n s', some (a, s') ∈ (s.drop n).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s : Stream'.WSeq α<VAR>t : Stream'.WSeq β<VAR>H : Stream'.WSeq.LiftRel R s t<VAR>n : ℕ<GOAL>Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) (s.drop n).destruct (t.drop n).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s : Stream'.WSeq α<VAR>t : Stream'.WSeq β<VAR>H : Stream'.WSeq.LiftRel R s t<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ b, b ∈ t ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s : Stream'.WSeq α<VAR>t : Stream'.WSeq β<VAR>H : Stream'.WSeq.LiftRel R s t<VAR>b : β<VAR>h : b ∈ t<GOAL>∃ a, a ∈ s ∧ R a b
<VAR>α : Type u<VAR>s : Stream'.WSeq α<VAR>a : α<VAR>h : a ∈ s<GOAL>s.head.Terminates
<VAR>α : Type u<VAR>s₁ s₂ : Stream'.WSeq α<VAR>a : α<GOAL>a ∈ s₁.append s₂ → a ∈ s₁ ∨ a ∈ s₂
<VAR>α : Type u<VAR>s₁ s₂ : Stream'.WSeq α<VAR>a : α<GOAL>a ∈ s₁ → a ∈ s₁.append s₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>b : β<VAR>s : Stream'.WSeq α<GOAL>b ∈ Stream'.WSeq.map f s → ∃ a, a ∈ s ∧ f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<GOAL>Stream'.WSeq.LiftRel R Stream'.WSeq.nil Stream'.WSeq.nil
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>s : Stream'.WSeq α<VAR>t : Stream'.WSeq β<GOAL>Stream'.WSeq.LiftRel R (Stream'.WSeq.cons a s) (Stream'.WSeq.cons b t) ↔ R a b ∧ Stream'.WSeq.LiftRel R s t
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s : Stream'.WSeq α<VAR>t : Stream'.WSeq β<GOAL>Stream'.WSeq.LiftRel R s.think t ↔ Stream'.WSeq.LiftRel R s t
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s : Stream'.WSeq α<VAR>t : Stream'.WSeq β<GOAL>Stream'.WSeq.LiftRel R s t.think ↔ Stream'.WSeq.LiftRel R s t
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<VAR>a : α<VAR>h : s ~ʷ t<GOAL>Stream'.WSeq.cons a s ~ʷ Stream'.WSeq.cons a t
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.think ~ʷ s
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<VAR>h : s ~ʷ t<GOAL>s.think ~ʷ t.think
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<GOAL>s ~ʷ t → s.head.Equiv t.head
<VAR>α : Type u<VAR>c : Computation (Stream'.WSeq α)<VAR>s : Stream'.WSeq α<VAR>h : s ∈ c<GOAL>Stream'.WSeq.flatten c ~ʷ s
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>c1 : Computation (Stream'.WSeq α)<VAR>c2 : Computation (Stream'.WSeq β)<VAR>h : Computation.LiftRel (Stream'.WSeq.LiftRel R) c1 c2<GOAL>Stream'.WSeq.LiftRel R (Stream'.WSeq.flatten c1) (Stream'.WSeq.flatten c2)
<VAR>α : Type u<VAR>c1 c2 : Computation (Stream'.WSeq α)<GOAL>Computation.LiftRel Stream'.WSeq.Equiv c1 c2 → Stream'.WSeq.flatten c1 ~ʷ Stream'.WSeq.flatten c2
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<VAR>h : s ~ʷ t<GOAL>s.tail ~ʷ t.tail
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<VAR>h : s ~ʷ t<VAR>n : ℕ<GOAL>s.drop n ~ʷ t.drop n
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<VAR>h : s ~ʷ t<VAR>n : ℕ<GOAL>(s.get? n).Equiv (t.get? n)
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<VAR>h : s ~ʷ t<VAR>a : α<GOAL>a ∈ s ↔ a ∈ t
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<VAR>h : s ~ʷ t<GOAL>s.Productive ↔ t.Productive
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<VAR>h : ∀ (n : ℕ), (s.get? n).Equiv (t.get? n)<GOAL>s ~ʷ t
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>s.length = Computation.map List.length s.toList
<VAR>α : Type u<GOAL>↑[] = Stream'.WSeq.nil
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>↑(a :: l) = Stream'.WSeq.cons a ↑l
<VAR>α : Type u<VAR>l : List α<GOAL>Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, Stream'.WSeq.nil) = Computation.pure l.reverse
<VAR>α : Type u<VAR>l : List α<VAR>s : Stream'.WSeq α<VAR>a : α<GOAL>Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, Stream'.WSeq.cons a s) = (Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (a :: l, s)).think
<VAR>α : Type u<VAR>l : List α<VAR>s : Stream'.WSeq α<GOAL>Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s.think) = (Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s)).think
<VAR>α : Type u<VAR>l : List α<VAR>s : Stream'.WSeq α<GOAL>Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s) = (fun x => l.reverse ++ x) <$> s.toList
<VAR>α : Type u<VAR>a : α<VAR>s : Stream'.WSeq α<GOAL>(Stream'.WSeq.cons a s).toList = (List.cons a <$> s.toList).think
<VAR>α : Type u<GOAL>Stream'.WSeq.nil.toList = Computation.pure []
<VAR>α : Type u<VAR>l : List α<GOAL>l ∈ (↑l).toList
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>(↑s).destruct = Computation.pure (Option.map (fun a => (a, ↑s.tail)) s.head)
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>(↑s).head = Computation.pure s.head
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>(↑s).tail = ↑s.tail
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>n : ℕ<GOAL>(↑s).drop n = ↑(s.drop n)
<VAR>α : Type u<VAR>s : Stream'.Seq α<VAR>n : ℕ<GOAL>(↑s).get? n = Computation.pure (s.get? n)
<VAR>α : Type u<VAR>s : Stream'.Seq α<GOAL>(↑s).toSeq = s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Stream'.WSeq.map f Stream'.WSeq.nil = Stream'.WSeq.nil
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Stream'.WSeq α<GOAL>Stream'.WSeq.map f (Stream'.WSeq.cons a s) = Stream'.WSeq.cons (f a) (Stream'.WSeq.map f s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream'.WSeq α<GOAL>Stream'.WSeq.map f s.think = (Stream'.WSeq.map f s).think
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>Stream'.WSeq.map id s = s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>Stream'.WSeq.map f (Stream'.WSeq.ret a) = Stream'.WSeq.ret (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s t : Stream'.WSeq α<GOAL>Stream'.WSeq.map f (s.append t) = (Stream'.WSeq.map f s).append (Stream'.WSeq.map f t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Stream'.WSeq α<GOAL>Stream'.WSeq.map (g ∘ f) s = Stream'.WSeq.map g (Stream'.WSeq.map f s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<VAR>s : Stream'.WSeq α<GOAL>a ∈ s → f a ∈ Stream'.WSeq.map f s
<VAR>α : Type u<VAR>a : α<VAR>S : Stream'.WSeq (Stream'.WSeq α)<GOAL>a ∈ S.join → ∃ s, s ∈ S ∧ a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Stream'.WSeq α<VAR>f : α → Stream'.WSeq β<VAR>b : β<VAR>h : b ∈ s.bind f<GOAL>∃ a, a ∈ s ∧ b ∈ f a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream'.WSeq α<GOAL>(Stream'.WSeq.map f s).destruct = Computation.map (Option.map (Prod.map f (Stream'.WSeq.map f))) s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Stream'.WSeq α<VAR>s2 : Stream'.WSeq β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : Stream'.WSeq.LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<GOAL>Stream'.WSeq.LiftRel S (Stream'.WSeq.map f1 s1) (Stream'.WSeq.map f2 s2)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s t : Stream'.WSeq α<VAR>h : s ~ʷ t<GOAL>Stream'.WSeq.map f s ~ʷ Stream'.WSeq.map f t
<VAR>α : Type u<VAR>s t : Stream'.WSeq α<GOAL>(s.append t).destruct = s.destruct.bind (Stream'.WSeq.destruct_append.aux t)
<VAR>α : Type u<VAR>S : Stream'.WSeq (Stream'.WSeq α)<GOAL>S.join.destruct = S.destruct.bind Stream'.WSeq.destruct_join.aux
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>s1 s2 : Stream'.WSeq α<VAR>t1 t2 : Stream'.WSeq β<VAR>h1 : Stream'.WSeq.LiftRel R s1 t1<VAR>h2 : Stream'.WSeq.LiftRel R s2 t2<GOAL>Stream'.WSeq.LiftRel R (s1.append s2) (t1.append t2)
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>S : Stream'.WSeq (Stream'.WSeq α)<VAR>T : Stream'.WSeq (Stream'.WSeq β)<VAR>U : Stream'.WSeq α → Stream'.WSeq β → Prop<VAR>ST : Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T<VAR>HU : ∀ (s1 : Stream'.WSeq α) (s2 : Stream'.WSeq β), (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ Stream'.WSeq.LiftRel R s t ∧ Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T) → U s1 s2<VAR>a : Option (α × Stream'.WSeq α)<VAR>ma : a ∈ S.join.destruct<GOAL>∃ b, b ∈ T.join.destruct ∧ Stream'.WSeq.LiftRelO R U a b
<VAR>α : Type u<VAR>β : Type v<VAR>R : α → β → Prop<VAR>S : Stream'.WSeq (Stream'.WSeq α)<VAR>T : Stream'.WSeq (Stream'.WSeq β)<VAR>h : Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T<GOAL>Stream'.WSeq.LiftRel R S.join T.join
<VAR>α : Type u<VAR>S T : Stream'.WSeq (Stream'.WSeq α)<VAR>h : Stream'.WSeq.LiftRel Stream'.WSeq.Equiv S T<GOAL>S.join ~ʷ T.join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Stream'.WSeq α<VAR>s2 : Stream'.WSeq β<VAR>f1 : α → Stream'.WSeq γ<VAR>f2 : β → Stream'.WSeq δ<VAR>h1 : Stream'.WSeq.LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → Stream'.WSeq.LiftRel S (f1 a) (f2 b)<GOAL>Stream'.WSeq.LiftRel S (s1.bind f1) (s2.bind f2)
<VAR>α : Type u<VAR>β : Type v<VAR>s1 s2 : Stream'.WSeq α<VAR>f1 f2 : α → Stream'.WSeq β<VAR>h1 : s1 ~ʷ s2<VAR>h2 : ∀ (a : α), f1 a ~ʷ f2 a<GOAL>s1.bind f1 ~ʷ s2.bind f2
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>(Stream'.WSeq.ret s).join ~ʷ s
<VAR>α : Type u<VAR>s : Stream'.WSeq α<GOAL>(Stream'.WSeq.map Stream'.WSeq.ret s).join ~ʷ s
<VAR>α : Type u<VAR>S T : Stream'.WSeq (Stream'.WSeq α)<GOAL>(S.append T).join ~ʷ S.join.append T.join
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Stream'.WSeq α<GOAL>s.bind (Stream'.WSeq.ret ∘ f) ~ʷ Stream'.WSeq.map f s
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : α → Stream'.WSeq β<GOAL>(Stream'.WSeq.ret a).bind f ~ʷ f a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>S : Stream'.WSeq (Stream'.WSeq α)<GOAL>Stream'.WSeq.map f S.join = (Stream'.WSeq.map (Stream'.WSeq.map f) S).join
<VAR>α : Type u<VAR>SS : Stream'.WSeq (Stream'.WSeq (Stream'.WSeq α))<GOAL>SS.join.join ~ʷ (Stream'.WSeq.map Stream'.WSeq.join SS).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Stream'.WSeq α<VAR>f : α → Stream'.WSeq β<VAR>g : β → Stream'.WSeq γ<GOAL>(s.bind f).bind g ~ʷ s.bind fun x => (f x).bind g
<GOAL>⇑(algebraMap ℝ ℂ) = Complex.ofReal'
<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra ℝ A<VAR>f : ℂ →ₐ[ℝ] A<VAR>x : ℝ<GOAL>f ↑x = (algebraMap ℝ A) x
<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra ℝ A<VAR>f g : ℂ →ₐ[ℝ] A<VAR>h : f Complex.I = g Complex.I<GOAL>f = g
<VAR>z : ℂ<GOAL>⇑(Complex.basisOneI.repr z) = ![z.re, z.im]
<GOAL>⇑Complex.basisOneI = ![1, Complex.I]
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℂ E<VAR>x : ℝ<VAR>y : E<GOAL>↑x • y = x • y
<GOAL>⇑Complex.conjAe = ⇑(starRingEnd ℂ)
<GOAL>(LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) Complex.conjAe.toLinearMap = !![1, 0; 0, -1]
<VAR>f : ℂ →ₐ[ℝ] ℂ<GOAL>f = AlgHom.id ℝ ℂ ∨ f = ↑Complex.conjAe
<GOAL>∀ (a : ℝ × ℝ), (Complex.equivRealProdLm.symm a).im = a.2
<GOAL>∀ (a : ℝ × ℝ), (Complex.equivRealProdLm.symm a).re = a.1
<GOAL>∀ (a : ℂ), Complex.equivRealProdLm a = (a.re, a.im)