ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>h_meas_f : AEMeasurable f μ<VAR>h_meas_g : AEMeasurable g μ<VAR>h_indep_fun : IndepFun f g μ<VAR>fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g<GOAL>∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>h_meas_f : AEMeasurable f μ<VAR>h_meas_g : AEMeasurable g μ<VAR>h_indep_fun : IndepFun f g μ<VAR>fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g<GOAL>∫⁻ (a : Ω), (AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g) a ∂μ = (∫⁻ (a : Ω), AEMeasurable.mk f h_meas_f a ∂μ) * ∫⁻ (a : Ω), AEMeasurable.mk g h_meas_g a ∂μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>h_meas_f : AEMeasurable f μ<VAR>h_meas_g : AEMeasurable g μ<VAR>h_indep_fun : IndepFun f g μ<VAR>fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g<GOAL>IndepFun (AEMeasurable.mk f h_meas_f) (AEMeasurable.mk g h_meas_g) μ
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type ?u.153874<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>x : M₁'<VAR>i : ι₂<VAR>y : M₂ i<GOAL>(directSumRight R M₁' M₂).symm ((lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] (lof R ι₂ M₂ i) y
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝³ : PseudoEMetricSpace X<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>inst✝ : IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>(fun x => c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>comap (fun x_1 => x * x_1) (𝓝[>] 0) = 𝓝[>] 0
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>comap (fun x_1 => x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0) = 𝓝 0 ⊓ 𝓟 (Ioi 0)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>comap (fun x_1 => x * x_1) (𝓝 0) = 𝓝 0
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>𝓝 ((Homeomorph.mulLeft₀ x ⋯).symm 0) = 𝓝 0
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>D_lt_one : D < 1<VAR>hx : x ∈ ball 0 (1 + D)<GOAL>0 < y D x
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>D_lt_one : D < 1<VAR>hx : ‖x‖ < 1 + D<GOAL>0 < y D x
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>D_lt_one : D < 1<VAR>hx : ‖x‖ < 1 + D<GOAL>Integrable (fun i => w D i * φ (x - i)) μ
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>D_lt_one : D < 1<VAR>hx : ‖x‖ < 1 + D<GOAL>0 < μ (support fun i => w D i * φ (x - i))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<GOAL>AnalyticWithinOn 𝕜 f univ ↔ AnalyticOn 𝕜 f univ
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>c₁✝ c₂✝ r x y z : R<VAR>a✝ b c : ℍ[R,c₁✝,c₂✝]<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a = -a ↔ a.re = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁴ : OrderedCommRing R<VAR>inst✝¹³ : StarRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.846623) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁴ : OrderedCommRing R<VAR>inst✝¹³ : StarRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>(∀ (a_1 : ↑(spectrum R a)), { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } a_1 ≤ { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ } a_1) ↔ ∀ x ∈ spectrum R a, f x ≤ g x
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁵ : CommSemiring R✝<VAR>inst✝⁴ : Semiring A✝<VAR>inst✝³ : Algebra R✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<GOAL>toSubmodule S * toSubmodule T = toSubmodule (S ⊔ T)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁵ : CommSemiring R✝<VAR>inst✝⁴ : Semiring A✝<VAR>inst✝³ : Algebra R✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<GOAL>toSubmodule (S ⊔ T) ≤ toSubmodule S * toSubmodule T
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁵ : CommSemiring R✝<VAR>inst✝⁴ : Semiring A✝<VAR>inst✝³ : Algebra R✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<VAR>x : A<VAR>hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)<GOAL>x ∈ toSubmodule S * toSubmodule T
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁵ : CommSemiring R✝<VAR>inst✝⁴ : Semiring A✝<VAR>inst✝³ : Algebra R✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<VAR>x✝ : A<VAR>hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)<VAR>x : A<VAR>hx : x ∈ ↑S ∪ ↑T<GOAL>x ∈ toSubmodule S * toSubmodule T
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁵ : CommSemiring R✝<VAR>inst✝⁴ : Semiring A✝<VAR>inst✝³ : Algebra R✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<VAR>x : A<VAR>hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)<VAR>r : R<GOAL>(algebraMap R A) r ∈ toSubmodule S * toSubmodule T
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁵ : CommSemiring R✝<VAR>inst✝⁴ : Semiring A✝<VAR>inst✝³ : Algebra R✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<VAR>x✝ : A<VAR>hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)<VAR>x y : A<VAR>hx : x ∈ toSubmodule S * toSubmodule T<VAR>hy : y ∈ toSubmodule S * toSubmodule T<GOAL>x * y ∈ toSubmodule S * toSubmodule T
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁵ : CommSemiring R✝<VAR>inst✝⁴ : Semiring A✝<VAR>inst✝³ : Algebra R✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<VAR>x✝ : A<VAR>hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)<VAR>x y : A<VAR>hx : x ∈ toSubmodule S * toSubmodule T<VAR>hy : y ∈ toSubmodule S * toSubmodule T<VAR>this : x * y ∈ toSubmodule S * toSubmodule T * (toSubmodule S * toSubmodule T)<GOAL>x * y ∈ toSubmodule S * toSubmodule T
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(W.variableChange C).b₆ = ↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 + 4 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) = ↑C.u⁻¹ ^ 6 * (W.a₃ ^ 2 + 4 * W.a₆ + 2 * C.r * (2 * W.a₄ + W.a₁ * W.a₃) + C.r ^ 2 * (W.a₁ ^ 2 + 4 * W.a₂) + 4 * C.r ^ 3)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁸ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : SFinite μ<VAR>f : X → ℝ≥0<VAR>s : Set X<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>g : X → E<GOAL>(∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasStrictDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>inst✝ : P.IsFinite<GOAL>P.ker.FG
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>inst✝ : P.IsFinite<GOAL>Ideal.span ↑⋯.toFinset = P.ker
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G : MonCat<VAR>inst✝ : MonoidalCategory V<GOAL>(Monoidal.fromTransported (functorCategoryEquivalence V G).symm).ε.app PUnit.unit = 𝟙 ((𝟙_ (SingleObj ↑G ⥤ V)).obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G : MonCat<VAR>inst✝ : MonoidalCategory V<GOAL>((functorCategoryEquivalence V G).symm.unitIso.hom.app (𝟙_ (SingleObj ↑G ⥤ V))).app PUnit.unit = 𝟙 ((𝟙_ (SingleObj ↑G ⥤ V)).obj PUnit.unit)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsBezout R<VAR>inst✝ : GCDMonoid R<VAR>x y : R<GOAL>Ideal.span {gcd x y} = Ideal.span {x, y}
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>a : S<VAR>x✝ : IsAlgebraic R a<VAR>f : R[X]<VAR>hf₁ : f ≠ 0<VAR>hf₂ : (aeval a) f = 0<GOAL>(aeval ((algebraMap S A) a)) f = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A * C).card * B.card ≤ (A * B).card * (B / C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A / C⁻¹).card * B.card ≤ (A * B).card * (B * C⁻¹).card
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>φ : L.BoundedFormula α (n + 1)<VAR>con : (∀'φ).IsAtomic<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>s : Set α<VAR>t : Set β<VAR>S : (i : ι) → Set (π i)<GOAL>IsBounded (s ×ˢ s) ↔ IsBounded s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>t : Set β<VAR>S : (i : ι) → Set (π i)<GOAL>IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>s : Set α<VAR>t : Set β<VAR>S : (i : ι) → Set (π i)<VAR>hs : s.Nonempty<GOAL>IsBounded (s ×ˢ s) ↔ IsBounded s
<VAR>ι : Type u_1<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Fintype ι<VAR>x : EuclideanSpace ℝ ι<VAR>r : ℝ<GOAL>volume (Metric.closedBall x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I✝ J X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<VAR>I : Set α<GOAL>I ∈ {I | M.Basis I X} ↔ I ∈ maximals (fun x x_1 => x ⊆ x_1) ({I | M.Indep I} ∩ Iic X)
<VAR>a b : ℕ<VAR>ha2 : a % 2 = 1<VAR>hb2 : b % 2 = 1<GOAL>(if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)
<VAR>a b : ℕ<VAR>ha2 : a % 2 = 1<VAR>hb2 : b % 2 = 1<VAR>ha1 : a % 4 = 1<GOAL>(if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)
<VAR>a b : ℕ<VAR>ha2 : a % 2 = 1<VAR>hb2 : b % 2 = 1<VAR>ha3 : a % 4 = 3<GOAL>(if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)
<VAR>a b : ℕ<VAR>ha2 : a % 2 = 1<VAR>hb2 : b % 2 = 1<VAR>ha3 : a % 4 = 3<VAR>hb1 : b % 4 = 1<GOAL>(if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)
<VAR>a b : ℕ<VAR>ha2 : a % 2 = 1<VAR>hb2 : b % 2 = 1<VAR>ha3 : a % 4 = 3<VAR>hb3 : b % 4 = 3<GOAL>(if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<VAR>f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := f'₀.mkContinuous ‖f‖ hf'₀<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<VAR>f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := f'₀.mkContinuous ‖f‖ hf'₀<VAR>hnorm : ‖f'‖ ≤ ‖f‖<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<VAR>f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := f'₀.mkContinuous ‖f‖ hf'₀<VAR>hnorm : ‖f'‖ ≤ ‖f‖<VAR>heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<VAR>f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := f'₀.mkContinuous ‖f‖ hf'₀<VAR>hnorm : ‖f'‖ ≤ ‖f‖<VAR>heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x<GOAL>‖(lift f'.toMultilinearMap) x‖ ≤ ‖f'‖ * injectiveSeminorm x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)<VAR>G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)<VAR>e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜] ↥(LinearMap.range (lift f.toMultilinearMap)) := (lift f.toMultilinearMap).quotKerEquivRange<VAR>this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e<VAR>this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e<VAR>f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)<VAR>hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖<VAR>f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) := f'₀.mkContinuous ‖f‖ hf'₀<VAR>hnorm : ‖f'‖ ≤ ‖f‖<VAR>heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x<VAR>hle : (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ injectiveSeminorm<GOAL>‖(lift f'.toMultilinearMap) x‖ ≤ ‖f'‖ * injectiveSeminorm x