ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>‖((let __src := liftEquiv 𝕜 E (⨂[𝕜] (i : ι), E' i); { toLinearEquiv := __src, norm_map' := ⋯ }) ((tprodL 𝕜).compContinuousLinearMap f)) x‖ ≤ (∏ i : ι, ‖f i‖) * ‖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>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>‖(lift ((tprodL 𝕜).compContinuousLinearMap f).toMultilinearMap) x‖ ≤ (∏ i : ι, ‖f i‖) * ‖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>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>‖(tprodL 𝕜).compContinuousLinearMap f‖ ≤ ∏ i : ι, ‖f i‖
<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>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>∀ (m : (i : ι) → E i), ‖((tprodL 𝕜).compContinuousLinearMap f) m‖ ≤ (∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
<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>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>m : (i : ι) → E i<GOAL>‖((tprodL 𝕜).compContinuousLinearMap f) m‖ ≤ (∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
<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>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>m : (i : ι) → E i<GOAL>‖(tprodL 𝕜) fun i => (f i) (m i)‖ ≤ (∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
<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>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>m : (i : ι) → E i<GOAL>∏ i : ι, ‖(f i) (m i)‖ ≤ (∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
<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>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>m : (i : ι) → E i<GOAL>∏ i : ι, ‖(f i) (m i)‖ ≤ ∏ x : ι, ‖f x‖ * ‖m x‖
<VAR>x y : ℝ<GOAL>Tendsto (fun x => log (rexp x)) atTop atTop
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.op.δ.unop = S.δ.op.unop
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>(pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop = (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>((pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop).op = ((pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop).op
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>Collinear k {p₁, p₂, p₃, p₄, p₅}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>Collinear k {p₄, p₅}
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>(x ^ n).toNNReal = x.toNNReal ^ n
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z : ℝ≥0∞<VAR>h1 : x ≠ 0<VAR>h2 : x ≠ ⊤<GOAL>x⁻¹ * y ≤ z ↔ y ≤ x * z
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_succ_n : IntFractPair K<GOAL>IntFractPair.stream v (n + 1) = some ifp_succ_n ↔ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>p : α → Bool<VAR>f : β → α<VAR>b : β<VAR>l : List β<GOAL>eraseP p (map f (b :: l)) = map f (eraseP (p ∘ f) (b :: l))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ (s ∩ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>e : ↑s ↪ ↑t<GOAL>s.encard ≤ t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>e : ↑s ↪ ↑t<GOAL>((fun a => ↑a) '' (⇑e '' univ)).encard ≤ t.encard
<VAR>R✝ : Type u<VAR>inst✝¹ : LinearOrderedAddCommMonoidWithTop R✝<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedAddCommMonoid R<VAR>a b : Tropical (WithTop R)<GOAL>a * b = 0 ↔ a = 0 ∨ b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : β → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => ∫⁻ (b : β) in s, f b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : β → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable (uncurry fun a => f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>hf : Continuous f<GOAL>SpecializingMap f ↔ ∀ (x : X), f '' closure {x} = closure {f x}
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.IsReflection t ∧ cs.length (w * t * t) < cs.length (w * t) ↔ ¬(cs.IsReflection t ∧ cs.length (w * t) < cs.length w)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.length w < cs.length (w * t) ↔ cs.length w ≤ cs.length (w * t)
<VAR>x✝ y✝ x y : ℝ<VAR>hx : x ∈ Icc (-1) 1<VAR>hy : y ∈ Icc (-(π / 2)) (π / 2)<GOAL>arcsin x ≤ y ↔ x ≤ sin y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>(eval P) (X 1 ^ 2 * X 2 + C W.a₁ * X 0 * X 1 * X 2 + C W.a₃ * X 1 * X 2 ^ 2 - (X 0 ^ 3 + C W.a₂ * X 0 ^ 2 * X 2 + C W.a₄ * X 0 * X 2 ^ 2 + C W.a₆ * X 2 ^ 3)) = P 1 ^ 2 * P 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 2 - (P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 + W.a₄ * P 0 * P 2 ^ 2 + W.a₆ * P 2 ^ 3)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝¹ : Monoid N✝<VAR>N : Type u_4<VAR>inst✝ : Monoid N<VAR>f : (i : ι) → M i →* N<VAR>s : Submonoid N<GOAL>MonoidHom.mrange (lift f) ≤ s ↔ ∀ (i : ι), MonoidHom.mrange (f i) ≤ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>mα : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<VAR>h : MeasurableSet (f '' s)<GOAL>MeasurableSet s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>x : E<VAR>y : NormedSpace.Dual 𝕜 E<GOAL>⟪(toDual 𝕜 E).symm y, x⟫_𝕜 = y x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>x : E<VAR>y : NormedSpace.Dual 𝕜 E<GOAL>((toDual 𝕜 E) ((toDual 𝕜 E).symm y)) x = y x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : SemilatticeInf α<VAR>b c : α<VAR>inst✝ : OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>ha : InfIrred ⊤<GOAL>False
<VAR>x : ℝ≥0∞<GOAL>x ^ (-1) = x⁻¹
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPullback<VAR>e : sq₁ ≅ sq₂<GOAL>sq₂.IsPullback
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPullback<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPullback<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPullback<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPullback<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<VAR>f : E →ₐ[F] K<GOAL>(f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>hC0 : C ≤ 0<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>hC0 : 0 < C<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>hC0 : 0 < C<VAR>hfi : Integrable f μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>hC0 : 0 < C<VAR>hfi : Integrable f μ<VAR>hμt : μ univ = ⊤<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>hC0 : 0 < C<VAR>hfi : Integrable f μ<VAR>hμt : μ univ < ⊤<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<VAR>hC0 : 0 < C<VAR>hfi : Integrable f μ<VAR>hμt : μ univ < ⊤<VAR>this : IsFiniteMeasure μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>hC0 : 0 < C<VAR>hfi : Integrable f μ<VAR>hμt : μ univ < ⊤<VAR>this : IsFiniteMeasure μ<VAR>h_le : ∀ᵐ (x : α) ∂μ, f x ∈ closedBall 0 C<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>y : ℝ<VAR>hXm : AEMeasurable X ℙ<GOAL>Measure.map (fun ω => X ω + y) ℙ = gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>y : ℝ<VAR>hXm : AEMeasurable X ℙ<GOAL>Measure.map ((fun ω => ω + y) ∘ X) ℙ = gaussianReal (μ + y) v
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))<VAR>B : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))<VAR>B : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))<VAR>ω : Ω<VAR>hωpos : Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))<VAR>hωneg : Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))<GOAL>Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))<VAR>B : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))<VAR>ω : Ω<VAR>hωpos : Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))<VAR>hωneg : Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))<GOAL>(fun n => (∑ i ∈ range n, X i ω) / ↑n) = fun x => (∑ i ∈ range x, (pos ∘ X i) ω) / ↑x - (∑ i ∈ range x, (neg ∘ X i) ω) / ↑x
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))<VAR>B : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))<VAR>ω : Ω<VAR>hωpos : Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))<VAR>hωneg : Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))<GOAL>𝓝 (∫ (a : Ω), X 0 a) = 𝓝 ((∫ (a : Ω), (pos ∘ X 0) a) - ∫ (a : Ω), (neg ∘ X 0) a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>m : Multiset α<VAR>xs : List α<GOAL>(Multiset.sym2 ⟦xs⟧).dedup = (dedup ⟦xs⟧).sym2
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Cycle α<VAR>hs : s.reverse.Nodup<VAR>x : α<VAR>hx : x ∈ s.reverse<GOAL>s.reverse.next hs x hx = s.prev ⋯ x ⋯
<VAR>G : Type w<VAR>inst✝³ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : R1Space G<VAR>inst✝ : BorelSpace G<VAR>H : μ.ContentRegular<VAR>K : Compacts G<GOAL>μ.measure ↑K = (fun s => ↑(μ.toFun s)) K
<VAR>G : Type w<VAR>inst✝³ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : R1Space G<VAR>inst✝ : BorelSpace G<VAR>H : μ.ContentRegular<VAR>K : Compacts G<GOAL>μ.measure ↑K ≤ (fun s => ↑(μ.toFun s)) K
<VAR>G : Type w<VAR>inst✝³ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : R1Space G<VAR>inst✝ : BorelSpace G<VAR>H : μ.ContentRegular<VAR>K : Compacts G<GOAL>(fun s => ↑(μ.toFun s)) K ≤ μ.measure ↑K