ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)<VAR>h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν<VAR>this : SigmaFinite μ'<VAR>hμ' : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun x => (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x<VAR>x : α<VAR>hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x<VAR>hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x<VAR>hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x<GOAL>μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
<VAR>C : Type u_2<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>S S₁ S₂ : ShortComplex C<VAR>A : C<VAR>γ : A ⟶ S.homology<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ
<VAR>C : Type u_2<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>S S₁ S₂ : ShortComplex C<VAR>A : C<VAR>γ : A ⟶ S.homology<VAR>A' : C<VAR>π : A' ⟶ A<VAR>hπ : Epi π<VAR>z : A' ⟶ S.cycles<VAR>hz : π ≫ γ = z ≫ S.homologyπ<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ
<VAR>C : Type u_2<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>S S₁ S₂ : ShortComplex C<VAR>A : C<VAR>γ : A ⟶ S.homology<VAR>A' : C<VAR>π : A' ⟶ A<VAR>hπ : Epi π<VAR>z : A' ⟶ S.cycles<VAR>hz : π ≫ γ = z ≫ S.homologyπ<GOAL>z = S.liftCycles (z ≫ S.iCycles) ⋯
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<GOAL>SwapTrue o x (term I ho) = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f g : α → β<VAR>h : Option.map f = Option.map g<VAR>x : α<GOAL>some (f x) = some (g x)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι✝ : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι : Type u_10<VAR>inst✝ : Nonempty ι<VAR>p : Seminorm 𝕜 E<VAR>q : ι' → Seminorm 𝕜₂ F<VAR>f : E →ₛₗ[σ₁₂] F<VAR>h : ∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p<VAR>i : ι'<GOAL>∃ s C, (q i).comp f ≤ C • s.sup fun x => p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι✝ : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι : Type u_10<VAR>inst✝ : Nonempty ι<VAR>p : Seminorm 𝕜 E<VAR>q : ι' → Seminorm 𝕜₂ F<VAR>f : E →ₛₗ[σ₁₂] F<VAR>h : ∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p<VAR>i : ι'<GOAL>∃ C, (q i).comp f ≤ C • {Classical.arbitrary ι}.sup fun x => p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : LocallyIntegrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : LocallyIntegrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<GOAL>f =ᶠ[ae (μ.restrict (⋃ n, closure (compactCovering β n)))] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : LocallyIntegrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>n : ℕ<GOAL>∀ᵐ (x : β) ∂μ.restrict (closure (compactCovering β n)), f x = 0 x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : LocallyIntegrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>n : ℕ<GOAL>Integrable f (μ.restrict (closure (compactCovering β n)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : LocallyIntegrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>n : ℕ<GOAL>∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ.restrict (closure (compactCovering β n)) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>hf : QuotientMap f<VAR>h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})<VAR>a : α<GOAL>f '' connectedComponent a = connectedComponent (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a✝ a' : α<VAR>b✝ : M<VAR>a x : α<VAR>b : M<GOAL>(single a b) x ≠ 0 ↔ x = a ∧ b ≠ 0
<VAR>n : ℕ<GOAL>antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
<VAR>n : ℕ<GOAL>(0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
<VAR>x y : ℂ<GOAL>cexp (x + y * I) = cexp x * (cos y + sin y * I)
<VAR>α✝ : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α✝ → E<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α✝<VAR>α : Type u_7<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → G<GOAL>∫ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫ (x : α) in s, f x ∂μ
<VAR>α✝ : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α✝ → E<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α✝<VAR>α : Type u_7<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → G<GOAL>∫ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫ (x : α), f x ∂Measure.map Subtype.val (Measure.comap Subtype.val μ)
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid Q<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R Q<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>f : Dual R M<VAR>n : N<VAR>g : Dual R N<VAR>p : P<VAR>m : M<GOAL>((dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n)) m = (g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)) m
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid Q<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R Q<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>f : Dual R M<VAR>n : N<VAR>g : Dual R N<VAR>p : P<VAR>m : M<GOAL>f m • g n • p = g n • f m • p
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>inst✝³ : CommMonoidWithZero M₀<VAR>p : ι → Prop<VAR>inst✝² : DecidablePred p<VAR>f : ι → M₀<VAR>s : Finset ι<VAR>i : ι<VAR>inst✝¹ : Nontrivial M₀<VAR>inst✝ : NoZeroDivisors M₀<GOAL>∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>inst✝³ : CommMonoidWithZero M₀<VAR>p : ι → Prop<VAR>inst✝² : DecidablePred p<VAR>f : ι → M₀<VAR>s : Finset ι<VAR>i : ι<VAR>inst✝¹ : Nontrivial M₀<VAR>inst✝ : NoZeroDivisors M₀<GOAL>(¬∃ a ∈ s, f a = 0) ↔ ∀ a ∈ s, f a ≠ 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>inst✝³ : CommMonoidWithZero M₀<VAR>p : ι → Prop<VAR>inst✝² : DecidablePred p<VAR>f : ι → M₀<VAR>s : Finset ι<VAR>i : ι<VAR>inst✝¹ : Nontrivial M₀<VAR>inst✝ : NoZeroDivisors M₀<GOAL>(∀ a ∈ s, f a ≠ 0) ↔ ∀ a ∈ s, f a ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>t : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>⨅ r, (ρ.IicSnd ↑↑r) s = (ρ.IicSnd ↑t) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<GOAL>Tendsto defaultRatCDF atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<GOAL>(fun x => 1) =ᶠ[atTop] defaultRatCDF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<GOAL>∃ a, ∀ b ≥ a, 1 = defaultRatCDF b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>¬IsMax a ↔ ∃ b, a < b
<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>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
<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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
<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>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0<GOAL>∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<GOAL>S.leftInv.leftInv = S
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<GOAL>S ≤ S.leftInv.leftInv
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : M<VAR>hx : x ∈ S<GOAL>x ∈ S.leftInv.leftInv
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : M<VAR>hx : x ∈ S<VAR>this : x = ↑(IsUnit.unit ⋯)⁻¹⁻¹<GOAL>x ∈ S.leftInv.leftInv
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : M<VAR>hx : x ∈ S<VAR>this : x = ↑(IsUnit.unit ⋯)⁻¹⁻¹<GOAL>↑(IsUnit.unit ⋯)⁻¹⁻¹ ∈ S.leftInv.leftInv
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ measurableCylinders α<VAR>ht : t ∈ measurableCylinders α<GOAL>s ∪ t ∈ measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ measurableCylinders α<VAR>ht : t ∈ measurableCylinders α<GOAL>(sᶜ ∩ tᶜ)ᶜ ∈ measurableCylinders α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>u v : UniformSpace G<VAR>hu : UniformGroup G<VAR>hv : UniformGroup G<VAR>h : 𝓝 1 = 𝓝 1<GOAL>𝓤 G = 𝓤 G
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<GOAL>eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm f q μ * eLpNorm g r μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<GOAL>eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm f q μ * eLpNorm g r μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<VAR>hr_ne_zero : r ≠ 0<GOAL>eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm f q μ * eLpNorm g r μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<VAR>hr_ne_zero : r ≠ 0<VAR>hq_top : ¬q = ⊤<VAR>hr_top : ¬r = ⊤<VAR>hpq : p < q<GOAL>eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm f q μ * eLpNorm g r μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<VAR>hr_ne_zero : r ≠ 0<VAR>hq_top : ¬q = ⊤<VAR>hr_top : ¬r = ⊤<VAR>hpq : p < q<GOAL>eLpNorm' (fun x => b (f x) (g x)) p.toReal μ ≤ eLpNorm' f q.toReal μ * eLpNorm' g r.toReal μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<VAR>hr_ne_zero : r ≠ 0<VAR>hq_top : ¬q = ⊤<VAR>hr_top : ¬r = ⊤<VAR>hpq : p < q<GOAL>0 < p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<VAR>hr_ne_zero : r ≠ 0<VAR>hq_top : ¬q = ⊤<VAR>hr_top : ¬r = ⊤<VAR>hpq : p < q<GOAL>p.toReal < q.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<VAR>hr_ne_zero : r ≠ 0<VAR>hq_top : ¬q = ⊤<VAR>hr_top : ¬r = ⊤<VAR>hpq : p < q<GOAL>1 / p.toReal = 1 / q.toReal + 1 / r.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<VAR>hr_ne_zero : r ≠ 0<VAR>hq_top : ¬q = ⊤<VAR>hr_top : ¬r = ⊤<VAR>hpq : p < q<GOAL>1 / q ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>hp_zero : ¬p = 0<VAR>hq_ne_zero : q ≠ 0<VAR>hr_ne_zero : r ≠ 0<VAR>hq_top : ¬q = ⊤<VAR>hr_top : ¬r = ⊤<VAR>hpq : p < q<GOAL>1 / r ≠ ⊤
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<GOAL>μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<GOAL>∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≤ ∫⁻ (ω : Ω), ↑(g ω) + edist f g ∂↑μ
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<GOAL>(fun a => ↑(f a)) ≤ fun a => ↑(g a) + edist f g
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<VAR>le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)<GOAL>(fun a => ↑(f a)) ≤ fun a => ↑(g a) + edist f g
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<VAR>le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)<VAR>ω : Ω<GOAL>(fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<VAR>le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)<VAR>ω : Ω<VAR>le' : f ω ≤ g ω + nndist f g<GOAL>(fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f g : Ω →ᵇ ℝ≥0<VAR>le_dist : ∀ (ω : Ω), dist (f ω) (g ω) ≤ ↑(nndist f g)<VAR>ω : Ω<VAR>le' : f ω ≤ g ω + nndist f g<VAR>le : ↑(f ω) ≤ ↑(g ω) + ↑(nndist f g)<GOAL>(fun a => ↑(f a)) ω ≤ (fun a => ↑(g a) + edist f g) ω
<VAR>s : Finset ℕ<VAR>m✝ n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<VAR>m : ℕ<VAR>m2 : 2 ≤ m<VAR>md : m * m ∣ n<GOAL>d ≤ m
<VAR>s : Finset ℕ<VAR>m✝ n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<VAR>m : ℕ<VAR>m2 : 2 ≤ m<VAR>md : m * m ∣ n<VAR>this : n.MinSqFacProp n.minSqFac<GOAL>d ≤ m
<VAR>s : Finset ℕ<VAR>m✝ n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<VAR>m : ℕ<VAR>m2 : 2 ≤ m<VAR>md : m * m ∣ n<VAR>this : n.MinSqFacProp (some d)<GOAL>d ≤ m
<VAR>s : Finset ℕ<VAR>m✝ n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<VAR>m : ℕ<VAR>m2 : 2 ≤ m<VAR>md : m * m ∣ n<VAR>this : n.MinSqFacProp (some d)<VAR>fd : m.minFac ∣ m<GOAL>d ≤ m
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I J : Submodule R₁ K<VAR>aI : R₁<VAR>haI : aI ∈ R₁⁰<VAR>hI : ∀ b ∈ I, IsInteger R₁ (aI • b)<VAR>aJ : R₁<VAR>haJ : aJ ∈ R₁⁰<VAR>hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)<VAR>h : J ≠ 0<GOAL>IsFractional R₁⁰ (I / J)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I J : Submodule R₁ K<VAR>aI : R₁<VAR>haI : aI ∈ R₁⁰<VAR>hI : ∀ b ∈ I, IsInteger R₁ (aI • b)<VAR>aJ : R₁<VAR>haJ : aJ ∈ R₁⁰<VAR>hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)<VAR>h : J ≠ 0<VAR>y : K<VAR>mem_J : y ∈ J<VAR>not_mem_zero : y ∉ 0<GOAL>IsFractional R₁⁰ (I / J)