ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ : Set α<VAR>inst✝ : Finite ι<VAR>t : ι → Set α<VAR>h : Pairwise (Disjoint on t)<VAR>ht : ∀ (i : ι), (t i).Finite<VAR>val✝ : Fintype ι<GOAL>∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : AddCommMonoid β<VAR>f : ι →₀ α<VAR>i : ι<VAR>a : α<VAR>g : ι → α → β<VAR>hg : ∀ (i : ι), g i 0 = 0<VAR>hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂<GOAL>(f.update i a).sum g + g i (f i) = f.sum g + g i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : AddCommMonoid β<VAR>f : ι →₀ α<VAR>i : ι<VAR>a : α<VAR>g : ι → α → β<VAR>hg : ∀ (i : ι), g i 0 = 0<VAR>hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂<GOAL>(erase i f).sum g + (single i a).sum g + g i (f i) = f.sum g + g i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : AddCommMonoid β<VAR>f : ι →₀ α<VAR>i : ι<VAR>a : α<VAR>g : ι → α → β<VAR>hg : ∀ (i : ι), g i 0 = 0<VAR>hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂<GOAL>(erase i f).sum g + (single i a).sum g + g i (f i) = (f.update i (f i)).sum g + g i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : AddCommMonoid β<VAR>f : ι →₀ α<VAR>i : ι<VAR>a : α<VAR>g : ι → α → β<VAR>hg : ∀ (i : ι), g i 0 = 0<VAR>hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂<GOAL>(erase i f).sum g + ((single i a).sum g + g i (f i)) = (erase i f).sum g + ((single i (f i)).sum g + g i a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : AddCommMonoid β<VAR>f : ι →₀ α<VAR>i : ι<VAR>a : α<VAR>g : ι → α → β<VAR>hg : ∀ (i : ι), g i 0 = 0<VAR>hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂<GOAL>(single i a).sum g + g i (f i) = (single i (f i)).sum g + g i a
<VAR>F : Type u_1<VAR>Γ✝ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>inst✝¹ : FunLike F ℍ ℂ<VAR>k : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>inst✝ : SlashInvariantFormClass F Γ k<VAR>f : F<VAR>γ : ↥Γ<VAR>z : ℍ<GOAL>f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * f z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>s : Finset (Fin n)<GOAL>s.card ≤ n
<VAR>n : ℕ<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>ih : ∀ m < Nat.card G, ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G], Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<GOAL>∃ H, N.IsComplement' H
<VAR>n : ℕ<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>ih : ∀ m < Nat.card G, ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G], Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<VAR>h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x<GOAL>False
<VAR>n : ℕ<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>ih : ∀ m < Nat.card G, ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G], Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<VAR>h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x<VAR>this : N.IsCommutative<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a✝ : ℝ<VAR>absorbs : Absorbent ℝ s<VAR>a : ℝ<VAR>x✝ : E<GOAL>x✝ ∈ {x | gauge s x < a} ↔ x✝ ∈ ⋃ r, ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a✝ : ℝ<VAR>absorbs : Absorbent ℝ s<VAR>a : ℝ<VAR>x✝ : E<GOAL>gauge s x✝ < a ↔ ∃ i, 0 < i ∧ i < a ∧ x✝ ∈ i • s
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPullback b.fst b.snd 0 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<GOAL>f = f'
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<GOAL>∀ (x : Ω[S⁄R]), f x = f' x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<VAR>x : Ω[S⁄R]<GOAL>f x = f' x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<VAR>x : Ω[S⁄R]<VAR>this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))<GOAL>f x = f' x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<VAR>x : Ω[S⁄R]<VAR>this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))<GOAL>∀ x ∈ Set.range ⇑(KaehlerDifferential.D R S), f x = f' x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<VAR>x : Ω[S⁄R]<VAR>this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))<GOAL>f 0 = f' 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<VAR>x : Ω[S⁄R]<VAR>this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))<GOAL>∀ (x y : Ω[S⁄R]), f x = f' x → f y = f' y → f (x + y) = f' (x + y)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<VAR>x : Ω[S⁄R]<VAR>this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))<GOAL>∀ (a : S) (x : Ω[S⁄R]), f x = f' x → f (a • x) = f' (a • x)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>AEStronglyMeasurable (fun v => VectorFourier.fourierPowSMulRight L f v n) μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>AEStronglyMeasurable (fun v => (-(2 * ↑π * I)) ^ n • ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)) μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>AEStronglyMeasurable (fun x => ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x_1 => L x)) (f x)) μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>AEStronglyMeasurable (fun x => (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x_1 => L x) μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<VAR>n : ℕ<GOAL>Continuous fun x => (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x_1 => L x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b a : K<GOAL>1 / -a = 1 / (-1 * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b a : K<GOAL>1 / (-1 * a) = 1 / a * (1 / -1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b a : K<GOAL>1 / a * (1 / -1) = 1 / a * -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b a : K<GOAL>1 / a * -1 = -(1 / a)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<GOAL>X - C a ∣ p - C (eval a p)
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<GOAL>Continuous f ↔ ∀ (y : E), Continuous fun x => (f x) y
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp a b - b = -toIocDiv hp a b • p
<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 : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(Lp F p μ)<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<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 : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(Lp F p μ)<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<GOAL>∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), AEStronglyMeasurable' m f μ → AEStronglyMeasurable' m g μ → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)
<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 : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f✝ : ↥(Lp F p μ)<VAR>hf✝ : AEStronglyMeasurable' m (↑↑f✝) μ<VAR>f g : α → F<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>h_disj : Disjoint (Function.support f) (Function.support g)<VAR>hPf : P (Memℒp.toLp f hf)<VAR>hPg : P (Memℒp.toLp g hg)<VAR>s_f : Set α := Function.support (AEStronglyMeasurable'.mk f hfm)<GOAL>P (Memℒp.toLp f hf + Memℒp.toLp g hg)
<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 : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f✝ : ↥(Lp F p μ)<VAR>hf✝ : AEStronglyMeasurable' m (↑↑f✝) μ<VAR>f g : α → F<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>h_disj : Disjoint (Function.support f) (Function.support g)<VAR>hPf : P (Memℒp.toLp f hf)<VAR>hPg : P (Memℒp.toLp g hg)<VAR>s_f : Set α := Function.support (AEStronglyMeasurable'.mk f hfm)<VAR>hs_f : MeasurableSet s_f<GOAL>P (Memℒp.toLp f hf + Memℒp.toLp g hg)
<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 : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f✝ : ↥(Lp F p μ)<VAR>hf✝ : AEStronglyMeasurable' m (↑↑f✝) μ<VAR>f g : α → F<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>h_disj : Disjoint (Function.support f) (Function.support g)<VAR>hPf : P (Memℒp.toLp f hf)<VAR>hPg : P (Memℒp.toLp g hg)<VAR>s_f : Set α := Function.support (AEStronglyMeasurable'.mk f hfm)<VAR>hs_f : MeasurableSet s_f<VAR>hs_f_eq : s_f =ᶠ[ae μ] Function.support f<GOAL>P (Memℒp.toLp f hf + Memℒp.toLp g hg)
<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 : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f✝ : ↥(Lp F p μ)<VAR>hf✝ : AEStronglyMeasurable' m (↑↑f✝) μ<VAR>f g : α → F<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>h_disj : Disjoint (Function.support f) (Function.support g)<VAR>hPf : P (Memℒp.toLp f hf)<VAR>hPg : P (Memℒp.toLp g hg)<VAR>s_f : Set α := Function.support (AEStronglyMeasurable'.mk f hfm)<VAR>hs_f : MeasurableSet s_f<VAR>hs_f_eq : s_f =ᶠ[ae μ] Function.support f<VAR>s_g : Set α := Function.support (AEStronglyMeasurable'.mk g hgm)<GOAL>P (Memℒp.toLp f hf + Memℒp.toLp g hg)
<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 : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), StronglyMeasurable f → StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f✝ : ↥(Lp F p μ)<VAR>hf✝ : AEStronglyMeasurable' m (↑↑f✝) μ<VAR>f g : α → F<VAR>hf : Memℒp f p μ<VAR>hg : Memℒp g p μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>h_disj : Disjoint (Function.support f) (Function.support g)<VAR>hPf : P (Memℒp.toLp f hf)<VAR>hPg : P (Memℒp.toLp g hg)<VAR>s_f : Set α := Function.support (AEStronglyMeasurable'.mk f hfm)<VAR>hs_f : MeasurableSet s_f<VAR>hs_f_eq : s_f =ᶠ[ae μ] Function.support f<VAR>s_g : Set α := Function.support (AEStronglyMeasurable'.mk g hgm)<VAR>hs_g : MeasurableSet s_g<GOAL>P (Memℒp.toLp f hf + Memℒp.toLp g hg)