ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>e : β → α<VAR>a : α<GOAL>a ∈ closure (range e) ↔ ∀ ε > 0, ∃ k, dist a (e k) < ε
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Monoid R<VAR>l : List α<VAR>fι : α → ι<VAR>fA : α → R<GOAL>l.dProd fι fA = (map fA l).prod
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 0 ∨ a ≠ 0<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ (completedHurwitzZetaEven a) s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 0 ∨ a ≠ 0<VAR>hs' : s ≠ 1<GOAL>s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 0 ∨ a ≠ 0<VAR>hs' : s ≠ 1<GOAL>s / 2 ≠ ↑(hurwitzEvenFEPair a).k
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<GOAL>A *ᵥ A.cramer b = A.det • b
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : Module.Finite R L<VAR>inst✝ : LieAlgebra.IsKilling R L<GOAL>(ad R L).range = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : Module.Finite R L<VAR>inst✝ : LieAlgebra.IsKilling R L<GOAL>(ad R L).range.toSubmodule = ⊤.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : Module.Finite R L<VAR>inst✝ : LieAlgebra.IsKilling R L<GOAL>(LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : Module.Finite R L<VAR>inst✝ : LieAlgebra.IsKilling R L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule<VAR>x : L<GOAL>D x = 0 x
<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✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>l : List α<GOAL>List.foldr (fun x x_1 => x ⊓ x_1) ⊤ l = l.toFinset.inf id
<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✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>l : List α<GOAL>Multiset.fold (fun x x_1 => x ⊓ x_1) ⊤ (↑l).dedup = (↑l).dedup.inf
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>s✝ t : Subfield K<VAR>f✝ f : K →+* L<VAR>s : Subfield K<VAR>y : L<GOAL>(y ∈ let __src := Subring.map f s.toSubring; { toSubring := __src, inv_mem' := ⋯ }) ↔ ∃ x ∈ s, f x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>a \ liminf u f = limsup (fun b => a \ u b) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>(a \ liminf u f)ᶜ = (limsup (fun b => a \ u b) f)ᶜ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>h : IsAssociatedPrime I M<VAR>hf : Function.Injective ⇑f<GOAL>IsAssociatedPrime I M'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Injective ⇑f<VAR>x : M<VAR>h : IsAssociatedPrime (Submodule.span R {x}).annihilator M<GOAL>IsAssociatedPrime (Submodule.span R {x}).annihilator M'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Injective ⇑f<VAR>x : M<VAR>h : IsAssociatedPrime (Submodule.span R {x}).annihilator M<GOAL>(Submodule.span R {x}).annihilator = (Submodule.span R {f x}).annihilator
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>J : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Injective ⇑f<VAR>x : M<VAR>h : IsAssociatedPrime (Submodule.span R {x}).annihilator M<VAR>r : R<GOAL>r ∈ (Submodule.span R {x}).annihilator ↔ r ∈ (Submodule.span R {f x}).annihilator
<VAR>α : Sort u_2<VAR>a : α<VAR>β : Sort u_1<VAR>C : α → Sort u_1<VAR>x : C a<VAR>y : β<GOAL>HEq (⋯ ▸ x) y ↔ HEq x y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>inst✝ : IsOpenImmersion g<VAR>e : Set.range ⇑f.base = Set.range ⇑g.base<GOAL>lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>inst✝ : IsOpenImmersion g<VAR>e : Set.range ⇑f.base = Set.range ⇑g.base<GOAL>(lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>inst✝ : IsOpenImmersion g<VAR>e : Set.range ⇑f.base = Set.range ⇑g.base<GOAL>lift f g ⋯ ≫ lift g f ⋯ = 𝟙 Y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>inst✝ : IsOpenImmersion g<VAR>e : Set.range ⇑f.base = Set.range ⇑g.base<GOAL>(lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Sort ?u.45682<VAR>δ : Sort ?u.45684<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>r : α → β → Bool<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<GOAL>all₂ r (a :: as) (b :: bs) = true ↔ Forall₂ (fun x x_1 => r x x_1 = true) (a :: as) (b :: bs)
<VAR>z : ℂ<VAR>x : ℚ<GOAL>(z / ↑x).re = z.re / ↑x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasDerivedCategory C<VAR>T : Triangle (DerivedCategory C)<VAR>hT : T ∈ distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(homologyFunctor C n₀).map T.mor₁ ≫ (homologyFunctor C n₀).map T.mor₂ = 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>d : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(changeForm h) ((contractLeft d) x) = (contractLeft d) ((changeForm h) x)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>d : Module.Dual R M<VAR>r : R<GOAL>(changeForm h) ((contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r)) = (contractLeft d) ((changeForm h) ((algebraMap R (CliffordAlgebra Q)) r))
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>d : Module.Dual R M<VAR>x y : CliffordAlgebra Q<VAR>hx : (changeForm h) ((contractLeft d) x) = (contractLeft d) ((changeForm h) x)<VAR>hy : (changeForm h) ((contractLeft d) y) = (contractLeft d) ((changeForm h) y)<GOAL>(changeForm h) ((contractLeft d) (x + y)) = (contractLeft d) ((changeForm h) (x + y))
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>d : Module.Dual R M<VAR>m : CliffordAlgebra Q<VAR>x : M<VAR>hx : (changeForm h) ((contractLeft d) m) = (contractLeft d) ((changeForm h) m)<GOAL>(changeForm h) ((contractLeft d) ((ι Q) x * m)) = (contractLeft d) ((changeForm h) ((ι Q) x * m))
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>G' : Type u_2<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>h : Group.IsNilpotent G<GOAL>Group.nilpotencyClass G' ≤ Group.nilpotencyClass G
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>G' : Type u_2<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>h : Group.IsNilpotent G<GOAL>∀ (n : ℕ), upperCentralSeries G n = ⊤ → upperCentralSeries G' n = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>G' : Type u_2<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>h : Group.IsNilpotent G<VAR>n : ℕ<VAR>hn : upperCentralSeries G n = ⊤<GOAL>upperCentralSeries G' n = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>G' : Type u_2<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>h : Group.IsNilpotent G<VAR>n : ℕ<VAR>hn : upperCentralSeries G n = ⊤<GOAL>⊤ ≤ upperCentralSeries G' n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>inst✝ : ContinuousMul α<VAR>hf : Tendsto (fun s => ∏ b ∈ s, f b) atTop (𝓝 a)<VAR>hg : Tendsto (fun s => ∏ b ∈ s, g b) atTop (𝓝 b)<GOAL>Tendsto (fun s => ∏ b ∈ s, f b * g b) atTop (𝓝 (a * b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>inst✝ : ContinuousMul α<VAR>hf : Tendsto (fun s => ∏ b ∈ s, f b) atTop (𝓝 a)<VAR>hg : Tendsto (fun s => ∏ b ∈ s, g b) atTop (𝓝 b)<GOAL>Tendsto (fun s => (∏ x ∈ s, f x) * ∏ x ∈ s, g x) atTop (𝓝 (a * b))
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝² : SetLike S G<VAR>inst✝¹ : DivisionMonoid G<VAR>inst✝ : SubgroupClass S G<VAR>H : S<GOAL>↑H / ↑H = ↑H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hfi : Integrable f μ<GOAL>(μ.withDensityᵥ f).trim hm ≪ᵥ (μ.trim hm).toENNRealVectorMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hfi : Integrable f μ<VAR>j : Set α<VAR>hj₁ : MeasurableSet j<VAR>hj₂ : ↑(μ.trim hm).toENNRealVectorMeasure j = 0<GOAL>↑((μ.withDensityᵥ f).trim hm) j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hfi : Integrable f μ<VAR>j : Set α<VAR>hj₁ : MeasurableSet j<VAR>hj₂ : μ j = 0<GOAL>↑((μ.withDensityᵥ f).trim hm) j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hfi : Integrable f μ<VAR>j : Set α<VAR>hj₁ : MeasurableSet j<VAR>hj₂ : μ j = 0<GOAL>∫ (x : α) in j, f x ∂μ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>V : Set β<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ V)<VAR>hU : x ∈ U<VAR>φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)<GOAL>TendstoUniformlyOn F (F x) (𝓝[U] x) V
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>V : Set β<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ V)<VAR>hU : x ∈ U<VAR>φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)<GOAL>Tendsto (fun q => (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>V : Set β<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ V)<VAR>hU : x ∈ U<VAR>φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)<GOAL>Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>V : Set β<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ V)<VAR>hU : x ∈ U<VAR>φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)<GOAL>Tendsto (Prod.map (↿F) ↿F ∘ φ) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V)) (𝓤 γ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>V : Set β<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ V)<VAR>hU : x ∈ U<VAR>φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)<GOAL>Tendsto φ (comap Prod.fst (𝓝 x)) (𝓤 (α × β))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>V : Set β<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ V)<VAR>hU : x ∈ U<VAR>φ : α × β → (α × β) × α × β := fun q => ((x, q.2), q)<GOAL>Tendsto (fun x_1 => ((x, x_1.1), x_1.2, x_1.2)) (comap (fun x_1 => (x, x_1.1)) (𝓤 α)) (𝓤 α ×ˢ 𝓤 β)
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>K : Type u_1<VAR>inst✝ : DivisionRing K<VAR>p q : K[X]<VAR>h : q ≠ 0<GOAL>(p * C q.leadingCoeff⁻¹).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>K : Type u_1<VAR>inst✝ : DivisionRing K<VAR>p q : K[X]<VAR>h : q ≠ 0<VAR>h₁ : q.leadingCoeff⁻¹ ≠ 0<GOAL>(p * C q.leadingCoeff⁻¹).degree = p.degree
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' Ioo ↑x ↑y = Ioo x y
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ↑y) = Ioi x ∩ Iio y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>l : Filter α<VAR>p : β → Prop<VAR>f : α → β<VAR>hf : Tendsto f l atTop<VAR>h_evtl : ∀ᶠ (x : β) in atTop, p x<GOAL>∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>l : Filter α<VAR>p : β → Prop<VAR>f : α → β<VAR>hf : Tendsto f l atTop<VAR>h_evtl : ∀ᶠ (x : β) in atTop, ∀ (y : β), x ≤ y → p y<GOAL>∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
<VAR>pqr : Multiset ℕ+<VAR>H : E' 3 = pqr<GOAL>1 < sumInv pqr
<VAR>pqr : Multiset ℕ+<VAR>H : E' 4 = pqr<GOAL>1 < sumInv pqr
<VAR>pqr : Multiset ℕ+<VAR>H : E' 5 = pqr<GOAL>1 < sumInv pqr
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>μ : K<VAR>n : ℕ<GOAL>Submodule.map f (LinearMap.range ((f - (algebraMap K (End K V)) μ) ^ n)) = LinearMap.range (f * (f - (algebraMap K (End K V)) μ) ^ n)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>μ : K<VAR>n : ℕ<GOAL>LinearMap.range (f * (f - (algebraMap K (End K V)) μ) ^ n) = LinearMap.range ((f - (algebraMap K (End K V)) μ) ^ n * f)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≤ l.length<GOAL>n < (insertNth n x l).length
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝¹⁷ : Semiring R₁<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M₁<VAR>inst✝¹³ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹² : TopologicalSpace M'₁<VAR>inst✝¹¹ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace M₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝⁸ : TopologicalSpace M₃<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁶ : TopologicalSpace M₄<VAR>inst✝⁵ : AddCommMonoid M₄<VAR>inst✝⁴ : Module R₁ M₁<VAR>inst✝³ : Module R₁ M'₁<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>inst✝ : Module R₁ M₂<VAR>f : M₁ →L[R₁] M₂<VAR>c : R₁<VAR>x : M₁<GOAL>f (c • x) = c • f x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : AddCommGroup M''<VAR>inst✝¹ : Module R M''<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>r : R<VAR>inst✝ : IsNoetherianRing R<GOAL>{r | ∃ x, x ≠ 0 ∧ r • x = 0} = {r | IsSMulRegular M r}ᶜ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : CommSemiring α<VAR>s : Finset ι<VAR>f g : ι → α<GOAL>∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : CommSemiring α<VAR>s : Finset ι<VAR>f g : ι → α<GOAL>∀ (a : ι) (s : Finset ι), (∀ x ∈ s, x < a) → ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j → ∏ i ∈ insert a s, (f i + g i) = ∏ i ∈ insert a s, f i + ∑ i ∈ insert a s, (g i * ∏ j ∈ filter (fun x => x < i) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => i < j) (insert a s), f j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a✝ : α<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : CommSemiring α<VAR>f g : ι → α<VAR>a : ι<VAR>s : Finset ι<VAR>ha : ∀ x ∈ s, x < a<VAR>ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j<GOAL>∏ i ∈ insert a s, (f i + g i) = ∏ i ∈ insert a s, f i + ∑ i ∈ insert a s, (g i * ∏ j ∈ filter (fun x => x < i) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => i < j) (insert a s), f j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a✝ : α<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : CommSemiring α<VAR>f g : ι → α<VAR>a : ι<VAR>s : Finset ι<VAR>ha : ∀ x ∈ s, x < a<VAR>ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j<VAR>ha' : a ∉ s<GOAL>∏ i ∈ insert a s, (f i + g i) = ∏ i ∈ insert a s, f i + ∑ i ∈ insert a s, (g i * ∏ j ∈ filter (fun x => x < i) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => i < j) (insert a s), f j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a✝ : α<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : CommSemiring α<VAR>f g : ι → α<VAR>a : ι<VAR>s : Finset ι<VAR>ha : ∀ x ∈ s, x < a<VAR>ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j<VAR>ha' : a ∉ s<GOAL>f a * ∏ i ∈ s, f i + (f a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j + (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j)) = f a * ∏ x ∈ s, f x + ((g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) * ∏ j ∈ filter (fun j => a < j) (insert a s), f j + ∑ x ∈ s, (g x * ∏ j ∈ filter (fun x_1 => x_1 < x) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => x < j) (insert a s), f j)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a✝ : α<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : CommSemiring α<VAR>f g : ι → α<VAR>a : ι<VAR>s : Finset ι<VAR>ha : ∀ x ∈ s, x < a<VAR>ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j<VAR>ha' : a ∉ s<GOAL>f a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j + (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) = (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) * ∏ j ∈ filter (fun j => a < j) (insert a s), f j + ∑ x ∈ s, (g x * ∏ j ∈ filter (fun x_1 => x_1 < x) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => x < j) (insert a s), f j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a✝ : α<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : CommSemiring α<VAR>f g : ι → α<VAR>a : ι<VAR>s : Finset ι<VAR>ha : ∀ x ∈ s, x < a<VAR>ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j<VAR>ha' : a ∉ s<GOAL>g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j + f a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j = (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) * ∏ j ∈ filter (fun j => a < j) (insert a s), f j + ∑ x ∈ s, (g x * ∏ j ∈ filter (fun x_1 => x_1 < x) (insert a s), (f j + g j)) * ∏ j ∈ filter (fun j => x < j) (insert a s), f j
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>D : ℕ := rankOfDiscrBdd N<VAR>B : ℝ≥0 := boundOfDiscBdd N<VAR>C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊<GOAL>{K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}.Finite