ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
<VAR>m n : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ Fin.last n<GOAL>(finSuccEquiv' (Fin.last n)) i = some (i.castLT ⋯)
<VAR>m n : ℕ<VAR>i : Fin n<VAR>h : i.castSucc ≠ Fin.last n<GOAL>(finSuccEquiv' (Fin.last n)) i.castSucc = some (i.castSucc.castLT ⋯)
<VAR>m n : ℕ<VAR>i : Fin n<VAR>h : i.castSucc ≠ Fin.last n<GOAL>some i = some (i.castSucc.castLT ⋯)
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsAntisymm α r<VAR>a : α<GOAL>r a a ∧ r a a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>hn : x ^ n = 0<GOAL>IsNilpotent (-x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>hn : x ^ n = 0<GOAL>(-x) ^ n = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x y : G<VAR>h : orderOf x = orderOf y<VAR>n : ℕ<GOAL>(zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x y : G<VAR>h : orderOf x = orderOf y<VAR>n : ℕ<GOAL>(finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z✝ X Y Z Z' : C<VAR>h : Z ⟶ Z'<GOAL>(𝟙 (X ⊗ Y) ⊗ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ 𝟙 Y ⊗ h)
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : P<VAR>I J : FractionalIdeal S P<GOAL>I = spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.51945, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : S.HasHomology<VAR>inst✝ : HasKernel S.g<GOAL>S.Exact ↔ Epi (kernel.lift S.g S.f ⋯)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.51945, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : S.HasHomology<VAR>inst✝ : HasKernel S.g<GOAL>Epi S.toCycles ↔ Epi (kernel.lift S.g S.f ⋯)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.51945, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : S.HasHomology<VAR>inst✝ : HasKernel S.g<GOAL>Arrow.mk S.toCycles ≅ Arrow.mk (kernel.lift S.g S.f ⋯)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x y : α<VAR>hf : IsRingHom f<GOAL>f 0 = f (0 + 0) - f 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x y : α<VAR>hf : IsRingHom f<GOAL>f 0 = f 0 + f 0 - f 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup H<VAR>inst✝² : NormedSpace 𝕜 H<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace G<VAR>f : F → G<VAR>g : E → F<VAR>s : Set F<VAR>t : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s (g x)<VAR>hg : AnalyticWithinAt 𝕜 g t x<VAR>h : MapsTo g t s<GOAL>AnalyticWithinAt 𝕜 (f ∘ g) t x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup H<VAR>inst✝² : NormedSpace 𝕜 H<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace G<VAR>f : F → G<VAR>g : E → F<VAR>s : Set F<VAR>t : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s (g x)<VAR>hg : AnalyticWithinAt 𝕜 g t x<VAR>h : MapsTo g t s<VAR>f' : F → G<VAR>left✝ : f (g x) = f' (g x)<VAR>ef : f =ᶠ[𝓝[s] g x] f'<VAR>hf' : AnalyticAt 𝕜 f' (g x)<GOAL>AnalyticWithinAt 𝕜 (f ∘ g) t x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup H<VAR>inst✝² : NormedSpace 𝕜 H<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace G<VAR>f : F → G<VAR>g : E → F<VAR>s : Set F<VAR>t : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s (g x)<VAR>hg : AnalyticWithinAt 𝕜 g t x<VAR>h : MapsTo g t s<VAR>f' : F → G<VAR>left✝ : f (g x) = f' (g x)<VAR>ef : f =ᶠ[𝓝[s] g x] f'<VAR>hf' : AnalyticAt 𝕜 f' (g x)<VAR>g' : E → F<VAR>gx : g x = g' x<VAR>eg : g =ᶠ[𝓝[t] x] g'<VAR>hg' : AnalyticAt 𝕜 g' x<GOAL>AnalyticWithinAt 𝕜 (f ∘ g) t x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup H<VAR>inst✝² : NormedSpace 𝕜 H<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace G<VAR>f : F → G<VAR>g : E → F<VAR>s : Set F<VAR>t : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s (g x)<VAR>hg : AnalyticWithinAt 𝕜 g t x<VAR>h : MapsTo g t s<VAR>f' : F → G<VAR>left✝ : f (g x) = f' (g x)<VAR>ef : f =ᶠ[𝓝[s] g x] f'<VAR>hf' : AnalyticAt 𝕜 f' (g x)<VAR>g' : E → F<VAR>gx : g x = g' x<VAR>eg : g =ᶠ[𝓝[t] x] g'<VAR>hg' : AnalyticAt 𝕜 g' x<GOAL>ContinuousWithinAt (f ∘ g) t x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup H<VAR>inst✝² : NormedSpace 𝕜 H<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace G<VAR>f : F → G<VAR>g : E → F<VAR>s : Set F<VAR>t : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s (g x)<VAR>hg : AnalyticWithinAt 𝕜 g t x<VAR>h : MapsTo g t s<VAR>f' : F → G<VAR>left✝ : f (g x) = f' (g x)<VAR>ef : f =ᶠ[𝓝[s] g x] f'<VAR>hf' : AnalyticAt 𝕜 f' (g x)<VAR>g' : E → F<VAR>gx : g x = g' x<VAR>eg : g =ᶠ[𝓝[t] x] g'<VAR>hg' : AnalyticAt 𝕜 g' x<GOAL>f ∘ g =ᶠ[𝓝[t] x] f' ∘ g'
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup H<VAR>inst✝² : NormedSpace 𝕜 H<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace G<VAR>f : F → G<VAR>g : E → F<VAR>s : Set F<VAR>t : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s (g x)<VAR>hg : AnalyticWithinAt 𝕜 g t x<VAR>h : MapsTo g t s<VAR>f' : F → G<VAR>left✝ : f (g x) = f' (g x)<VAR>ef : f =ᶠ[𝓝[s] g x] f'<VAR>hf' : AnalyticAt 𝕜 f' (g x)<VAR>g' : E → F<VAR>gx : g x = g' x<VAR>eg : g =ᶠ[𝓝[t] x] g'<VAR>hg' : AnalyticAt 𝕜 g' x<GOAL>AnalyticAt 𝕜 (f' ∘ g') x
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), x + z < f x<GOAL>z < τ f
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), x + z < f x<VAR>x : ℝ<VAR>hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y<GOAL>z < τ f
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), x + z < f x<VAR>x : ℝ<VAR>hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y<GOAL>f x - x ≤ τ f
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), x + z < f x<VAR>x : ℝ<VAR>hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y<GOAL>∀ (x_1 : ℝ), x_1 + (f x - x) ≤ f x_1
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), x + z < f x<VAR>x : ℝ<VAR>hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y<GOAL>∀ (x_1 : ℝ), f x - x ≤ f x_1 - x_1
<VAR>α β : Type u<VAR>a : Cardinal.{u_1}<VAR>ha : a < ℵ₀<GOAL>succ a < ℵ₀
<VAR>α β : Type u<VAR>n : ℕ<VAR>ha : ↑n < ℵ₀<GOAL>succ ↑n < ℵ₀
<VAR>α β : Type u<VAR>n : ℕ<VAR>ha : ↑n < ℵ₀<GOAL>↑n.succ < ℵ₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<GOAL>↑↑(condexpIndL1Fin hm ⋯ ⋯ x) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x + condexpIndL1Fin hm ht hμt x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<GOAL>↑↑(condexpIndL1Fin hm ⋯ ⋯ x) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x + condexpIndL1Fin hm ht hμt x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<GOAL>↑↑(condexpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x + condexpIndL1Fin hm ht hμt x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<GOAL>↑↑(condexpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x) + ↑↑(condexpIndL1Fin hm ht hμt x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<GOAL>↑↑(condexpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x) + ↑↑(condexpIndL1Fin hm ht hμt x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<VAR>ht_eq : ↑↑(condexpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm ht hμt x)<GOAL>↑↑(condexpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x) + ↑↑(condexpIndL1Fin hm ht hμt x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<VAR>ht_eq : ↑↑(condexpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm ht hμt x)<GOAL>↑↑(condexpIndSMul hm ⋯ hμst x) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm ht hμt x) x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<VAR>ht_eq : ↑↑(condexpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm ht hμt x)<GOAL>↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 ⋯ hμst 1))) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm ht hμt x) x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<VAR>ht_eq : ↑↑(condexpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm ht hμt x)<GOAL>↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1 + indicatorConstLp 2 ht hμt 1))) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm ht hμt x) x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<VAR>ht_eq : ↑↑(condexpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm ht hμt x)<GOAL>↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1) + (condexpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1))) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm ht hμt x) x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<VAR>ht_eq : ↑↑(condexpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm ht hμt x)<GOAL>↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) (↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) + ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1)))) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm ht hμt x) x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<VAR>ht_eq : ↑↑(condexpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm ht hμt x)<GOAL>↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) + (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1))) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm ht hμt x) x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<VAR>hs_eq : ↑↑(condexpIndL1Fin hm hs hμs x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)<VAR>ht_eq : ↑↑(condexpIndL1Fin hm ht hμt x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm ht hμt x)<GOAL>↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) + ↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1))) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm ht hμt x) x_1
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ g, (∀ (x : α), g x < ↑(f x)) ∧ UpperSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>g : α → EReal<VAR>g_lt_f : ∀ (x : α), ↑(-f x) < g x<VAR>gcont : LowerSemicontinuous g<VAR>g_integrable : Integrable (fun x => (g x).toReal) μ<VAR>g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤<VAR>gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε<GOAL>∃ g, (∀ (x : α), g x < ↑(f x)) ∧ UpperSemicontinuous g ∧ Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F K<GOAL>IsPurelyInseparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F K<VAR>x : E<VAR>h : IsSeparable F x<GOAL>x ∈ (algebraMap F E).range