ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : Nonempty ι<VAR>m : ι → A<GOAL>‖∏ i : ι, m i‖ ≤ ∏ i : ι, ‖m i‖
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>a✝ b a : α<VAR>hb : b ∈ s<GOAL>↑(a * b) = ↑a
<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>f₀ f₁ : F → 𝕜<VAR>f₀' f₁' x₀ x₁ : F<VAR>s₀ s₁ t : Set F<VAR>L₀ L₁ : Filter F<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>(toDual 𝕜 F).symm (fderiv 𝕜 f₁ x) = (toDual 𝕜 F).symm (fderiv 𝕜 f x)
<VAR>i : Nat<VAR>α✝ : Type u_1<VAR>xs : List α✝<VAR>j : Nat<VAR>h₀ : i < xs.length<VAR>h₁ : xs.Nodup<VAR>h₂ : xs[i]? = xs[j]?<GOAL>i = j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X][Y]<VAR>q : R[X]<GOAL>eval (map f q) (map (mapRingHom f) p) = map f (eval q p)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>R : Presieve X<GOAL>Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y✝ Z : C<VAR>f : Y✝ ⟶ X<VAR>S R✝ : Sieve X<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>R : Presieve X<VAR>Y : D<GOAL>Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → PMF β<VAR>g : β → PMF γ<VAR>x y : α<VAR>hy : y ≠ x<GOAL>p y * (pure y) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → PMF β<VAR>g : β → PMF γ<VAR>x : α<GOAL>p x * (pure x) x = p x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → Set X<VAR>ho : ∀ (i : α), IsOpen (f i)<VAR>hU : ⋃ i, f i = univ<GOAL>IsOpen s ↔ ∀ (i : α), IsOpen (f i ∩ s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → Set X<VAR>ho : ∀ (i : α), IsOpen (f i)<VAR>hU : ⋃ i, f i = univ<VAR>h : ∀ (i : α), IsOpen (f i ∩ s)<GOAL>IsOpen s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : α → Set X<VAR>ho : ∀ (i : α), IsOpen (f i)<VAR>hU : ⋃ i, f i = univ<VAR>h : ∀ (i : α), IsOpen (f i ∩ s)<GOAL>IsOpen (⋃ i, f i ∩ s)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁<VAR>β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁<VAR>γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂<VAR>δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂<VAR>a : A<GOAL>({ app := fun X_1 => ({ app := fun X_2 => L₆.map (γ.app X_2), naturality := ⋯ } ≫ { app := fun X => δ.app (L₃.obj X), naturality := ⋯ }).app (G₁.obj X_1), naturality := ⋯ } ≫ { app := fun X => K₂.map (({ app := fun X => L₄.map (α.app X), naturality := ⋯ } ≫ { app := fun X => β.app (L₁.obj X), naturality := ⋯ }).app X), naturality := ⋯ }).app a = ({ app := fun X_1 => L₆.map (({ app := fun X_2 => γ.app (G₁.obj X_2), naturality := ⋯ } ≫ { app := fun X => H₂.map (α.app X), naturality := ⋯ }).app X_1), naturality := ⋯ } ≫ { app := fun X => ({ app := fun X => δ.app (H₁.obj X), naturality := ⋯ } ≫ { app := fun X => K₂.map (β.app X), naturality := ⋯ }).app (L₁.obj X), naturality := ⋯ }).app a
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁<VAR>β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁<VAR>γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂<VAR>δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂<VAR>a : A<GOAL>L₆.map (γ.app (G₁.obj a)) ≫ δ.app (L₃.obj (G₁.obj a)) ≫ K₂.map (L₄.map (α.app a)) ≫ K₂.map (β.app (L₁.obj a)) = L₆.map (γ.app (G₁.obj a)) ≫ L₆.map (H₂.map (α.app a)) ≫ δ.app (H₁.obj (L₁.obj a)) ≫ K₂.map (β.app (L₁.obj a))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁<VAR>β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁<VAR>γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂<VAR>δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂<VAR>a : A<GOAL>L₆.map (γ.app (G₁.obj a)) ≫ δ.app (L₃.obj (G₁.obj a)) ≫ K₂.map (L₄.map (α.app a)) ≫ K₂.map (β.app (L₁.obj a)) = L₆.map (γ.app (G₁.obj a)) ≫ (δ.app (L₃.obj (G₁.obj a)) ≫ (L₄ ⋙ K₂).map (α.app a)) ≫ K₂.map (β.app (L₁.obj a))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p₁ : ι → P<VAR>p₂ : P<VAR>h : ∑ i ∈ s, w i = 1<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (affineCombination k s p₁) w -ᵥ p₂
<VAR>n : ℕ<GOAL>n ! * (n + 1).ascFactorial 0 = (n + 0)!
<VAR>n k : ℕ<GOAL>n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!
<VAR>α β : Type u<VAR>f : Cardinal.{u} → Cardinal.{max u v}<VAR>s : Set Cardinal.{u}<VAR>hs : BddAbove s<GOAL>BddAbove (f '' s)
<VAR>α β : Type u<VAR>f : Cardinal.{u} → Cardinal.{max u v}<VAR>s : Set Cardinal.{u}<VAR>hs : Small.{u, u + 1} ↑s<GOAL>Small.{max u v, (max u v) + 1} ↑(f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y✝ : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n<VAR>hg0 : Summable fun n => g n y₀<VAR>y : 𝕜<GOAL>Summable fun n => g n y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>K : Type u_6<VAR>inst✝ : RCLike K<VAR>f : α → K<GOAL>Memℒp (fun x => RCLike.re (f x)) p μ ∧ Memℒp (fun x => RCLike.im (f x)) p μ ↔ Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>K : Type u_6<VAR>inst✝ : RCLike K<VAR>f : α → K<GOAL>Memℒp (fun x => RCLike.re (f x)) p μ ∧ Memℒp (fun x => RCLike.im (f x)) p μ → Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>K : Type u_6<VAR>inst✝ : RCLike K<VAR>f : α → K<VAR>hre : Memℒp (fun x => RCLike.re (f x)) p μ<VAR>him : Memℒp (fun x => RCLike.im (f x)) p μ<GOAL>Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>K : Type u_6<VAR>inst✝ : RCLike K<VAR>f : α → K<VAR>hre : Memℒp (fun x => RCLike.re (f x)) p μ<VAR>him : Memℒp (fun x => RCLike.im (f x)) p μ<GOAL>f = (fun x => ↑(RCLike.re (f x))) + fun x => RCLike.I * ↑(RCLike.im (f x))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>K : Type u_6<VAR>inst✝ : RCLike K<VAR>f : α → K<VAR>hre : Memℒp (fun x => RCLike.re (f x)) p μ<VAR>him : Memℒp (fun x => RCLike.im (f x)) p μ<VAR>x : α<GOAL>f x = ((fun x => ↑(RCLike.re (f x))) + fun x => RCLike.I * ↑(RCLike.im (f x))) x
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>p : α → (i : ι) → i ∈ S → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : ContinuousOn f F<VAR>x : X<VAR>x_in : x ∈ F<VAR>hx : ∀ {y : X}, y ∈ F → JoinedIn F x y<GOAL>IsPathConnected (f '' F)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : ContinuousOn f F<VAR>x : X<VAR>x_in : x ∈ F<VAR>hx : ∀ {y : X}, y ∈ F → JoinedIn F x y<GOAL>∀ {y : Y}, y ∈ f '' F → JoinedIn (f '' F) (f x) y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : ContinuousOn f F<VAR>x : X<VAR>x_in : x ∈ F<VAR>hx : ∀ {y : X}, y ∈ F → JoinedIn F x y<VAR>y : X<VAR>y_in : y ∈ F<GOAL>JoinedIn (f '' F) (f x) (f y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : ContinuousOn f F<VAR>x : X<VAR>x_in : x ∈ F<VAR>hx : ∀ {y : X}, y ∈ F → JoinedIn F x y<VAR>y : X<VAR>y_in : y ∈ F<GOAL>ContinuousOn f (range ⇑⋯.somePath)
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>eLpNorm f_lim p μ ≤ liminf (fun n => eLpNorm (f n) p μ) atTop
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>eLpNorm f_lim 0 μ ≤ liminf (fun n => eLpNorm (f n) 0 μ) atTop
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>hp0 : p ≠ 0<GOAL>eLpNorm f_lim p μ ≤ liminf (fun n => eLpNorm (f n) p μ) atTop
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm f_lim p μ ≤ liminf (fun n => eLpNorm (f n) p μ) atTop
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm' f_lim p.toReal μ ≤ liminf (fun n => eLpNorm' (f n) p.toReal μ) atTop
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E✝<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<VAR>hp_pos : 0 < p.toReal<GOAL>eLpNorm' f_lim p.toReal μ ≤ liminf (fun n => eLpNorm' (f n) p.toReal μ) atTop
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d - x) = ∫ (x : ℝ) in d - b..d - a, f x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hs : 1 ∈ s<VAR>hn : m ≤ n<GOAL>s ^ m ⊆ s ^ n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hs : 1 ∈ s<GOAL>s ^ m ⊆ s ^ m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hs : 1 ∈ s<VAR>n✝ : ℕ<VAR>hmn✝ : m ≤ n✝<VAR>ih : s ^ m ⊆ s ^ n✝<GOAL>s ^ m ⊆ s ^ (n✝ + 1)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : DecompositionMonoid R<VAR>x : R<VAR>hx : Squarefree x<VAR>y : R<VAR>hy : x ∣ y ^ 2<GOAL>x ∣ y
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : DecompositionMonoid R<VAR>y a b : R<VAR>ha : a ∣ y<VAR>hb : b ∣ y<VAR>hx : Squarefree (a * b)<VAR>hy : a * b ∣ y ^ 2<GOAL>a * b ∣ y
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a b : A<GOAL>σ (a * b) \ {0} = σ (b * a) \ {0}
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a b : A<GOAL>∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a b x✝ y✝ : A<VAR>k : 𝕜<VAR>k_neq : k ∉ {0}<VAR>k_mem : ↑(Units.mk0 k k_neq) ∈ σ (x✝ * y✝)<GOAL>k ∈ σ (y✝ * x✝) \ {0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<GOAL>↑(v.restrict i) j = ↑v (j ∩ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<GOAL>↑{ measureOf' := fun s => if MeasurableSet s then ↑v (s ∩ i) else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ } j = ↑v (j ∩ i)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<GOAL>‖0‖ = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<GOAL>0 ∈ closure ↑S
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃<GOAL>(sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁)) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃<GOAL>(sc • sa • r₁ + (sc • ra • r₂ + rc • r₃)) /ₒ (sc * (sa * s₁)) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>r₃ : X<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₁ = ra * ↑s₂<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃<GOAL>r₁ /ₒ s₁ + (ra • r₂ /ₒ (sa * s₁) + rc • r₃ /ₒ (sc * (sa * s₁))) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Integrable f μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>Integrable f (c • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Memℒp f 1 μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>Memℒp f 1 (c • μ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : R0Space X<VAR>x y : X<GOAL>IsCompact (closure {x})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : R0Space X<VAR>x y : X<VAR>ι✝ : Type u_1<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hxU : closure {x} ⊆ ⋃ i, U i<GOAL>∃ t, closure {x} ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : R0Space X<VAR>x y : X<VAR>ι✝ : Type u_1<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hxU : closure {x} ⊆ ⋃ i, U i<VAR>i : ι✝<VAR>hi : x ∈ U i<GOAL>∃ t, closure {x} ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : R0Space X<VAR>x y✝ : X<VAR>ι✝ : Type u_1<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hxU : closure {x} ⊆ ⋃ i, U i<VAR>i : ι✝<VAR>hi : x ∈ U i<VAR>y : X<VAR>hy : y ∈ closure {x}<GOAL>y ∈ ⋃ i_1 ∈ {i}, U i_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : R0Space X<VAR>x y✝ : X<VAR>ι✝ : Type u_1<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hxU : closure {x} ⊆ ⋃ i, U i<VAR>i : ι✝<VAR>hi : x ∈ U i<VAR>y : X<VAR>hy : y ⤳ x<GOAL>y ∈ ⋃ i_1 ∈ {i}, U i_1
<VAR>a✝ n a : ℕ<VAR>L : List ℕ<VAR>hL : Sorted (fun x x_1 => x < x_1) (a :: L)<GOAL>(map (fun i => 2 ^ i) (a :: L)).sum.bitIndices = a :: L
<VAR>a✝ n a : ℕ<VAR>L : List ℕ<VAR>hL✝ : Sorted (fun x x_1 => x < x_1) (a :: L)<VAR>haL : ∀ b ∈ L, a < b<VAR>hL : Sorted (fun x x_1 => x < x_1) L<GOAL>(map (fun i => 2 ^ i) (a :: L)).sum.bitIndices = a :: L
<VAR>a✝ n a : ℕ<VAR>L : List ℕ<VAR>hL✝ : Sorted (fun x x_1 => x < x_1) (a :: L)<VAR>hL : Sorted (fun x x_1 => x < x_1) L<VAR>haL : ∀ b ∈ L, a + 1 ≤ b<GOAL>(map (fun i => 2 ^ i) (a :: L)).sum.bitIndices = a :: L
<VAR>a✝ n a : ℕ<VAR>L₀ : List ℕ<VAR>hL₀ : Sorted (fun x x_1 => x < x_1) L₀<VAR>hL✝ : Sorted (fun x x_1 => x < x_1) (a :: map (fun x => x + a + 1) L₀)<VAR>hL : Sorted (fun x x_1 => x < x_1) (map (fun x => x + a + 1) L₀)<VAR>haL : ∀ b ∈ map (fun x => x + a + 1) L₀, a + 1 ≤ b<VAR>x✝ : L₀.length < (a :: map (fun x => x + a + 1) L₀).length<VAR>hrw : ((fun x => 2 ^ x) ∘ fun x => x + a + 1) = fun i => 2 ^ a * (2 * 2 ^ i)<GOAL>(map (fun i => 2 ^ i) (a :: map (fun x => x + a + 1) L₀)).sum.bitIndices = a :: map (fun x => x + a + 1) L₀
<VAR>a✝ n a : ℕ<VAR>L₀ : List ℕ<VAR>hL₀ : Sorted (fun x x_1 => x < x_1) L₀<VAR>hL✝ : Sorted (fun x x_1 => x < x_1) (a :: map (fun x => x + a + 1) L₀)<VAR>hL : Sorted (fun x x_1 => x < x_1) (map (fun x => x + a + 1) L₀)<VAR>haL : ∀ b ∈ map (fun x => x + a + 1) L₀, a + 1 ≤ b<VAR>x✝ : L₀.length < (a :: map (fun x => x + a + 1) L₀).length<VAR>hrw : ((fun x => 2 ^ x) ∘ fun x => x + a + 1) = fun i => 2 ^ a * (2 * 2 ^ i)<GOAL>(2 ^ a + 2 ^ a * (2 * (map (HPow.hPow 2) L₀).sum)).bitIndices = a :: map (fun x => x + a + 1) L₀