ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>p : TangentBundle I M<VAR>hg : MDifferentiableWithinAt I' I'' g u (f p.proj)<VAR>hf : MDifferentiableWithinAt I I' f s p.proj<VAR>h : s ⊆ f ⁻¹' u<VAR>hps : UniqueMDiffWithinAt I s p.proj<GOAL>(mfderivWithin I I'' (g ∘ f) s p.proj) p.snd = (mfderivWithin I' I'' g u (f p.proj)) ((mfderivWithin I I' f s p.proj) p.snd)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>p : TangentBundle I M<VAR>hg : MDifferentiableWithinAt I' I'' g u (f p.proj)<VAR>hf : MDifferentiableWithinAt I I' f s p.proj<VAR>h : s ⊆ f ⁻¹' u<VAR>hps : UniqueMDiffWithinAt I s p.proj<GOAL>((mfderivWithin I' I'' g u (f p.proj)).comp (mfderivWithin I I' f s p.proj)) p.snd = (mfderivWithin I' I'' g u (f p.proj)) ((mfderivWithin I I' f s p.proj) p.snd)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>hs : StrictConvex 𝕜 s<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>hx₀ : x ≠ 0<VAR>t : 𝕜<VAR>ht : 1 < t<GOAL>x ∈ t • interior s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>hs : StrictConvex 𝕜 s<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>hx₀ : x ≠ 0<VAR>t : 𝕜<VAR>ht : 1 < t<GOAL>t⁻¹ • x ∈ interior s
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M<VAR>a b : ℕ<VAR>hab : a ≤ b + 1<VAR>f : ℕ → M<GOAL>∏ k ∈ Icc a (b + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : NumberField k<VAR>inst✝ : IsGalois k K<GOAL>card (InfinitePlace K) = (Finset.filter (IsUnramifiedIn K) Finset.univ).card * finrank k K + (Finset.filter (IsUnramifiedIn K) Finset.univ)ᶜ.card * (finrank k K / 2)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝³ : SemilatticeInf α<VAR>s✝ : Finset β<VAR>H : s✝.Nonempty<VAR>f✝ : β → α<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : InfHomClass F α β<VAR>f : F<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>g : ι → α<GOAL>f (s.inf' hs g) = s.inf' hs (⇑f ∘ g)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasPushouts C<VAR>W X Y Z : C<VAR>f✝ : X ⟶ Y<VAR>g✝ : X ⟶ Z<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g₁ : X ⟶ W<VAR>inst✝¹ : Epi g₁<VAR>g₂ : W ⟶ Z<VAR>inst✝ : Mono g₂<VAR>hg : g₁ ≫ g₂ = g<VAR>f' : W ⟶ Y<VAR>hf : g₁ ≫ f' = f<VAR>t : PushoutCocone f g<VAR>ht : IsColimit t<GOAL>Mono t.inl
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>i : ℕ<VAR>hp : 1 ≤ p.natDegree<GOAL>(normalizeScaleRoots p).coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>i : ℕ<VAR>hp : 1 ≤ p.natDegree<GOAL>(if p.coeff i = 0 then 0 else if i = p.natDegree then p.leadingCoeff ^ i else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff ^ i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>n.sqrt ^ 2 ≤ n
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<GOAL>Commute P Q
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<VAR>PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R<GOAL>Commute P Q
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<VAR>PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R<VAR>QP_eq_QPQ : Q * P = Q * P * Q<GOAL>Commute P Q
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)<GOAL>Function.Surjective ⇑(f.val.app (op U))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>x : ↥U<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>x : ↥U<VAR>s₀ : (forget C).obj ((stalkFunctor C ↑x).obj F.val)<VAR>hs₀ : ((stalkFunctor C ↑x).map f.val) s₀ = (G.presheaf.germ x) t<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>x : ↥U<VAR>s₀ : (forget C).obj ((stalkFunctor C ↑x).obj F.val)<VAR>hs₀ : ((stalkFunctor C ↑x).map f.val) s₀ = (G.presheaf.germ x) t<VAR>V₁ : Opens ↑X<VAR>hxV₁ : ↑x ∈ V₁<VAR>s₁ : (forget C).obj (F.presheaf.obj (op V₁))<VAR>hs₁ : (F.presheaf.germ ⟨↑x, hxV₁⟩) s₁ = s₀<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>x : ↥U<VAR>V₁ : Opens ↑X<VAR>hxV₁ : ↑x ∈ V₁<VAR>s₁ : (forget C).obj (F.presheaf.obj (op V₁))<VAR>hs₁ : (germ G.val ⟨↑x, hxV₁⟩) ((f.val.app (op V₁)) s₁) = (G.presheaf.germ x) t<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>x : ↥U<VAR>V₁ : Opens ↑X<VAR>hxV₁ : ↑x ∈ V₁<VAR>s₁ : (forget C).obj (F.presheaf.obj (op V₁))<VAR>hs₁ : (germ G.val ⟨↑x, hxV₁⟩) ((f.val.app (op V₁)) s₁) = (G.presheaf.germ x) t<VAR>V₂ : Opens ↑X<VAR>hxV₂ : ↑x ∈ V₂<VAR>iV₂V₁ : V₂ ⟶ V₁<VAR>iV₂U : V₂ ⟶ U<VAR>heq : (G.presheaf.map iV₂V₁.op) ((f.val.app (op V₁)) s₁) = (G.presheaf.map iV₂U.op) t<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ iVU s, (f.val.app (op V)) s = (G.val.map iVU.op) t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : PreservesFilteredColimits (forget C)<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : PreservesLimits (forget C)<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>U : Opens ↑X<VAR>h : ∀ (x : ↥U), Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)<VAR>t : (forget C).obj (G.val.obj (op U))<VAR>x : ↥U<VAR>V₁ : Opens ↑X<VAR>hxV₁ : ↑x ∈ V₁<VAR>s₁ : (forget C).obj (F.presheaf.obj (op V₁))<VAR>hs₁ : (germ G.val ⟨↑x, hxV₁⟩) ((f.val.app (op V₁)) s₁) = (G.presheaf.germ x) t<VAR>V₂ : Opens ↑X<VAR>hxV₂ : ↑x ∈ V₂<VAR>iV₂V₁ : V₂ ⟶ V₁<VAR>iV₂U : V₂ ⟶ U<VAR>heq : (G.presheaf.map iV₂V₁.op) ((f.val.app (op V₁)) s₁) = (G.presheaf.map iV₂U.op) t<GOAL>(f.val.app (op V₂)) ((F.val.map iV₂V₁.op) s₁) = (G.val.map iV₂U.op) t
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p μ)<VAR>hf_meas : f ∈ lpMeasSubgroup F m p μ<GOAL>Memℒp (Exists.choose ⋯) p (μ.trim hm)
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p μ)<VAR>hf_meas : f ∈ lpMeasSubgroup F m p μ<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<GOAL>Memℒp (Exists.choose ⋯) p (μ.trim hm)
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p μ)<VAR>hf_meas : f ∈ lpMeasSubgroup F m p μ<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>g : α → F := Exists.choose hf<GOAL>Memℒp (Exists.choose ⋯) p (μ.trim hm)
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p μ)<VAR>hf_meas : f ∈ lpMeasSubgroup F m p μ<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>g : α → F := Exists.choose hf<VAR>hg : StronglyMeasurable (Exists.choose hf)<VAR>hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf<GOAL>Memℒp (Exists.choose ⋯) p (μ.trim hm)
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p μ)<VAR>hf_meas : f ∈ lpMeasSubgroup F m p μ<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>g : α → F := Exists.choose hf<VAR>hg : StronglyMeasurable (Exists.choose hf)<VAR>hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf<GOAL>Memℒp g p (μ.trim hm)
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p μ)<VAR>hf_meas : f ∈ lpMeasSubgroup F m p μ<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>g : α → F := Exists.choose hf<VAR>hg : StronglyMeasurable (Exists.choose hf)<VAR>hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf<GOAL>eLpNorm g p (μ.trim hm) < ⊤
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p μ)<VAR>hf_meas : f ∈ lpMeasSubgroup F m p μ<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>g : α → F := Exists.choose hf<VAR>hg : StronglyMeasurable (Exists.choose hf)<VAR>hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf<VAR>h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm (↑↑f) p μ<GOAL>eLpNorm g p (μ.trim hm) < ⊤
<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p μ)<VAR>hf_meas : f ∈ lpMeasSubgroup F m p μ<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>g : α → F := Exists.choose hf<VAR>hg : StronglyMeasurable (Exists.choose hf)<VAR>hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf<VAR>h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm (↑↑f) p μ<GOAL>eLpNorm (↑↑f) p μ < ⊤
<VAR>m✝ n m : ℕ<GOAL>(m + 1) % 2 = 1 ↔ m % 2 = 0
<VAR>x p : ℝ<VAR>hp : p > 2<VAR>hxp : LiouvilleWith p x<GOAL>x ∈ ⋃ m, (fun x => x + ↑m) ⁻¹' ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
<VAR>x p : ℝ<VAR>hp : p > 2<VAR>hxp : LiouvilleWith p x<VAR>n : ℕ<VAR>hn : 1 / (↑n + 1) < p - 2<GOAL>x ∈ ⋃ m, (fun x => x + ↑m) ⁻¹' ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
<VAR>x p : ℝ<VAR>hp : p > 2<VAR>hxp : LiouvilleWith p x<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<GOAL>x ∈ ⋃ m, (fun x => x + ↑m) ⁻¹' ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
<VAR>x p : ℝ<VAR>hp : p > 2<VAR>hxp : LiouvilleWith p x<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<GOAL>∀ (y : ℝ), LiouvilleWith p y → y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<GOAL>∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<GOAL>∀ (x_1 : ℕ), (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < ↑x_1 ^ (-(2 + 1 / (↑n + 1)))) ∧ 1 ≤ x_1 → ∃ a ∈ Finset.Icc 0 ↑x_1, |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ (2 + 1 / ↑(n + 1))
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>hb : 1 ≤ b<VAR>a : ℤ<VAR>hlt : |x - ↑a / ↑b| < ↑b ^ (-(2 + 1 / (↑n + 1)))<GOAL>∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>hb : 1 ≤ b<VAR>a : ℤ<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)<GOAL>∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>hb : 1 ≤ b<VAR>a : ℤ<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)<GOAL>a ∈ Finset.Icc 0 ↑b
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>a : ℤ<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)<VAR>hb : 1 ≤ ↑b<GOAL>a ∈ Finset.Icc 0 ↑b
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>a : ℤ<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)<VAR>hb : 1 ≤ ↑b<VAR>hb0 : 0 < ↑b<GOAL>a ∈ Finset.Icc 0 ↑b
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>a : ℤ<VAR>hb : 1 ≤ ↑b<VAR>hb0 : 0 < ↑b<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b<GOAL>a ∈ Finset.Icc 0 ↑b
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>a : ℤ<VAR>hb : 1 ≤ ↑b<VAR>hb0 : 0 < ↑b<VAR>hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b<GOAL>a ∈ Finset.Icc 0 ↑b
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>a : ℤ<VAR>hb : 1 ≤ ↑b<VAR>hb0 : 0 < ↑b<VAR>hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b<GOAL>↑(-1) < ↑a ∧ ↑a < ↑(1 + ↑b)
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>a : ℤ<VAR>hb : 1 ≤ ↑b<VAR>hb0 : 0 < ↑b<VAR>hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b<GOAL>-1 < ↑a ∧ ↑a < 1 + ↑b
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>a : ℤ<VAR>hb : 1 ≤ ↑b<VAR>hb0 : 0 < ↑b<VAR>hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b<GOAL>-1 ≤ x * ↑b - 1
<VAR>p : ℝ<VAR>hp : p > 2<VAR>n : ℕ<VAR>hn : 2 + 1 / (↑n + 1) < p<VAR>x : ℝ<VAR>hxp : LiouvilleWith p x<VAR>hx01 : x ∈ Ico 0 1<VAR>b : ℕ<VAR>a : ℤ<VAR>hb : 1 ≤ ↑b<VAR>hb0 : 0 < ↑b<VAR>hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b<GOAL>1 + x * ↑b ≤ 1 + ↑b
<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>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝¹ : ReflectsLimit (cospan h i) F<VAR>inst✝ : F.Faithful<VAR>H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>F.map (f ≫ h) = F.map (g ≫ i)
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>‖log ↑n‖ ≤ ↑n ^ ε / ε
<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>‖log ↑0‖ ≤ ↑0 ^ ε / ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>h : n > 0<GOAL>‖log ↑n‖ ≤ ↑n ^ ε / ε
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>h : n > 0<GOAL>Real.log ↑n ≤ ↑n ^ ε / ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>S : ι → Set X<VAR>hc : s.Countable<VAR>hcomp : ∀ i ∈ s, IsSigmaCompact (S i)<GOAL>IsSigmaCompact (⋃ i ∈ s, S i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>S : ι → Set X<VAR>hc : s.Countable<VAR>hcomp : ∀ i ∈ s, IsSigmaCompact (S i)<VAR>this : Countable ↑s<GOAL>IsSigmaCompact (⋃ i ∈ s, S i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>S : ι → Set X<VAR>hc : s.Countable<VAR>hcomp : ∀ i ∈ s, IsSigmaCompact (S i)<VAR>this : Countable ↑s<GOAL>IsSigmaCompact (⋃ x, S ↑x)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>disc : TotallyDisconnectedSpace X<VAR>x y : X<VAR>h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y<GOAL>x = y