ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V'<VAR>inst✝ : Module K V'<VAR>f g : V →ₗ[K] V'<GOAL>range (f + g) ≤ range f ⊔ range g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<GOAL>IsClosed (B.polar s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<GOAL>IsClosed (⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>x : E<VAR>x✝ : x ∈ s<GOAL>IsClosed {y | ‖(B x) y‖ ≤ 1}
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>c : 𝕜<GOAL>HasGradientAtFilter (fun x => c) 0 x L
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>c : 𝕜<GOAL>HasFDerivAtFilter (fun x => c) 0 x L
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>f : E → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>Integrable (fun x => (pdf X ℙ μ x).toReal • f x) μ ↔ Integrable (fun x => f (X x)) ℙ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>f : E → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>Integrable f (map X ℙ) ↔ Integrable f (μ.withDensity ((map X ℙ).rnDeriv μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>I X : Set α<VAR>hIX : M.Basis I X<GOAL>(M.map f hf).Basis (f '' I) (f '' X)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ : Multiset α<VAR>a✝ b : α<VAR>s t : Multiset α<VAR>a : α<GOAL>s + {a} = t ↔ a ∈ t ∧ s = t.erase a
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ : Multiset α<VAR>a✝ b : α<VAR>s t : Multiset α<VAR>a : α<GOAL>a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b✝ : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>b : AffineBasis ι k V<VAR>v : V<GOAL>∑ i : ι, (b.coord i) v • b i = v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b✝ : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>b : AffineBasis ι k V<VAR>v : V<VAR>hb : ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) v) = v<GOAL>∑ i : ι, (b.coord i) v • b i = v
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : NormOneClass A<VAR>a : A<GOAL>spectralRadius 𝕜 a ≤ ↑‖a‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : NormOneClass A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ σ a<GOAL>↑‖k‖₊ ≤ ↑‖a‖₊
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : MulZeroClass α<VAR>a✝ b✝ : WithTop α<VAR>inst✝ : LT α<VAR>a b : WithTop α<VAR>ha : a < ⊤<VAR>hb : b < ⊤<GOAL>a * b < ⊤
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : MulZeroClass α<VAR>a✝ b✝ : WithTop α<VAR>inst✝ : LT α<VAR>a b : WithTop α<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>a * b ≠ ⊤
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>c : R<GOAL>c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>j✝ : J<GOAL>((rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y).hom ≫ biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝ = (α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ (f j) X Y).symm).hom ≫ biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>j✝ : J<GOAL>∑ x : J, (biproduct.π f x ▷ X ⊗ 𝟙 Y) ≫ (biproduct.ι (fun j => f j ⊗ X) x ⊗ 𝟙 Y) ≫ biproduct.π (fun j => f j ⊗ X) j✝ ▷ Y = (α_ (⨁ f) X Y).hom ≫ biproduct.π f j✝ ▷ (X ⊗ Y) ≫ (α_ (f j✝) X Y).inv
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>j✝ : J<GOAL>∑ x : J, ((biproduct.π f x ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ (biproduct.ι (fun j => f j ⊗ X) x ⊗ 𝟙 Y) ≫ (biproduct.π (fun j => f j ⊗ X) j✝ ⊗ 𝟙 Y) = (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>j✝ : J<GOAL>(∑ x : J, if h : x = j✝ then (biproduct.π f x ⊗ 𝟙 X) ≫ eqToHom ⋯ ⊗ 𝟙 Y else (biproduct.π f x ⊗ 𝟙 X) ≫ 0 ⊗ 𝟙 Y) = (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → F) → Prop<VAR>h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → F⦄, Disjoint (Function.support f) (Function.support g) → Memℒp f p μ → Memℒp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑↑f}<VAR>h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>f : α → F<VAR>hf : Memℒp f p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>f_Lp : ↥(Lp F p μ) := toLp f hf<GOAL>P f
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → F) → Prop<VAR>h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → F⦄, Disjoint (Function.support f) (Function.support g) → Memℒp f p μ → Memℒp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑↑f}<VAR>h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>f : α → F<VAR>hf : Memℒp f p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>f_Lp : ↥(Lp F p μ) := toLp f hf<VAR>hfm_Lp : AEStronglyMeasurable' m (↑↑f_Lp) μ<GOAL>P f
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → F) → Prop<VAR>h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → F⦄, Disjoint (Function.support f) (Function.support g) → Memℒp f p μ → Memℒp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑↑f}<VAR>h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>f : α → F<VAR>hf : Memℒp f p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>f_Lp : ↥(Lp F p μ) := toLp f hf<VAR>hfm_Lp : AEStronglyMeasurable' m (↑↑f_Lp) μ<GOAL>P ↑↑(toLp f hf)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → F) → Prop<VAR>h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → F⦄, Disjoint (Function.support f) (Function.support g) → Memℒp f p μ → Memℒp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑↑f}<VAR>h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>f : α → F<VAR>hf : Memℒp f p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>f_Lp : ↥(Lp F p μ) := toLp f hf<VAR>hfm_Lp : AEStronglyMeasurable' m (↑↑f_Lp) μ<GOAL>P ↑↑f_Lp
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → F) → Prop<VAR>h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → F⦄, Disjoint (Function.support f) (Function.support g) → Memℒp f p μ → Memℒp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑↑f}<VAR>h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>f : α → F<VAR>hf : Memℒp f p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>f_Lp : ↥(Lp F p μ) := toLp f hf<VAR>hfm_Lp : AEStronglyMeasurable' m (↑↑f_Lp) μ<GOAL>∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), (fun f => P ↑↑f) ↑(Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → F) → Prop<VAR>h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → F⦄, Disjoint (Function.support f) (Function.support g) → Memℒp f p μ → Memℒp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑↑f}<VAR>h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>f : α → F<VAR>hf : Memℒp f p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>f_Lp : ↥(Lp F p μ) := toLp f hf<VAR>hfm_Lp : AEStronglyMeasurable' m (↑↑f_Lp) μ<GOAL>∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → (fun f => P ↑↑f) (toLp f hf) → (fun f => P ↑↑f) (toLp g hg) → (fun f => P ↑↑f) (toLp f hf + toLp g hg)
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>count p n < count p (n + 1) ↔ p n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x y : α<VAR>h4 : x ≠ y<VAR>h5 : τ = swap x y<GOAL>closure {σ, τ} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x y : α<VAR>h4 : x ≠ y<VAR>h5 : τ = swap x y<VAR>i : ℕ<VAR>hi : (σ ^ i) x = y<GOAL>closure {σ, τ} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x y : α<VAR>h4 : x ≠ y<VAR>h5 : τ = swap x y<VAR>i : ℕ<VAR>hi : (σ ^ i) x = y<GOAL>closure {σ, swap x ((σ ^ i) x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x y : α<VAR>h4 : x ≠ y<VAR>h5 : τ = swap x y<VAR>i : ℕ<VAR>hi : (σ ^ i) x = y<VAR>h : Fintype.card α ∣ i<GOAL>x = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x y : α<VAR>h4 : x ≠ y<VAR>h5 : τ = swap x y<VAR>i : ℕ<VAR>hi : (σ ^ i) x = y<VAR>m : ℕ<VAR>hm : i = Fintype.card α * m<GOAL>x = y
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>n n' : ℤ<VAR>hf : (a ^ n).x = (-a ^ n').x<GOAL>False
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>n n' : ℤ<VAR>hf : (a ^ n).x = (-a ^ n').x<VAR>H : 0 < (a ^ n).x<GOAL>False
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>n n' : ℤ<VAR>hf : (a ^ n).x = (-a ^ n').x<VAR>H : (a ^ n').x < 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>x : β<VAR>f✝ : α → β<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → β<GOAL>sInf {a | ∀ᶠ (n : β) in map f (ae μ), n ≤ a} = sInf {a | μ {x | a < f x} = 0}
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Iio a = Ioi (a / c)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f volume a b<VAR>c : ℝ<VAR>hc : c = 0<GOAL>IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f volume a b<VAR>c : ℝ<VAR>hc : c ≠ 0<GOAL>IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntegrableOn f [[a, b]] volume<VAR>c : ℝ<VAR>hc : c ≠ 0<GOAL>IntegrableOn (fun x => f (c * x)) [[a / c, b / c]] volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A✝<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntegrableOn f [[a, b]] volume<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>A : MeasurableEmbedding fun x => x * c⁻¹<GOAL>IntegrableOn (fun x => f (c * x)) [[a / c, b / c]] volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A✝<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntegrableOn f [[a, b]] volume<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>A : MeasurableEmbedding fun x => x * c⁻¹<GOAL>IntegrableOn ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) ((fun x => x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume
<VAR>P : Type u_1<VAR>inst✝¹ : SemilatticeSup P<VAR>inst✝ : OrderBot P<VAR>x : P<VAR>I J K : Ideal P<VAR>S : Set (Ideal P)<GOAL>x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
<VAR>x : ℝ*<GOAL>|x|.Infinite ↔ x.Infinite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : ℝ<VAR>f : ℕ → ℝ≥0<GOAL>HasSum (fun i => ↑(f i)) r ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, (fun i => ↑(f i)) i) atTop (𝓝 r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : ℝ<VAR>f : ℕ → ℝ≥0<GOAL>(∃ (hx : 0 ≤ r), Tendsto (fun a => ∑ a ∈ a, f a) atTop (𝓝 ⟨r, hx⟩)) ↔ ∃ (hx : 0 ≤ r), Tendsto (fun a => ∑ a ∈ Finset.range a, f a) atTop (𝓝 ⟨r, hx⟩)
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>↑(toCircle (n • ↑x)) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x y : 𝓞 K<VAR>hy : x - 1 = λ * y<GOAL>λ ^ 4 ∣ x ^ 3 - 1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x y : 𝓞 K<VAR>hy : x - 1 = λ * y<VAR>this : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))<GOAL>λ ^ 4 ∣ x ^ 3 - 1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x y : 𝓞 K<VAR>hy : x - 1 = λ * y<VAR>this : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))<GOAL>λ ^ 3 * λ ∣ λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>t : Finset β<VAR>i : (a : α) → a ∈ s → β<VAR>j : (a : β) → a ∈ t → α<VAR>hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t<VAR>hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s<VAR>left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a<VAR>right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>t : Finset β<VAR>i : (a : α) → a ∈ s → β<VAR>j : (a : β) → a ∈ t → α<VAR>hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t<VAR>hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s<VAR>left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a<VAR>right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a<VAR>a1 : α<VAR>h1 : a1 ∈ s<VAR>a2 : α<VAR>h2 : a2 ∈ s<VAR>eq : i a1 h1 = i a2 h2<GOAL>a1 = a2
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F₁ F₂ F₃ : J ⥤ C<VAR>j : J<GOAL>(α_ F₁ F₂ F₃).hom.app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F₁ F₂ F₃ : J ⥤ C<VAR>j : J<GOAL>(α_ F₁ F₂ F₃).hom.app j ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j) = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F₁ F₂ F₃ : J ⥤ C<VAR>j : J<GOAL>(α_ F₁ F₂ F₃).hom.app j ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j) = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>eval₂ f (z * f p.leadingCoeff) p.integralNormalization = ∑ i ∈ p.support.attach, f (p.integralNormalization.coeff ↑i * p.leadingCoeff ^ ↑i) * z ^ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>∑ n ∈ p.support, f (p.integralNormalization.coeff n) * (z * f p.leadingCoeff) ^ n = ∑ i ∈ p.support.attach, f (p.integralNormalization.coeff ↑i * p.leadingCoeff ^ ↑i) * z ^ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>∑ x ∈ p.support, f (p.integralNormalization.coeff x) * (f p.leadingCoeff ^ x * z ^ x) = ∑ x ∈ p.support.attach, f (p.integralNormalization.coeff ↑x) * (f p.leadingCoeff ^ ↑x * z ^ ↑x)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<VAR>hp : ¬p = 0<GOAL>∑ i ∈ p.support.attach, f (p.integralNormalization.coeff ↑i * p.leadingCoeff ^ ↑i) * z ^ ↑i = ∑ i ∈ p.support.attach, f (p.coeff ↑i * p.leadingCoeff ^ (p.natDegree - 1)) * z ^ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<VAR>hp : ¬p = 0<VAR>one_le_deg : 1 ≤ p.natDegree<GOAL>∑ i ∈ p.support.attach, f (p.integralNormalization.coeff ↑i * p.leadingCoeff ^ ↑i) * z ^ ↑i = ∑ i ∈ p.support.attach, f (p.coeff ↑i * p.leadingCoeff ^ (p.natDegree - 1)) * z ^ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>∑ i ∈ p.support.attach, f (p.coeff ↑i * p.leadingCoeff ^ (p.natDegree - 1)) * z ^ ↑i = f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f z p