ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<GOAL>(permutations'Aux x s).Nodup ↔ x ∉ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : (permutations'Aux x s).Nodup<GOAL>x ∉ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : (permutations'Aux x s).Nodup<VAR>H : x ∈ s<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : (permutations'Aux x s).Nodup<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<GOAL>k < (permutations'Aux x s).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<GOAL>k + 1 < (permutations'Aux x s).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<GOAL>(permutations'Aux x s).nthLe k ?intro.intro.refine_1 = (permutations'Aux x s).nthLe (k + 1) ?intro.intro.refine_2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<GOAL>(permutations'Aux x s).nthLe k ⋯ = (permutations'Aux x s).nthLe (k + 1) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<GOAL>insertNth k x s = insertNth (k + 1) x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<VAR>hl : (insertNth k x s).length = (insertNth (k + 1) x s).length<GOAL>insertNth k x s = insertNth (k + 1) x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<VAR>hl : (insertNth k x s).length = (insertNth (k + 1) x s).length<VAR>n : ℕ<VAR>hn : n < (insertNth k x s).length<VAR>hn' : n < (insertNth (k + 1) x s).length<GOAL>(insertNth k x s).nthLe n hn = (insertNth (k + 1) x s).nthLe n hn'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H✝ : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<VAR>hl : (insertNth k x s).length = (insertNth (k + 1) x s).length<VAR>n : ℕ<VAR>hn : n < (insertNth k x s).length<VAR>hn' : n < (insertNth (k + 1) x s).length<VAR>H : n < k<GOAL>(insertNth k x s).nthLe n hn = (insertNth (k + 1) x s).nthLe n hn'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H : x ∈ s<VAR>n : ℕ<VAR>hk : n < s.length<VAR>hk' : s.nthLe n hk = x<VAR>hl : (insertNth n x s).length = (insertNth (n + 1) x s).length<VAR>hn : n < (insertNth n x s).length<VAR>hn' : n < (insertNth (n + 1) x s).length<GOAL>(insertNth n x s).nthLe n hn = (insertNth (n + 1) x s).nthLe n hn'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>x : α<VAR>h : ∀ (i j : ℕ) (h₁ : i < (permutations'Aux x s).length) (h₂ : j < (permutations'Aux x s).length), (permutations'Aux x s).nthLe i h₁ = (permutations'Aux x s).nthLe j h₂ → i = j<VAR>H✝ : x ∈ s<VAR>k : ℕ<VAR>hk : k < s.length<VAR>hk' : s.nthLe k hk = x<VAR>hl : (insertNth k x s).length = (insertNth (k + 1) x s).length<VAR>n : ℕ<VAR>hn : n < (insertNth k x s).length<VAR>hn' : n < (insertNth (k + 1) x s).length<VAR>H : k < n<GOAL>(insertNth k x s).nthLe n hn = (insertNth (k + 1) x s).nthLe n hn'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>T R (n - 2) = 2 * X * T R (n - 1) - T R n
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : Monoid A<VAR>inst✝⁹ : Monoid B<VAR>inst✝⁸ : Monoid C<VAR>inst✝⁷ : Monoid D<VAR>inst✝⁶ : CommGroup E<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace C<VAR>inst✝² : TopologicalSpace D<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalGroup E<VAR>f g : ContinuousMonoidHom A B<VAR>h : f.toContinuousMap = g.toContinuousMap<GOAL>∀ (x : A), f x = g x
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>F : J ⥤ Mon_ C<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>(((Functor.const J).obj (limit F)).map f ≫ (fun j => { hom := limit.π (F ⋙ forget C) j, one_hom := ⋯, mul_hom := ⋯ }) j').hom = ((fun j => { hom := limit.π (F ⋙ forget C) j, one_hom := ⋯, mul_hom := ⋯ }) j ≫ F.map f).hom
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx : 1 < x<VAR>hz : 0 < z<GOAL>1 < x ^ z
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx : 1 < x<VAR>hz : 0 < z<GOAL>1 ^ z < x ^ z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>hc : IsComplete ↑(iSup V)<VAR>this : CompleteSpace ↥(iSup V)<GOAL>DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t l l' : Multiset α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<VAR>h : l.toFinset = l'.toFinset<GOAL>l = l'
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ s₂✝ : Finmap β<VAR>s₁ s₂ : AList β<VAR>h : ⟦s₁⟧.Disjoint ⟦s₂⟧<GOAL>⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>l : List R[A]<GOAL>(List.map (fun f => f.support.inf degt) l).sum ≤ l.prod.support.inf degt
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>l : List R[A]<GOAL>Quot.lift (fun l => List.foldr (fun x x_1 => x ⊓ x_1) ⊤ l) ⋯ (Multiset.map degt l.prod.support.val) ≤ List.foldl (fun x x_1 => x + x_1) 0 (List.map (fun f => f.support.inf degt) l)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>l : List R[A]<GOAL>degt 0 ≤ 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>l : List R[A]<GOAL>∀ (a b : A), degt (a + b) ≤ degt a + degt b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable σ<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>hp : PrimrecPred p<VAR>f : α → Subtype p<VAR>this : Primcodable (Subtype p) := Primcodable.subtype hp<GOAL>(Primrec fun a => ↑(f a)) ↔ Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable σ<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>hp : PrimrecPred p<VAR>f : α → Subtype p<VAR>this : Primcodable (Subtype p) := Primcodable.subtype hp<VAR>h : Primrec fun a => ↑(f a)<GOAL>Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable σ<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>hp : PrimrecPred p<VAR>f : α → Subtype p<VAR>this : Primcodable (Subtype p) := Primcodable.subtype hp<VAR>h : Primrec fun a => ↑(f a)<VAR>n : ℕ<GOAL>encode (Option.map (fun a => ↑(f a)) (decode n)) = encode (Option.map f (decode n))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : ι → Filter α<VAR>m : α → β<VAR>hf : Directed (fun x x_1 => x ≥ x_1) f<VAR>inst✝ : Nonempty ι<VAR>s : Set β<VAR>hs : m ⁻¹' s ∈ iInf f<VAR>i : ι<VAR>hi : m ⁻¹' s ∈ f i<GOAL>map m (f i) ≤ 𝓟 s
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<GOAL>‖fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₂ f)) w n‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<GOAL>‖fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n fun v => fourierPowSMulRight L f v k) w‖ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<GOAL>∫ (v : V), ‖iteratedFDeriv ℝ n (fun v => fourierPowSMulRight L f v k) v‖ ∂μ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<VAR>I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v => ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ<GOAL>∫ (v : V), ‖iteratedFDeriv ℝ n (fun v => fourierPowSMulRight L f v k) v‖ ∂μ ≤ (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<VAR>I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v => ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ<GOAL>∫ (v : V), ‖iteratedFDeriv ℝ n (fun v => fourierPowSMulRight L f v k) v‖ ∂μ ≤ ∫ (a : V), (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖ ∂μ
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<VAR>I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v => ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ<GOAL>0 ≤ᶠ[ae μ] fun a => ‖iteratedFDeriv ℝ n (fun v => fourierPowSMulRight L f v k) a‖
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<VAR>I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v => ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ<GOAL>Integrable (fun a => (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖) μ
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>w : W<VAR>I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v => ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ<GOAL>(fun a => ‖iteratedFDeriv ℝ n (fun v => fourierPowSMulRight L f v k) a‖) ≤ᶠ[ae μ] fun a => (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Zero α<VAR>inst✝ : One α<VAR>f : m ≃. n<VAR>i✝ : n<VAR>j✝ : m<GOAL>f.symm.toMatrix i✝ j✝ = f.toMatrixᵀ i✝ j✝
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Zero α<VAR>inst✝ : One α<VAR>f : m ≃. n<VAR>i✝ : n<VAR>j✝ : m<GOAL>(if i✝ ∈ f j✝ then 1 else 0) = of (fun x y => if x ∈ f y then 1 else 0) i✝ j✝
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : DecidableEq J<VAR>j : J<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(single j).map f j ≫ (singleObjApplyIso j Y).hom = (singleObjApplyIso j X).hom ≫ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>↑(⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x<VAR>hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x<VAR>hu' : IntervalIntegrable u' volume a b<VAR>hv' : IntervalIntegrable v' volume a b<GOAL>∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x<VAR>hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x<VAR>hu' : IntervalIntegrable u' volume a b<VAR>hv' : IntervalIntegrable v' volume a b<GOAL>∫ (x : ℝ) in a..b, u x * v' x = ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x - u' x * v x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x<VAR>hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x<VAR>hu' : IntervalIntegrable u' volume a b<VAR>hv' : IntervalIntegrable v' volume a b<GOAL>IntervalIntegrable (fun x => u' x * v x + u x * v' x) volume a b