ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<VAR>hh : h = predictablePart (f + g) ℱ μ - g<VAR>hhpred : Adapted ℱ fun n => h (n + 1)<VAR>hhmgle : Martingale h ℱ μ<GOAL>martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<VAR>hh : h = predictablePart (f + g) ℱ μ - g<VAR>hhpred : Adapted ℱ fun n => h (n + 1)<VAR>hhmgle : Martingale h ℱ μ<GOAL>f n - martingalePart (f + g) ℱ μ n =ᶠ[ae μ] 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<VAR>hh : h = predictablePart (f + g) ℱ μ - g<VAR>hhpred : Adapted ℱ fun n => h (n + 1)<VAR>hhmgle : Martingale h ℱ μ<VAR>ω : Ω<VAR>hω : h n ω = h 0 ω<GOAL>(f n - martingalePart (f + g) ℱ μ n) ω = 0 ω
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<VAR>hh : h = predictablePart (f + g) ℱ μ - g<VAR>hhpred : Adapted ℱ fun n => h (n + 1)<VAR>hhmgle : Martingale h ℱ μ<VAR>ω : Ω<VAR>hω : (f - martingalePart (f + g) ℱ μ) n ω = (f - martingalePart (f + g) ℱ μ) 0 ω<GOAL>(f n - martingalePart (f + g) ℱ μ n) ω = 0 ω
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<VAR>hh : h = predictablePart (f + g) ℱ μ - g<VAR>hhpred : Adapted ℱ fun n => h (n + 1)<VAR>hhmgle : Martingale h ℱ μ<VAR>ω : Ω<VAR>hω : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω<GOAL>(f n - martingalePart (f + g) ℱ μ n) ω = 0 ω
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<VAR>hh : h = predictablePart (f + g) ℱ μ - g<VAR>hhpred : Adapted ℱ fun n => h (n + 1)<VAR>hhmgle : Martingale h ℱ μ<VAR>ω : Ω<VAR>hω : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω<GOAL>(f 0 - ((f + g) 0 - predictablePart (f + g) ℱ μ 0)) ω = 0 ω
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>S : Set (Set α)<VAR>x y : α<VAR>H : ∀ s ∈ S, x ∈ s ↔ y ∈ s<VAR>s : Set α<GOAL>MeasurableSet s → (x ∈ s ↔ y ∈ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>S : Set (Set α)<VAR>x y : α<VAR>H : ∀ s ∈ S, x ∈ s ↔ y ∈ s<VAR>s : Set α<GOAL>∀ t ∈ S, x ∈ t ↔ y ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>S : Set (Set α)<VAR>x y : α<VAR>H : ∀ s ∈ S, x ∈ s ↔ y ∈ s<VAR>s : Set α<GOAL>x ∈ ∅ ↔ y ∈ ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>S : Set (Set α)<VAR>x y : α<VAR>H : ∀ s ∈ S, x ∈ s ↔ y ∈ s<VAR>s : Set α<GOAL>∀ (t : Set α), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>S : Set (Set α)<VAR>x y : α<VAR>H : ∀ s ∈ S, x ∈ s ↔ y ∈ s<VAR>s : Set α<GOAL>∀ (f : ℕ → Set α), (∀ (n : ℕ), x ∈ f n ↔ y ∈ f n) → (x ∈ ⋃ i, f i ↔ y ∈ ⋃ i, f i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g✝ : Y → Z<VAR>g : Z → W<VAR>hf : IsProperMap f<VAR>hg : IsProperMap g<GOAL>IsProperMap (Prod.map f g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g✝ : Y → Z<VAR>g : Z → W<VAR>hf : Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x<VAR>hg : Continuous g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x<GOAL>Continuous (Prod.map f g) ∧ ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄, Tendsto (Prod.map f g) (↑𝒰) (𝓝 y) → ∃ x, Prod.map f g x = y ∧ ↑𝒰 ≤ 𝓝 x
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : α → E<GOAL>∫ (z : α × β), f z.1 ∂μ.prod ν = (ν univ).toReal • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : α → E<GOAL>∫ (z : β × α), f z.swap.1 ∂ν.prod μ = (ν univ).toReal • ∫ (x : α), f x ∂μ
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>h : ¬Acc (fun x x_1 => x < x_1) a<VAR>ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }<VAR>f : ι → Cardinal.{u} := Subtype.val<VAR>hι : Nonempty ι<VAR>c : Cardinal.{u}<VAR>hc : ¬Acc (fun x x_1 => x < x_1) c<VAR>h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)<GOAL>False
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>h : ¬Acc (fun x x_1 => x < x_1) a<VAR>ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }<VAR>f : ι → Cardinal.{u} := Subtype.val<VAR>hι : Nonempty ι<VAR>c : Cardinal.{u}<VAR>hc : ¬Acc (fun x x_1 => x < x_1) c<VAR>h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)<VAR>j : Cardinal.{u}<VAR>h' : j < c<VAR>hj : ¬Acc (fun x x_1 => x < x_1) j<GOAL>Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLE.proof_1
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>h : ¬Acc (fun x x_1 => x < x_1) a<VAR>ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }<VAR>f : ι → Cardinal.{u} := Subtype.val<VAR>hι : Nonempty ι<VAR>c : Cardinal.{u}<VAR>hc : ¬Acc (fun x x_1 => x < x_1) c<VAR>h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)<VAR>j : Cardinal.{u}<VAR>h' : j < c<VAR>hj : ¬Acc (fun x x_1 => x < x_1) j<VAR>this : #(Quotient.out (f ⟨c, hc⟩)) ≤ #(Quotient.out (f ⟨j, hj⟩))<GOAL>Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLE.proof_1
<VAR>M : Type u_1<VAR>inst✝²⁴ : Monoid M<VAR>N : Type u_2<VAR>inst✝²³ : Monoid N<VAR>P : Type u_3<VAR>inst✝²² : Monoid P<VAR>φ : M →* N<VAR>φ' : N →* M<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>A : Type u_4<VAR>inst✝²¹ : AddMonoid A<VAR>inst✝²⁰ : DistribMulAction M A<VAR>B : Type u_5<VAR>inst✝¹⁹ : AddMonoid B<VAR>inst✝¹⁸ : DistribMulAction N B<VAR>B₁ : Type u_6<VAR>inst✝¹⁷ : AddMonoid B₁<VAR>inst✝¹⁶ : DistribMulAction M B₁<VAR>C : Type u_7<VAR>inst✝¹⁵ : AddMonoid C<VAR>inst✝¹⁴ : DistribMulAction P C<VAR>A' : Type u_8<VAR>inst✝¹³ : AddGroup A'<VAR>inst✝¹² : DistribMulAction M A'<VAR>B' : Type u_9<VAR>inst✝¹¹ : AddGroup B'<VAR>inst✝¹⁰ : DistribMulAction N B'<VAR>R : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : MulSemiringAction M R<VAR>R' : Type u_11<VAR>inst✝⁷ : Ring R'<VAR>inst✝⁶ : MulSemiringAction M R'<VAR>S : Type u_12<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : MulSemiringAction N S<VAR>S' : Type u_13<VAR>inst✝³ : Ring S'<VAR>inst✝² : MulSemiringAction N S'<VAR>T : Type u_14<VAR>inst✝¹ : Semiring T<VAR>inst✝ : MulSemiringAction P T<VAR>f : R →ₑ+*[φ] S<VAR>x : R<GOAL>((MulSemiringActionHom.id N).comp f) x = f x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : SeminormedAddCommGroup G<VAR>x₀ : G<VAR>R : ℝ<VAR>hf : support f ⊆ ball 0 R<VAR>hg : ∀ x ∈ ball x₀ R, g x = g x₀<VAR>h2 : ∀ (t : G), (L (f t)) (g (x₀ - t)) = (L (f t)) (g x₀)<GOAL>(f ⋆[L, μ] g) x₀ = ∫ (t : G), (L (f t)) (g x₀) ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.withDensity f)<VAR>f' : α → ℝ≥0∞ := AEMeasurable.mk f hf<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.withDensity f)<VAR>f' : α → ℝ≥0∞ := AEMeasurable.mk f hf<VAR>this : μ.withDensity f = μ.withDensity f'<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>G : Type u<VAR>inst✝³ : Groupoid G<VAR>inst✝² : IsFreeGroupoid G<VAR>T : WideSubquiver (Symmetrify (Generators G))<VAR>inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)<VAR>X : Type u<VAR>inst✝ : Group X<VAR>f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X<VAR>f' : Labelling (Generators G) X := fun a b e => if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩<GOAL>∃! F, ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
<VAR>G : Type u<VAR>inst✝³ : Groupoid G<VAR>inst✝² : IsFreeGroupoid G<VAR>T : WideSubquiver (Symmetrify (Generators G))<VAR>inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)<VAR>X : Type u<VAR>inst✝ : Group X<VAR>f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X<VAR>f' : Labelling (Generators G) X := fun a b e => if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩<VAR>F' : G ⥤ CategoryTheory.SingleObj X<VAR>hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g<VAR>uF' : ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'<GOAL>∃! F, ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
<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>G : Type u_4<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : ChartedSpace H G<VAR>inst✝³ : Monoid G<VAR>inst✝² : SmoothMul I G<VAR>g h✝ : G<VAR>M : Type u_5<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>x : M<VAR>r : 𝕜<VAR>X Y : LeftInvariantDerivation I G<VAR>f f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>h : G<GOAL>((X f).comp (𝑳 I g)) h = (X (f.comp (𝑳 I g))) h
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : (𝓤 α).IsCountablyGenerated<VAR>inst✝ : SeparableSpace α<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : (𝓤 α).IsCountablyGenerated<VAR>inst✝ : SeparableSpace α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : (𝓤 α).IsCountablyGenerated<VAR>inst✝ : SeparableSpace α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>t : ℕ → Set (α × α)<VAR>hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i)<VAR>h_basis : (𝓤 α).HasAntitoneBasis t<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : (𝓤 α).IsCountablyGenerated<VAR>inst✝ : SeparableSpace α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>t : ℕ → Set (α × α)<VAR>h_basis : (𝓤 α).HasAntitoneBasis t<VAR>ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets<VAR>hto : ∀ (i : ℕ), IsOpen (t i)<VAR>hts : ∀ (i : ℕ), SymmetricRel (t i)<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : (𝓤 α).IsCountablyGenerated<VAR>inst✝ : SeparableSpace α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>t : ℕ → Set (α × α)<VAR>h_basis : (𝓤 α).HasAntitoneBasis t<VAR>ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets<VAR>hto : ∀ (i : ℕ), IsOpen (t i)<VAR>hts : ∀ (i : ℕ), SymmetricRel (t i)<GOAL>toTopologicalSpace = generateFrom (⋃ x ∈ s, range fun k => ball x (t k))
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : (𝓤 α).IsCountablyGenerated<VAR>inst✝ : SeparableSpace α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>t : ℕ → Set (α × α)<VAR>h_basis : (𝓤 α).HasAntitoneBasis t<VAR>ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets<VAR>hto : ∀ (i : ℕ), IsOpen (t i)<VAR>hts : ∀ (i : ℕ), SymmetricRel (t i)<GOAL>∀ u ∈ ⋃ x ∈ s, range fun k => ball x (t k), IsOpen u
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : (𝓤 α).IsCountablyGenerated<VAR>inst✝ : SeparableSpace α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>t : ℕ → Set (α × α)<VAR>h_basis : (𝓤 α).HasAntitoneBasis t<VAR>ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets<VAR>hto : ∀ (i : ℕ), IsOpen (t i)<VAR>hts : ∀ (i : ℕ), SymmetricRel (t i)<GOAL>∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ ⋃ x ∈ s, range fun k => ball x (t k), a ∈ v ∧ v ⊆ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α →ₛ ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>f.lintegral (Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α →ₛ ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>∑' (x : { x // x ∈ f.range }) (i : ι), ↑x * (μ i) (↑f ⁻¹' {↑x}) = ∑' (i : ι) (x : { x // x ∈ f.range }), ↑x * (μ i) (↑f ⁻¹' {↑x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : Monoid α<VAR>inst✝² : Unique αˣ<VAR>M : Type u_5<VAR>inst✝¹ : CancelCommMonoidWithZero M<VAR>inst✝ : Unique Mˣ<VAR>p q : M<VAR>pp : Prime p<VAR>qp : Prime q<GOAL>p ∣ q ↔ p = q
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>heI : e ∉ I<GOAL>e ∈ M.closure I ↔ M.Dep (insert e I)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroClass M₀<VAR>f g : ι → M₀<VAR>x : ι<VAR>hfg : x ∈ support fun x => f x * g x<VAR>hg : g x = 0<GOAL>(fun x => f x * g x) x = 0
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>↑univUnitBall.symm 0 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>inst✝ : LinearOrder β<VAR>hf : QuasilinearOn 𝕜 s f<GOAL>MonotoneOn f s ∨ AntitoneOn f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>inst✝ : LinearOrder β<VAR>hf : QuasilinearOn 𝕜 s f<GOAL>∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ segment 𝕜 a b → f c ∈ uIcc (f a) (f b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → β<VAR>inst✝ : LinearOrder β<VAR>hf : QuasilinearOn 𝕜 s f<VAR>a : 𝕜<VAR>ha : a ∈ s<VAR>b : 𝕜<VAR>hb : b ∈ s<VAR>c : 𝕜<VAR>a✝ : c ∈ s<VAR>h : c ∈ segment 𝕜 a b<GOAL>f c ∈ uIcc (f a) (f b)
<VAR>α : Type u_1<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀ : H<VAR>bound✝ : α → ℝ<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ H<VAR>μ : Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x => F x t) (F' t) x₀<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀ : H<VAR>bound✝ : α → ℝ<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ H<VAR>μ : Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x => F x t) (F' t) x₀<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))<VAR>hF_meas : (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧ ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀ : H<VAR>bound✝ : α → ℝ<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ H<VAR>μ : Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>h_lip : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))<VAR>hF_meas : (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧ ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀ : H<VAR>bound✝ : α → ℝ<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ H<VAR>μ : Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>h_lip : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀) ∧ ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))<VAR>hF_meas : (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧ ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))<VAR>H₁ : Integrable F' (μ.restrict (Set.Ioc a b)) ∧ HasFDerivAt (fun x => ∫ (a : ℝ) in Set.Ioc a b, F x a ∂μ) (∫ (a : ℝ) in Set.Ioc a b, F' a ∂μ) x₀<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀