ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>v : V<VAR>inst✝¹ : Fintype ↑(G.neighborSet v)<VAR>inst✝ : DecidableEq V<GOAL>(G.incidenceFinset v).card = Fintype.card ↑(G.incidenceSet v)
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>K : Type v<VAR>inst✝ : Field K<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>q : k[X]<VAR>hq : Irreducible q<VAR>hdvd : q ∣ map (RingHom.id k) p<GOAL>q.degree = 1
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>K : Type v<VAR>inst✝ : Field K<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>q : k[X]<VAR>hq : Irreducible q<VAR>hdvd : q ∣ p<GOAL>q.degree = 1
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>K : Type v<VAR>inst✝ : Field K<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>q : k[X]<VAR>hq : Irreducible q<VAR>hdvd : q ∣ p<VAR>hlc : IsUnit q.leadingCoeff⁻¹<GOAL>q.degree = 1
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>K : Type v<VAR>inst✝ : Field K<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>q : k[X]<VAR>hq : Irreducible q<VAR>hdvd : q ∣ p<VAR>hlc : IsUnit q.leadingCoeff⁻¹<VAR>hsep' : (q * C q.leadingCoeff⁻¹).Separable<GOAL>q.degree = 1
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>K : Type v<VAR>inst✝ : Field K<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>q : k[X]<VAR>hq : Irreducible q<VAR>hdvd : q ∣ p<VAR>hlc : IsUnit q.leadingCoeff⁻¹<VAR>hsep' : (q * C q.leadingCoeff⁻¹).Separable<VAR>hirr' : Irreducible q<GOAL>q.degree = 1
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>K : Type v<VAR>inst✝ : Field K<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>q : k[X]<VAR>hq : Irreducible q<VAR>hdvd : q ∣ p<VAR>hlc : IsUnit q.leadingCoeff⁻¹<VAR>hsep' : (q * C q.leadingCoeff⁻¹).Separable<VAR>hirr' : Irreducible (q * C q.leadingCoeff⁻¹)<GOAL>q.degree = 1
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>K : Type v<VAR>inst✝ : Field K<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>q : k[X]<VAR>hq : Irreducible q<VAR>hdvd : q ∣ p<VAR>hlc : IsUnit q.leadingCoeff⁻¹<VAR>hsep' : (q * C q.leadingCoeff⁻¹).Separable<VAR>hirr' : Irreducible (q * C q.leadingCoeff⁻¹)<VAR>x : k<VAR>hx : eval x (q * C q.leadingCoeff⁻¹) = 0<GOAL>q.degree = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>R' : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁴ : FunLike F E ℝ<VAR>inst✝³ : AddGroup E<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : NonarchAddGroupSeminorm E<VAR>x y : ℝ<GOAL>r • max x y = max (r • x) (r • y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : Inducing g<GOAL>Inducing (g ∘ f) ↔ Inducing f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : Inducing g<VAR>h : Inducing (g ∘ f)<GOAL>Inducing f
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>‖x - y‖ = ‖x‖ + ‖y‖ ↔ angle x y = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x - y‖ = ‖x‖ + ‖y‖<GOAL>angle x y = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x - y‖ = ‖x‖ + ‖y‖<GOAL>⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x - y‖ = ‖x‖ + ‖y‖<VAR>hxy₁ : 0 ≤ ‖x - y‖<VAR>hxy₂ : 0 ≤ ‖x‖ + ‖y‖<GOAL>⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2<VAR>hxy₁ : 0 ≤ ‖x - y‖<VAR>hxy₂ : 0 ≤ ‖x‖ + ‖y‖<GOAL>⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : α → 𝕜<VAR>g : α → R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : (f ^ n) =O[l] (g ^ n)<GOAL>f =O[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : α → 𝕜<VAR>g : α → R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : (f ^ n) =O[l] (g ^ n)<VAR>C : ℝ<VAR>_hC₀ : C > 0<VAR>hC : IsBigOWith C l (f ^ n) (g ^ n)<GOAL>f =O[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : α → 𝕜<VAR>g : α → R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : (f ^ n) =O[l] (g ^ n)<VAR>C : ℝ<VAR>_hC₀ : C > 0<VAR>hC : IsBigOWith C l (f ^ n) (g ^ n)<VAR>c : ℝ<VAR>hc₀ : 0 ≤ c<VAR>hc : C ≤ c ^ n<GOAL>f =O[l] g
<VAR>a b r : ℤ<VAR>hr : 0 < r<VAR>v x : ℤ<GOAL>x ∈ filter (fun x => x ≡ v [ZMOD r]) (Ico a b) ↔ x ∈ map { toFun := fun x => x + v, inj' := ⋯ } (filter (fun x => r ∣ x) (Ico (a - v) (b - v)))
<VAR>z w : ℝ<GOAL>z = w → ↑z = ↑w
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<GOAL>UpperSemicontinuousWithinAt f univ x ↔ UpperSemicontinuousAt f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : TopologicalSpace α<VAR>f✝ : α → G<VAR>s : Set α<VAR>x✝¹ : α<VAR>H : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ContinuousMul M<VAR>inst✝² : Group H<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : TopologicalGroup H<VAR>f : G →* H →* M<VAR>hl : ∀ (x : G), Tendsto (⇑(f x)) (𝓝 1) (𝓝 ((f x) 1))<VAR>hr : ∀ (y : H), Tendsto (fun x => (f x) y) (𝓝 1) (𝓝 ((f 1) y))<VAR>x✝ : G × H<VAR>x : G<VAR>y : H<VAR>hf : Tendsto (fun x => (f x.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))<GOAL>Tendsto (fun x_1 => (f x) y * (f x_1.1) y * ((f x) x_1.2 * (f x_1.1) x_1.2)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f x) y))
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : TopologicalSpace α<VAR>f✝ : α → G<VAR>s : Set α<VAR>x✝¹ : α<VAR>H : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ContinuousMul M<VAR>inst✝² : Group H<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : TopologicalGroup H<VAR>f : G →* H →* M<VAR>hl : ∀ (x : G), Tendsto (⇑(f x)) (𝓝 1) (𝓝 ((f x) 1))<VAR>hr : ∀ (y : H), Tendsto (fun x => (f x) y) (𝓝 1) (𝓝 ((f 1) y))<VAR>x✝ : G × H<VAR>x : G<VAR>y : H<VAR>hf : Tendsto (fun x => (f x.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))<GOAL>𝓝 ((f x) y * (f 1) y * ((f x) 1 * (f 1) 1)) = 𝓝 ((f x) y)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>↑(implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) a = (f a, 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : 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 F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<GOAL>AEStronglyMeasurable' m (↑↑((condexpL1CLM F' hm μ) f)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : 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 F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<GOAL>∀ (c : F') {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), (fun f => AEStronglyMeasurable' m (↑↑((condexpL1CLM F' hm μ) f)) μ) ↑(simpleFunc.indicatorConst 1 hs ⋯ c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : 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 F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<GOAL>∀ ⦃f g : α → F'⦄ (hf : Memℒp f 1 μ) (hg : Memℒp g 1 μ), Disjoint (Function.support f) (Function.support g) → (fun f => AEStronglyMeasurable' m (↑↑((condexpL1CLM F' hm μ) f)) μ) (Memℒp.toLp f hf) → (fun f => AEStronglyMeasurable' m (↑↑((condexpL1CLM F' hm μ) f)) μ) (Memℒp.toLp g hg) → (fun f => AEStronglyMeasurable' m (↑↑((condexpL1CLM F' hm μ) f)) μ) (Memℒp.toLp f hf + Memℒp.toLp g hg)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : 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 F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<GOAL>IsClosed {f | (fun f => AEStronglyMeasurable' m (↑↑((condexpL1CLM F' hm μ) f)) μ) f}
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l : Line α✝ ι✝<VAR>i : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>inst✝ : Nonempty ι<VAR>x : α<GOAL>(fun x i => ((diagonal α ι).idxFun i).getD x) x = fun x_1 => x
<VAR>α : Type u_1<VAR>s t✝ t : Finset α<VAR>val✝ : Multiset α<VAR>nodup✝ : val✝.Nodup<GOAL>{ val := val✝, nodup := nodup✝ } ∈ t.powerset ↔ { val := val✝, nodup := nodup✝ } ⊆ t
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hp1 : p.degree = 1<VAR>hm : p.Monic<GOAL>p = X - C (-p.coeff 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<GOAL>¬ν ≤ μ ↔ ∃ s, MeasurableSet s ∧ μ s < ν s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>inst✝ : CompleteLattice β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>f (sSup s) = ⨆ a ∈ s, f a
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>h : IsGLB s a<GOAL>⋃ x ∈ s, Ioi x = Ioi a
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>h : IsGLB s a<VAR>x : α<VAR>hx : x ∈ s<GOAL>Ioi x ⊆ Ioi a
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>h : IsGLB s a<VAR>x : α<VAR>hx : x ∈ Ioi a<GOAL>x ∈ ⋃ i ∈ s, Ioi i
<VAR>x : PartENat<VAR>hx : x ≠ ⊤<GOAL>x < x + 1
<VAR>x : PartENat<VAR>hx : x ≠ ⊤<GOAL>0 < 1
<VAR>n m : ℕ<GOAL>n ^^^ (n ^^^ m) = m
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>u : ℕ → α<GOAL>CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I a₀ b₀ : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume<VAR>ha : Tendsto a l (𝓝 a₀)<VAR>hb : Tendsto b l (𝓝 b₀)<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<GOAL>IntegrableOn f (Ioc a₀ b₀) volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I a₀ b₀ : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume<VAR>ha : Tendsto a l (𝓝 a₀)<VAR>hb : Tendsto b l (𝓝 b₀)<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<VAR>i : ι<VAR>hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<GOAL>∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂volume.restrict (Ioc a₀ b₀) ≤ I
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I a₀ b₀ : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume<VAR>ha : Tendsto a l (𝓝 a₀)<VAR>hb : Tendsto b l (𝓝 b₀)<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<VAR>i : ι<VAR>hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<GOAL>∫ (x : ℝ) in Ioc (a i) (b i) ∩ Ioc a₀ b₀, ‖f x‖ ∂volume ≤ I
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I a₀ b₀ : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume<VAR>ha : Tendsto a l (𝓝 a₀)<VAR>hb : Tendsto b l (𝓝 b₀)<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<VAR>i : ι<VAR>hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<GOAL>∀ (a : ℝ), 0 a ≤ (fun x => ‖f x‖) a
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I a₀ b₀ : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume<VAR>ha : Tendsto a l (𝓝 a₀)<VAR>hb : Tendsto b l (𝓝 b₀)<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<VAR>i : ι<VAR>hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I<GOAL>∀ (a_1 : ℝ), (Ioc (a i) (b i) ∩ Ioc a₀ b₀) a_1 ≤ Ioc (a i) (b i) a_1
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x y : α<VAR>inst✝¹ : LE α<VAR>inst✝ : LECmp cmp<GOAL>cmp x y ≠ Ordering.lt ↔ y ≤ x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<GOAL>¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<VAR>h_ne_zero : v.maxPowDividing I ≠ 0<GOAL>¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<VAR>h_ne_zero : v.maxPowDividing I ≠ 0<GOAL>¬v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣ v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<VAR>h_ne_zero : v.maxPowDividing I ≠ 0<VAR>h_contr : v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣ v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<VAR>h_ne_zero : v.maxPowDividing I ≠ 0<VAR>h_contr : v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣ v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I<VAR>hv_prime : Prime v.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<VAR>h_ne_zero : v.maxPowDividing I ≠ 0<VAR>h_contr : v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣ v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I<VAR>hv_prime : Prime v.asIdeal<VAR>w : HeightOneSpectrum R<VAR>hw : w ∈ hf.toFinset.erase v<VAR>hvw' : v.asIdeal ∣ w.maxPowDividing I<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<VAR>h_ne_zero : v.maxPowDividing I ≠ 0<VAR>h_contr : v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣ v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I<VAR>hv_prime : Prime v.asIdeal<VAR>w : HeightOneSpectrum R<VAR>hw : w ∈ hf.toFinset.erase v<VAR>hvw' : v.asIdeal ∣ w.maxPowDividing I<VAR>hw_prime : Prime w.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<VAR>h_ne_zero : v.maxPowDividing I ≠ 0<VAR>h_contr : v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣ v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I<VAR>hv_prime : Prime v.asIdeal<VAR>w : HeightOneSpectrum R<VAR>hw : w ∈ hf.toFinset.erase v<VAR>hvw' : v.asIdeal ∣ w.maxPowDividing I<VAR>hw_prime : Prime w.asIdeal<VAR>hvw : v.asIdeal ∣ w.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>hf : (mulSupport fun v => v.maxPowDividing I).Finite<VAR>h_ne_zero : v.maxPowDividing I ≠ 0<VAR>h_contr : v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣ v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I<VAR>hv_prime : Prime v.asIdeal<VAR>w : HeightOneSpectrum R<VAR>hw : w ∈ hf.toFinset.erase v<VAR>hvw' : v.asIdeal ∣ w.maxPowDividing I<VAR>hw_prime : Prime w.asIdeal<VAR>hvw : v.asIdeal = w.asIdeal<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x✝ y : G<VAR>i : ℤ<VAR>x : G<VAR>z : ℤ<GOAL>x ^ (z % ↑(orderOf x)) = x ^ (z % ↑(orderOf x) + ↑(orderOf x) * (z / ↑(orderOf x)))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x✝ y : G<VAR>i : ℤ<VAR>x : G<VAR>z : ℤ<GOAL>x ^ (z % ↑(orderOf x) + ↑(orderOf x) * (z / ↑(orderOf x))) = x ^ z
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>x✝ : ℂ<GOAL>logDeriv cexp x✝ = 1 x✝
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Add α<VAR>a b c d : WithTop α<VAR>x y : α<GOAL>a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤