ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>X✝ Y✝ : J<VAR>g : X✝ ⟶ Y✝<VAR>x : F.obj X✝<VAR>h : x ∈ ⋂ f, F.map f ⁻¹' s<GOAL>F.map g x ∈ ⋂ f, F.map f ⁻¹' s
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>X✝ Y✝ : J<VAR>g : X✝ ⟶ Y✝<VAR>x : F.obj X✝<VAR>h : ∀ (i_1 : X✝ ⟶ i), x ∈ F.map i_1 ⁻¹' s<GOAL>∀ (i_1 : Y✝ ⟶ i), F.map g x ∈ F.map i_1 ⁻¹' s
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>X✝ Y✝ : J<VAR>g : X✝ ⟶ Y✝<VAR>x : F.obj X✝<VAR>h : ∀ (i_1 : X✝ ⟶ i), x ∈ F.map i_1 ⁻¹' s<VAR>f : Y✝ ⟶ i<GOAL>F.map g x ∈ F.map f ⁻¹' s
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>X✝ Y✝ : J<VAR>g : X✝ ⟶ Y✝<VAR>x : F.obj X✝<VAR>h : ∀ (i_1 : X✝ ⟶ i), x ∈ F.map i_1 ⁻¹' s<VAR>f : Y✝ ⟶ i<GOAL>F.map f (F.map g x) ∈ s
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>X✝ Y✝ : J<VAR>g : X✝ ⟶ Y✝<VAR>x : F.obj X✝<VAR>h : ∀ (i_1 : X✝ ⟶ i), x ∈ F.map i_1 ⁻¹' s<VAR>f : Y✝ ⟶ i<GOAL>F.map f (F.map g x) ∈ s ↔ x ∈ F.map (g ≫ f) ⁻¹' s
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>X✝ Y✝ : J<VAR>g : X✝ ⟶ Y✝<VAR>x : F.obj X✝<VAR>h : ∀ (i_1 : X✝ ⟶ i), x ∈ F.map i_1 ⁻¹' s<VAR>f : Y✝ ⟶ i<GOAL>F.map f (F.map g x) ∈ s ↔ x ∈ (F.map g ≫ F.map f) ⁻¹' s
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>j : J<GOAL>{ obj := fun j => ↑(⋂ f, F.map f ⁻¹' s), map := fun {X Y} g => MapsTo.restrict (F.map g) (⋂ f, F.map f ⁻¹' s) (⋂ f, F.map f ⁻¹' s) ⋯ }.map (𝟙 j) = 𝟙 ({ obj := fun j => ↑(⋂ f, F.map f ⁻¹' s), map := fun {X Y} g => MapsTo.restrict (F.map g) (⋂ f, F.map f ⁻¹' s) (⋂ f, F.map f ⁻¹' s) ⋯ }.obj j)
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>j : J<GOAL>(fun x => ⟨𝟙 (F.obj j) ↑x, ⋯⟩) = 𝟙 ↑(⋂ f, F.map f ⁻¹' s)
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>X✝ Y✝ Z✝ : J<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>{ obj := fun j => ↑(⋂ f, F.map f ⁻¹' s), map := fun {X Y} g => MapsTo.restrict (F.map g) (⋂ f, F.map f ⁻¹' s) (⋂ f, F.map f ⁻¹' s) ⋯ }.map (f ≫ g) = { obj := fun j => ↑(⋂ f, F.map f ⁻¹' s), map := fun {X Y} g => MapsTo.restrict (F.map g) (⋂ f, F.map f ⁻¹' s) (⋂ f, F.map f ⁻¹' s) ⋯ }.map f ≫ { obj := fun j => ↑(⋂ f, F.map f ⁻¹' s), map := fun {X Y} g => MapsTo.restrict (F.map g) (⋂ f, F.map f ⁻¹' s) (⋂ f, F.map f ⁻¹' s) ⋯ }.map g
<VAR>J : Type u<VAR>inst✝ : Category.{?u.10050, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>X✝ Y✝ Z✝ : J<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>(fun x => ⟨(F.map f ≫ F.map g) ↑x, ⋯⟩) = (fun x => ⟨F.map f ↑x, ⋯⟩) ≫ fun x => ⟨F.map g ↑x, ⋯⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s t : Set X<GOAL>𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s t : Set X<GOAL>𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s t : Set X<GOAL>(∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s) → s ⊆ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s t : Set X<VAR>x : X<VAR>hx : x ∈ s<VAR>h : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s<GOAL>x ∈ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s t : Set X<VAR>x : X<VAR>hx : x ∈ s<VAR>h : x ∉ t → x ∉ s<GOAL>x ∈ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s t : Set X<VAR>x : X<VAR>hx : x ∈ s<VAR>h : x ∉ t → x ∉ s<VAR>hxt : x ∉ t<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹⁵ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>N : Type u_3<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : Module R N<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid P<VAR>inst✝⁹ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v : ι → M<VAR>v' : ι → M'<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>f v + f (v ∘ ⇑(Equiv.swap i j)) = 0
<VAR>R : Type u_1<VAR>inst✝¹⁵ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>N : Type u_3<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : Module R N<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid P<VAR>inst✝⁹ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v : ι → M<VAR>v' : ι → M'<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>f (v ∘ ⇑(Equiv.swap i j)) + f v = 0
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>f : G →* H<VAR>emb : OpenEmbedding ⇑f<VAR>U : Set H<VAR>hU : U ∈ 𝓝 1<GOAL>⇑f ⁻¹' U ∈ 𝓝 1
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>f : G →* H<VAR>emb : OpenEmbedding ⇑f<VAR>U : Set H<VAR>hU : U ∈ 𝓝 1<GOAL>U ∈ 𝓝 (f 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Function.Surjective ⇑(mapBaseChange R A B)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<VAR>this : Subsingleton (Ω[B⁄A])<GOAL>Function.Surjective ⇑(mapBaseChange R A B)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<VAR>this : Subsingleton (Ω[B⁄A])<GOAL>⊤ ≤ LinearMap.ker (map R A B B)
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h✝ h : ∀ (n : ℕ), P (n + 1) → P n<VAR>k seed : ℕ<VAR>hk : 1 < k<VAR>hs : P seed.succ<VAR>hm : ∀ (x : ℕ), seed < x → P x → P (k * x)<VAR>n x✝ : ℕ<VAR>hl : seed.succ ≤ x✝<VAR>hP✝ : P x✝<GOAL>x✝ < (fun x => k * x) x✝
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h✝ h : ∀ (n : ℕ), P (n + 1) → P n<VAR>k seed : ℕ<VAR>hk : 1 < k<VAR>hs : P seed.succ<VAR>hm : ∀ (x : ℕ), seed < x → P x → P (k * x)<VAR>n x✝ : ℕ<VAR>hl : seed.succ ≤ x✝<VAR>hP✝ : P x✝<GOAL>x✝ = 1 * x✝
<VAR>l : List ℕ<VAR>a m n : ℕ<GOAL>(zeckendorf 0).IsZeckendorfRep
<VAR>l : List ℕ<VAR>a m n✝ n : ℕ<GOAL>(n + 1).zeckendorf.IsZeckendorfRep
<VAR>l : List ℕ<VAR>a m n✝ n : ℕ<GOAL>Chain' (fun a b => b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))
<VAR>l : List ℕ<VAR>a✝ m n✝ n a : ℕ<VAR>ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?<GOAL>a + 2 ≤ (n + 1).greatestFib
<VAR>l : List ℕ<VAR>a✝ m n✝ n a : ℕ<VAR>ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?<VAR>h : n + 1 - fib (n + 1).greatestFib = 0<GOAL>a + 2 ≤ (n + 1).greatestFib
<VAR>l : List ℕ<VAR>a✝ m n✝ n a : ℕ<VAR>ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?<VAR>h : n + 1 - fib (n + 1).greatestFib > 0<GOAL>a + 2 ≤ (n + 1).greatestFib
<VAR>l : List ℕ<VAR>a✝ m n✝ n a : ℕ<VAR>ha : (n + 1 - fib (n + 1).greatestFib).greatestFib = a<VAR>h : n + 1 - fib (n + 1).greatestFib > 0<GOAL>a + 2 ≤ (n + 1).greatestFib
<VAR>l : List ℕ<VAR>a m n✝ n : ℕ<VAR>h : n + 1 - fib (n + 1).greatestFib > 0<GOAL>(n + 1 - fib (n + 1).greatestFib).greatestFib + 2 ≤ (n + 1).greatestFib
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<GOAL>finrank ℝ ↥⊤.direction = 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<GOAL>finrank ℝ V = 2
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝<VAR>inst✝¹ : Algebra F L<VAR>K K' : IntermediateField F L<VAR>inst✝ : Normal F ↥K<GOAL>normalClosure F (↥K) L = K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<GOAL>⨆ x, ↑(f x) = ⊤ ↔ ¬BddAbove (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<GOAL>(∀ b < ⊤, ∃ i, b < ↑(f i)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>evalEval x y (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>y ^ 2 + (W.a₁ * x + W.a₃) * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a b : W ⟶ (cone f hi).pt<VAR>z : (forget Stonean).obj W<VAR>hfst : (a ≫ fst f hi) z = (b ≫ fst f hi) z<GOAL>a z = b z
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z W : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>a b : W ⟶ (cone f hi).pt<VAR>z : (forget Stonean).obj W<VAR>hfst : (a ≫ fst f hi) z = (b ≫ fst f hi) z<GOAL>↑(a z) = ↑(b z)
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q r : ℝ≥0<GOAL>↑(↑r).toNNReal ≤ ↑r
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.toCompositionAsSet.length = c.length
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<GOAL>∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<GOAL>C * (a * (‖y‖ / ↑r')) ^ n ≤ C * a ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<GOAL>C * (a * (‖y‖ / ↑r')) ^ n ≤ C * a ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>this : 0 ≤ a<GOAL>C * (a * (‖y‖ / ↑r')) ^ n ≤ C * a ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>this : 0 ≤ a<GOAL>a * (‖y‖ / ↑r') ≤ a
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝¹ : P.IsPrime<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>hIP : comap (algebraMap R S) I ≤ P<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝¹ : P.IsPrime<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>hIP : comap (algebraMap R S) I ≤ P<VAR>Q' : Ideal (S ⧸ I)<VAR>Q'_prime : Q'.IsPrime<VAR>hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝¹ : P.IsPrime<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>hIP : comap (algebraMap R S) I ≤ P<VAR>Q' : Ideal (S ⧸ I)<VAR>Q'_prime : Q'.IsPrime<VAR>hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P<GOAL>comap (algebraMap R S) (comap (Quotient.mk I) Q') = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝¹ : P.IsPrime<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>hIP : comap (algebraMap R S) I ≤ P<VAR>Q' : Ideal (S ⧸ I)<VAR>Q'_prime : Q'.IsPrime<VAR>hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P<GOAL>comap ((Quotient.mk I).comp (algebraMap R S)) Q' = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝¹ : P.IsPrime<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>hIP : comap (algebraMap R S) I ≤ P<VAR>Q' : Ideal (S ⧸ I)<VAR>Q'_prime : Q'.IsPrime<VAR>hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P<GOAL>comap ((Quotient.mk I).comp (algebraMap R S)) Q' = comap (Quotient.mk (comap (algebraMap R S) I)) (comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q')
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝¹ : P.IsPrime<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>hIP : comap (algebraMap R S) I ≤ P<VAR>Q' : Ideal (S ⧸ I)<VAR>Q'_prime : Q'.IsPrime<VAR>hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P<GOAL>comap (Quotient.mk (comap (algebraMap R S) I)) (map (Quotient.mk (comap (algebraMap R S) I)) P) = P
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>hurwitzZetaOdd (↑x) (-(2 * ↑k)) = -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n<GOAL>hurwitzZetaOdd (↑x) (-(2 * ↑k)) = -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n<VAR>h3 : (2 * ↑k + 1).Gammaℂ ≠ 0<GOAL>hurwitzZetaOdd (↑x) (-(2 * ↑k)) = -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n<VAR>h3 : (2 * ↑k + 1).Gammaℂ ≠ 0<GOAL>Complex.sin (↑π * (2 * ↑k + 1) / 2) * (-1) ^ (k + 1) / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1))) = -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n<VAR>h3 : (2 * ↑k + 1).Gammaℂ ≠ 0<GOAL>Complex.sin (↑π * (2 * ↑k + 1) / 2) * (-1) ^ (k + 1) = -1
<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>hp : p.Monic<VAR>hroots : Multiset.card p.roots = p.natDegree<GOAL>(Multiset.map (fun a => X - C a) p.roots).prod = p
<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>hp : p.Monic<VAR>hroots : Multiset.card p.roots = p.natDegree<GOAL>(Multiset.map (fun a => X - C a) p.roots).prod = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>inst✝¹⁵ : Category.{u_7, u_1} C<VAR>inst✝¹⁴ : Category.{u_6, u_2} D<VAR>inst✝¹³ : Category.{?u.106857, u_3} E<VAR>inst✝¹² : Category.{?u.106861, u_4} J<VAR>F₁ F₂ F₃ : C ⥤ D<VAR>τ : F₁ ⟶ F₂<VAR>τ' : F₂ ⟶ F₃<VAR>e : F₁ ≅ F₂<VAR>G G' : D ⥤ E<VAR>τ'' : G ⟶ G'<VAR>H : E ⥤ J<VAR>A : Type u_5<VAR>inst✝¹¹ : AddMonoid A<VAR>inst✝¹⁰ : HasShift C A<VAR>inst✝⁹ : HasShift D A<VAR>inst✝⁸ : HasShift E A<VAR>inst✝⁷ : HasShift J A<VAR>inst✝⁶ : F₁.CommShift A<VAR>inst✝⁵ : F₂.CommShift A<VAR>inst✝⁴ : F₃.CommShift A<VAR>inst✝³ : G.CommShift A<VAR>inst✝² : G'.CommShift A<VAR>inst✝¹ : H.CommShift A<VAR>inst✝ : CommShift τ A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctor D a).map (τ.app X) = (F₁.commShiftIso a).inv.app X ≫ τ.app ((shiftFunctor C a).obj X) ≫ (F₂.commShiftIso a).hom.app X
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>x y : α<VAR>x✝ : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c<VAR>z : α<VAR>hx : x ∈ {x | r.Rel x z}<VAR>hy : y ∈ {x | r.Rel x z}<GOAL>r.Rel x y
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S : Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c✝ d✝ : C<VAR>p : d✝ ⟶ c✝<VAR>γ : c✝ ⟶ c✝<VAR>hs : γ ∈ S.arrows c✝ c✝<GOAL>p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d✝ d✝
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S : Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c✝ d✝ : C<VAR>p : d✝ ⟶ c✝<VAR>γ : c✝ ⟶ c✝<VAR>hs : γ ∈ S.arrows c✝ c✝<GOAL>p = Groupoid.inv (Groupoid.inv p)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<GOAL>((fun x => rexp (f x)) =Θ[l] fun x => rexp (g x)) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x - g x|
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : OpensMeasurableSpace X<VAR>hf : LocallyIntegrable f (μ.restrict s)<VAR>x : X<VAR>a✝ : x ∈ s<VAR>t : Set X<VAR>ht_mem : t ∈ 𝓝 x<VAR>ht_int : IntegrableOn f t (μ.restrict s)<GOAL>IntegrableAtFilter f (𝓝[s] x) μ