ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<VAR>hU1 : ∀ (n : ℕ), U n ∈ nhds 1<VAR>hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n<VAR>hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n<VAR>hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<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>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<VAR>hU1 : ∀ (n : ℕ), U n ∈ nhds 1<VAR>hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n<VAR>hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n<VAR>hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)<GOAL>EquicontinuousAt (fun f => ⇑↑f) 1
<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>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<VAR>hU1 : ∀ (n : ℕ), U n ∈ nhds 1<VAR>hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n<VAR>hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n<VAR>hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)<GOAL>∀ (k : ℕ), True → ∀ᶠ (x : X) in nhds 1, ∀ (i : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}), (↑i 1, ↑i x) ∈ {x | x.2 / x.1 ∈ V k}
<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>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<VAR>hU1 : ∀ (n : ℕ), U n ∈ nhds 1<VAR>hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n<VAR>hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n<VAR>hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)<VAR>n : ℕ<VAR>x✝¹ : True<VAR>x : X<VAR>hx : x ∈ U n<VAR>x✝ : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}<VAR>f : X →* Y<VAR>hf : f ∈ {f | Set.MapsTo (⇑f) (U 0) (V 0)}<GOAL>(↑⟨f, hf⟩ 1, ↑⟨f, hf⟩ x) ∈ {x | x.2 / x.1 ∈ V 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>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<VAR>hU1 : ∀ (n : ℕ), U n ∈ nhds 1<VAR>hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n<VAR>hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n<VAR>hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)<VAR>n : ℕ<VAR>x✝¹ : True<VAR>x : X<VAR>hx : x ∈ U n<VAR>x✝ : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}<VAR>f : X →* Y<VAR>hf : f ∈ {f | Set.MapsTo (⇑f) (U 0) (V 0)}<GOAL>(1, ↑⟨f, hf⟩ x).2 ∈ V n
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I✝ I : Ideal R<VAR>i : ℕ<VAR>r : R<GOAL>(monomial i) r ∈ reesAlgebra I ↔ r ∈ I ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ q✝ : α → Prop<VAR>inst✝³ : DecidablePred p✝<VAR>inst✝² : DecidablePred q✝<VAR>s✝ t✝ s t : Finset α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : _root_.Disjoint p q<GOAL>_root_.Disjoint (filter p s) (filter q t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ q✝ : α → Prop<VAR>inst✝³ : DecidablePred p✝<VAR>inst✝² : DecidablePred q✝<VAR>s✝ t✝ s t : Finset α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : _root_.Disjoint p q<GOAL>∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ q✝ : α → Prop<VAR>inst✝³ : DecidablePred p✝<VAR>inst✝² : DecidablePred q✝<VAR>s✝ t✝ s t : Finset α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : _root_.Disjoint p q<VAR>a : α<VAR>left✝¹ : a ∈ s<VAR>hp : p a<VAR>left✝ : a ∈ t<VAR>hq : q a<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ q✝ : α → Prop<VAR>inst✝³ : DecidablePred p✝<VAR>inst✝² : DecidablePred q✝<VAR>s✝ t✝ s t : Finset α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : ∀ (i : α), _root_.Disjoint (p i) (q i)<VAR>a : α<VAR>left✝¹ : a ∈ s<VAR>hp : p a<VAR>left✝ : a ∈ t<VAR>hq : q a<GOAL>False
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>s : SummableFamily Γ R α<VAR>g : Γ<VAR>hg : g ∈ s.hsum.support<GOAL>g ∈ ⋃ a, (s a).support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>s : SummableFamily Γ R α<VAR>g : Γ<VAR>hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0<GOAL>g ∈ ⋃ a, (s a).support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>s : SummableFamily Γ R α<VAR>g : Γ<VAR>hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0<VAR>a : α<VAR>left✝ : a ∈ ⋯.toFinset<VAR>h2 : (s a).coeff g ≠ 0<GOAL>g ∈ ⋃ a, (s a).support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>s : SummableFamily Γ R α<VAR>g : Γ<VAR>hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0<VAR>a : α<VAR>left✝ : a ∈ ⋯.toFinset<VAR>h2 : (s a).coeff g ≠ 0<GOAL>∃ i, g ∈ (s i).support
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x y : E<VAR>r : ℝ<GOAL>y ∈ p.ball 0 r ↔ p y < r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>u : R[X]ˣ<GOAL>(↑u).coeff 0 ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>u : R[X]ˣ<GOAL>(↑u).coeff (↑u).natDegree ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>u : R[X]ˣ<GOAL>¬↑u = 0
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : StrongOplaxNatTrans F G<VAR>θ : StrongOplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : G.obj c ⟶ a'<GOAL>(η.naturality (f ≫ g)).hom ▷ h ≫ (α_ (η.app a) (G.map (f ≫ g)) h).hom ≫ η.app a ◁ G.mapComp f g ▷ h = F.mapComp f g ▷ η.app c ▷ h ≫ (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫ (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫ F.map f ◁ (η.naturality g).hom ▷ h ≫ (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫ (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫ (η.naturality f).hom ▷ G.map g ▷ h ≫ (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom
<VAR>α : Type u_1<VAR>b : ℂ<VAR>hb : b ≠ 0<GOAL>(fun x => 0 ^ x) =ᶠ[𝓝 b] 0
<VAR>α : Type u_1<VAR>b : ℂ<VAR>hb : b ≠ 0<GOAL>∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<GOAL>i ≤ ↑n
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<GOAL>i ≤ last n
<VAR>μ : YoungDiagram<VAR>j a b : ℕ<GOAL>(a, b) ∈ μ.col j ↔ (a, b) ∈ Finset.range (μ.colLen j) ×ˢ {j}
<VAR>μ : YoungDiagram<VAR>j a b : ℕ<GOAL>b = j → (a < μ.colLen b ↔ a < μ.colLen j)
<VAR>μ : YoungDiagram<VAR>a b : ℕ<GOAL>a < μ.colLen b ↔ a < μ.colLen b
<VAR>a b r : ℤ<VAR>hr : 0 < r<VAR>x : ℤ<GOAL>x ∈ filter (fun x => r ∣ x) (Ioc a b) ↔ x ∈ map { toFun := fun x => x * r, inj' := ⋯ } (Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)
<VAR>a b r : ℤ<VAR>hr : 0 < r<VAR>x : ℤ<GOAL>((a < x ∧ x ≤ b) ∧ ∃ c, x = c * r) ↔ ∃ a_1, (a < a_1 * r ∧ a_1 * r ≤ b) ∧ { toFun := fun x => x * r, inj' := ⋯ } a_1 = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<GOAL>(∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ s.card • ∑ i ∈ s, f i • g i
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>this : HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x)) ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))<VAR>ofReal_two : ↑2 = 2<GOAL>HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x)) ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! * Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>this : HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x)) ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))<VAR>ofReal_two : ↑2 = 2<VAR>x✝ : ℕ<GOAL>1 / ↑x✝ ^ (2 * k + 1) * Real.sin (2 * π * ↑x✝ * x) = (1 / ↑x✝ ^ (2 * k + 1) * ((fourier ↑x✝) ↑x - (fourier (-↑x✝)) ↑x) / (2 * I)).re
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>this : HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x)) ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))<VAR>ofReal_two : ↑2 = 2<GOAL>(-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! * Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))) = ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / (2 * I)).re
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>I : IsIso f<VAR>Z : C<VAR>g : X ⟶ Z<GOAL>f ≫ inv f ≫ g = g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>t : List α<VAR>IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t<VAR>s : List α<GOAL>s ∈ (a :: t).sublists' ↔ s <+ a :: t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>t : List α<VAR>IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t<VAR>s : List α<GOAL>(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Algebra R 𝕜<VAR>p : 𝕜[X]<VAR>q : R[X]<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => eval x p) s x = eval x (derivative p)
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Algebra R 𝕜<VAR>p : 𝕜[X]<VAR>q : R[X]<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>deriv (fun x => eval x p) x = eval x (derivative p)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X : OppositeShift C A<VAR>a b : A<GOAL>(shiftFunctorAdd' (OppositeShift C A) a b (a + b) ⋯).inv.app X = ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app (Opposite.unop X)).op
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F F' : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝ : F.Faithful<VAR>α : F ≅ F'<VAR>X✝ Y✝ : C<VAR>a₁✝ a₂✝ : X✝ ⟶ Y✝<VAR>h : F'.map a₁✝ = F'.map a₂✝<GOAL>F.map a₁✝ = F.map a₂✝
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < 1 + ε ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 + ε ↑(r i x)
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>s : NonUnitalStarSubalgebra R A<GOAL>Submodule.span R ↑s = s.toSubmodule
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<GOAL>borel X ≤ μ.caratheodory
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<GOAL>MeasurableSpace.generateFrom {s | IsClosed s} ≤ μ.caratheodory
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<VAR>Ssep : ∀ (n : ℕ), IsMetricSeparated (S n) t<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<VAR>Ssep : ∀ (n : ℕ), IsMetricSeparated (S n) t<VAR>Ssep' : ∀ (n : ℕ), IsMetricSeparated (S n) (s ∩ t)<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<VAR>Ssep : ∀ (n : ℕ), IsMetricSeparated (S n) t<VAR>Ssep' : ∀ (n : ℕ), IsMetricSeparated (S n) (s ∩ t)<VAR>S_sub : ∀ (n : ℕ), S n ⊆ s \ t<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<VAR>Ssep : ∀ (n : ℕ), IsMetricSeparated (S n) t<VAR>Ssep' : ∀ (n : ℕ), IsMetricSeparated (S n) (s ∩ t)<VAR>S_sub : ∀ (n : ℕ), S n ⊆ s \ t<VAR>hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<VAR>Ssep : ∀ (n : ℕ), IsMetricSeparated (S n) t<VAR>Ssep' : ∀ (n : ℕ), IsMetricSeparated (S n) (s ∩ t)<VAR>S_sub : ∀ (n : ℕ), S n ⊆ s \ t<VAR>hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s<VAR>iUnion_S : ⋃ n, S n = s \ t<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<VAR>Ssep : ∀ (n : ℕ), IsMetricSeparated (S n) t<VAR>Ssep' : ∀ (n : ℕ), IsMetricSeparated (S n) (s ∩ t)<VAR>S_sub : ∀ (n : ℕ), S n ⊆ s \ t<VAR>hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s<VAR>iUnion_S : ⋃ n, S n = s \ t<VAR>htop : ¬μ (s \ t) = ⊤<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<VAR>Ssep : ∀ (n : ℕ), IsMetricSeparated (S n) t<VAR>Ssep' : ∀ (n : ℕ), IsMetricSeparated (S n) (s ∩ t)<VAR>S_sub : ∀ (n : ℕ), S n ⊆ s \ t<VAR>hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s<VAR>iUnion_S : ⋃ n, S n = s \ t<VAR>htop : ¬μ (s \ t) = ⊤<GOAL>μ (⋃ n, S n) ≤ ⨆ n, μ (S n)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>hm : μ.IsMetric<VAR>t : Set X<VAR>ht : t ∈ {s | IsClosed s}<VAR>s : Set X<VAR>S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}<VAR>Ssep : ∀ (n : ℕ), IsMetricSeparated (S n) t<VAR>Ssep' : ∀ (n : ℕ), IsMetricSeparated (S n) (s ∩ t)<VAR>S_sub : ∀ (n : ℕ), S n ⊆ s \ t<VAR>hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s<VAR>iUnion_S : ⋃ n, S n = s \ t<VAR>htop : ¬μ (s \ t) = ⊤<VAR>this : ∀ (n : ℕ), S n ⊆ S (n + 1)<GOAL>μ (⋃ n, S n) ≤ ⨆ n, μ (S n)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<GOAL>(((Basis.singleton Unit K).constr K) fun x => ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i) 1 = ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<GOAL>∑ i : Unit, (Basis.singleton Unit K).equivFun 1 i • ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i = ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>h : s.IsPWO<GOAL>s.IsWF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<GOAL>∏ᶠ (i : α) (_ : a = i), f i = f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝³ : SemilatticeSup α<VAR>s✝ : Finset β<VAR>H : s✝.Nonempty<VAR>f✝ : β → α<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : SupHomClass F α β<VAR>f : F<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>g : ι → α<GOAL>f (s.sup' hs g) = s.sup' hs (⇑f ∘ g)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition n<VAR>i : ℕ<VAR>hi : i < (l.splitWrtComposition c).length<GOAL>(l.splitWrtComposition c).get ⟨i, hi⟩ = drop (c.sizeUpTo i) (take (c.sizeUpTo (i + 1)) l)