ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p n : ℕ<VAR>hp : p ≠ 0<VAR>e : ℕ<VAR>hn : n ∈ p.smoothNumbers<VAR>this : NoZeroDivisors ℕ<VAR>hp' : p ^ e ≠ 0<VAR>q : ℕ<VAR>hq : q ∈ (p ^ e * n).primeFactorsList<VAR>H : q ∈ (p ^ e).primeFactorsList<GOAL>q < p.succ
<VAR>p n : ℕ<VAR>hp : p ≠ 0<VAR>e : ℕ<VAR>hn : n ∈ p.smoothNumbers<VAR>this : NoZeroDivisors ℕ<VAR>hp' : p ^ e ≠ 0<VAR>q : ℕ<VAR>hq : q ∈ (p ^ e * n).primeFactorsList<VAR>H : q ∈ n.primeFactorsList<GOAL>q < p.succ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a ≤ b<GOAL>insert b (Ico a b) = Icc a b
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝² : CommRing S✝<VAR>inst✝¹ : Algebra R S✝<VAR>inst✝ : IsLocalization M S✝<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>I : Ideal R<GOAL>I = ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝² : CommRing S✝<VAR>inst✝¹ : Algebra R S✝<VAR>inst✝ : IsLocalization M S✝<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>I : Ideal R<GOAL>I ≤ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝² : CommRing S✝<VAR>inst✝¹ : Algebra R S✝<VAR>inst✝ : IsLocalization M S✝<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>I : Ideal R<GOAL>⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I
<VAR>a : UnitAddCircle<GOAL>{ f := ofReal' ∘ evenKernel (-a), g := ofReal' ∘ cosKernel (-a), k := 1 / 2, ε := 1, f₀ := if -a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ } = { f := ofReal' ∘ evenKernel a, g := ofReal' ∘ cosKernel a, k := 1 / 2, ε := 1, f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i → ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯<GOAL>x ∈ ⨆ i, S i → ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯<GOAL>⨆ i, S i ≤ U
<VAR>x y : ℝ<GOAL>arsinh x ≤ 0 ↔ x ≤ 0
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'<GOAL>l.balanceL x r = l.balance' x r
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'<GOAL>l.size = 0 → r.size ≤ 1
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'<GOAL>1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type w<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Small.{v, u} R<GOAL>Flat R M ↔ ∀ ⦃N N' N'' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type w<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Small.{v, u} R<VAR>H : ∀ ⦃N N' N'' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)<VAR>N' N'' : Type v<VAR>x✝³ : AddCommGroup N'<VAR>x✝² : AddCommGroup N''<VAR>x✝¹ : Module R N'<VAR>x✝ : Module R N''<VAR>L : N' →ₗ[R] N''<VAR>hL : Function.Injective ⇑L<VAR>x : N' ⊗[R] M<VAR>hx : (rTensor M L) x = 0<GOAL>x ∈ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>preNormEDS b c d 3 = c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<VAR>hg_eq : g =ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) f)<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<VAR>hg_eq : g =ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condexpL2 ℝ ℝ hm) f)<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<VAR>hg_eq : g =ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊<GOAL>∫⁻ (x : α) in s, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<VAR>hg_eq : g =ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊<GOAL>∫⁻ (a : α) in s, ↑‖g a‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<VAR>hg_eq : g =ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊<GOAL>IntegrableOn (↑↑f) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<VAR>hg_eq : g =ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊<GOAL>StronglyMeasurable g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<VAR>hg_eq : g =ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊<GOAL>IntegrableOn g s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp ℝ 2 μ)<VAR>h_meas : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) f)) μ := lpMeas.aeStronglyMeasurable' ((condexpL2 ℝ ℝ hm) f)<VAR>g : α → ℝ := Exists.choose h_meas<VAR>hg_meas : StronglyMeasurable g<VAR>hg_eq : g =ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_eq_restrict : g =ᶠ[ae (μ.restrict s)] ↑↑↑((condexpL2 ℝ ℝ hm) f)<VAR>hg_nnnorm_eq : (fun x => ↑‖g x‖₊) =ᶠ[ae (μ.restrict s)] fun x => ↑‖↑↑↑((condexpL2 ℝ ℝ hm) f) x‖₊<GOAL>∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, ↑↑f x ∂μ
<VAR>ι : Type u_1<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ✝ : Type w<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>K : ℝ≥0<VAR>h : Isometry g<GOAL>LipschitzWith K (g ∘ f) ↔ LipschitzWith K f
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : CommRing Rₘ<VAR>inst✝¹ : Algebra R Rₘ<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : DimensionLEOne R<VAR>p : Ideal Rₘ<VAR>hp0 : p ≠ ⊥<VAR>hpp : p.IsPrime<GOAL>p.IsMaximal
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : CommRing Rₘ<VAR>inst✝¹ : Algebra R Rₘ<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : DimensionLEOne R<VAR>p : Ideal Rₘ<VAR>hp0 : p ≠ ⊥<VAR>hpp : p.IsPrime<VAR>P : Ideal Rₘ<VAR>hpP : p < P<VAR>hPm : P.IsMaximal<GOAL>False
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : CommRing Rₘ<VAR>inst✝¹ : Algebra R Rₘ<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : DimensionLEOne R<VAR>p : Ideal Rₘ<VAR>hp0 : p ≠ ⊥<VAR>hpp : p.IsPrime<VAR>P : Ideal Rₘ<VAR>hpP : p < P<VAR>hPm : P.IsMaximal<VAR>hpP' : ⟨p, hpp⟩ < ⟨P, ⋯⟩<GOAL>False
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : CommRing Rₘ<VAR>inst✝¹ : Algebra R Rₘ<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : DimensionLEOne R<VAR>p : Ideal Rₘ<VAR>hp0 : p ≠ ⊥<VAR>hpp : p.IsPrime<VAR>P : Ideal Rₘ<VAR>hpP : p < P<VAR>hPm : P.IsMaximal<VAR>hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩<GOAL>False
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : CommRing Rₘ<VAR>inst✝¹ : Algebra R Rₘ<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : DimensionLEOne R<VAR>p : Ideal Rₘ<VAR>hp0 : p ≠ ⊥<VAR>hpp : p.IsPrime<VAR>P : Ideal Rₘ<VAR>hpP : p < P<VAR>hPm : P.IsMaximal<VAR>hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩<VAR>this : (Ideal.comap (algebraMap R Rₘ) p).IsPrime<GOAL>False
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : CommRing Rₘ<VAR>inst✝¹ : Algebra R Rₘ<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : DimensionLEOne R<VAR>p : Ideal Rₘ<VAR>hp0 : p ≠ ⊥<VAR>hpp : p.IsPrime<VAR>P : Ideal Rₘ<VAR>hpP : p < P<VAR>hPm : P.IsMaximal<VAR>hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩<VAR>this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime<VAR>this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime<GOAL>False
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : CommRing Rₘ<VAR>inst✝¹ : Algebra R Rₘ<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : DimensionLEOne R<VAR>p : Ideal Rₘ<VAR>hp0 : p ≠ ⊥<VAR>hpp : p.IsPrime<VAR>P : Ideal Rₘ<VAR>hpP : p < P<VAR>hPm : P.IsMaximal<VAR>hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩<VAR>this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime<VAR>this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime<VAR>hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P<GOAL>False
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : CommRing Rₘ<VAR>inst✝¹ : Algebra R Rₘ<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : DimensionLEOne R<VAR>p : Ideal Rₘ<VAR>hp0 : p ≠ ⊥<VAR>hpp : p.IsPrime<VAR>P : Ideal Rₘ<VAR>hpP : p < P<VAR>hPm : P.IsMaximal<VAR>hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩<VAR>this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime<VAR>this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime<VAR>hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P<GOAL>⊥ < Ideal.comap (algebraMap R Rₘ) p
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : TotalComplexShape c₁ c₂ c₁₂<VAR>I : Type u_4<VAR>inst✝¹ : AddMonoid I<VAR>c : ComplexShape I<VAR>inst✝ : c.TensorSigns<VAR>p q : I<GOAL>c.ε (p + q) = c.ε p * c.ε q