ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<VAR>hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p<VAR>v : (ι → ℝ) → F := u ∘ ⇑e.symm<VAR>hv : ContDiff ℝ 1 v<GOAL>↑c * ∫⁻ (a : E), ↑‖u a‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * (↑c * ∫⁻ (a : E), ↑‖fderiv ℝ u a‖₊ ∂Measure.map (⇑e.symm) volume) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<VAR>hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p<VAR>v : (ι → ℝ) → F := u ∘ ⇑e.symm<VAR>hv : ContDiff ℝ 1 v<VAR>h2v : HasCompactSupport v<GOAL>↑c * ∫⁻ (a : E), ↑‖u a‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * (↑c * ∫⁻ (a : E), ↑‖fderiv ℝ u a‖₊ ∂Measure.map (⇑e.symm) volume) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝¹ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝¹<VAR>this✝ : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<VAR>hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p<VAR>v : (ι → ℝ) → F := u ∘ ⇑e.symm<VAR>hv : ContDiff ℝ 1 v<VAR>h2v : HasCompactSupport v<VAR>this : ∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑(‖↑e.symm‖₊ ^ p) * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂Measure.map (⇑e.symm) volume) ^ p<GOAL>↑c * ∫⁻ (a : E), ↑‖u a‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * (↑c * ∫⁻ (a : E), ↑‖fderiv ℝ u a‖₊ ∂Measure.map (⇑e.symm) volume) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝¹ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝¹<VAR>this✝ : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<VAR>hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p<VAR>v : (ι → ℝ) → F := u ∘ ⇑e.symm<VAR>hv : ContDiff ℝ 1 v<VAR>h2v : HasCompactSupport v<VAR>this : ↑c * ∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * ↑(c ^ p) * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂Measure.map (⇑e.symm) volume) ^ p<GOAL>↑c * ∫⁻ (a : E), ↑‖u a‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * (↑c * ∫⁻ (a : E), ↑‖fderiv ℝ u a‖₊ ∂Measure.map (⇑e.symm) volume) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝¹ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝¹<VAR>this✝ : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<VAR>hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p<VAR>v : (ι → ℝ) → F := u ∘ ⇑e.symm<VAR>hv : ContDiff ℝ 1 v<VAR>h2v : HasCompactSupport v<VAR>this : ↑c * ∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * ↑(c ^ p) * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂Measure.map (⇑e.symm) volume) ^ p<GOAL>↑c * ∫⁻ (a : E), ↑‖u a‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * ↑(c ^ p) * (∫⁻ (a : E), ↑‖fderiv ℝ u a‖₊ ∂Measure.map (⇑e.symm) volume) ^ p
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Iic a = Iic ↑a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>(a \ b) \ a = ⊥
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g g' : G<VAR>h : ∃ d, g' = g + d<GOAL>(x %ᵒᶠ g) g' = 0
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>r : ℚ<GOAL>‖↑r‖ = |↑r|
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>r : ℚ<GOAL>‖↑↑r‖ = |↑r|
<VAR>b : ℝ<GOAL>IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume ↔ 0 < b
<VAR>b : ℝ<VAR>h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume<GOAL>0 < b
<VAR>b : ℝ<VAR>h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume<VAR>hb : b ≤ 0<GOAL>False
<VAR>b : ℝ<VAR>h : IntegrableOn (fun x => rexp (-b * x ^ 2)) (Ioi 0) volume<VAR>hb : b ≤ 0<VAR>this : ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, ↑‖rexp (-b * x ^ 2)‖₊<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>ν : Measure β<VAR>f : β → ℝ≥0∞<VAR>g : α ≃ᵐ β<VAR>hg : MeasurePreserving (⇑g) μ ν<GOAL>∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedRing α<VAR>n : ℕ<GOAL>‖↑(n + 1)‖ ≤ ↑(n + 1) * ‖1‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedRing α<VAR>n : ℕ<GOAL>‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s✝ t r : Set α<VAR>s : ι → Set α<VAR>h : Pairwise (Disjoint on s)<VAR>i : ι<VAR>x : α<VAR>hx : x ∈ s i<VAR>j : ι<VAR>hx' : (fun x => ↑x.snd) ⟨i, ⟨x, hx⟩⟩ ∈ s j<GOAL>⟨i, ⟨x, hx⟩⟩ = ⟨j, ⟨(fun x => ↑x.snd) ⟨i, ⟨x, hx⟩⟩, hx'⟩⟩
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s✝ t r : Set α<VAR>s : ι → Set α<VAR>h : Pairwise (Disjoint on s)<VAR>i : ι<VAR>x : α<VAR>hx : x ∈ s i<VAR>hx' : (fun x => ↑x.snd) ⟨i, ⟨x, hx⟩⟩ ∈ s i<GOAL>⟨i, ⟨x, hx⟩⟩ = ⟨i, ⟨(fun x => ↑x.snd) ⟨i, ⟨x, hx⟩⟩, hx'⟩⟩
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>hg : Supermartingale g ℱ μ<GOAL>Supermartingale (f + g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>hg : Supermartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>μ[(f + g) j|↑ℱ i] ≤ᶠ[ae μ] (f + g) i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>hg : Supermartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>μ[f j|↑ℱ i] + μ[g j|↑ℱ i] ≤ᶠ[ae μ] (f + g) i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>hg : Supermartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>∀ (a : Ω), (μ[f j|↑ℱ i]) a ≤ f i a → (μ[g j|↑ℱ i]) a ≤ g i a → (μ[f j|↑ℱ i] + μ[g j|↑ℱ i]) a ≤ (f + g) i a
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>hg : Supermartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>a✝² : Ω<VAR>a✝¹ : (μ[f j|↑ℱ i]) a✝² ≤ f i a✝²<VAR>a✝ : (μ[g j|↑ℱ i]) a✝² ≤ g i a✝²<GOAL>(μ[f j|↑ℱ i] + μ[g j|↑ℱ i]) a✝² ≤ (f + g) i a✝²
<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>R : Type u_1<VAR>inst✝⁴ : Zero R<VAR>inst✝³ : SMulWithZero R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞<VAR>inst✝ : DecidableEq R<VAR>c : R<GOAL>c • ⊤ = if c = 0 then 0 else ⊤
<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>R : Type u_1<VAR>inst✝⁴ : Zero R<VAR>inst✝³ : SMulWithZero R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞<VAR>inst✝ : DecidableEq R<VAR>c : R<GOAL>(if c • 1 = 0 then 0 else ⊤) = if c = 0 then 0 else ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x : α<GOAL>x ∈ f.support ↔ f x ≠ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : α → β<VAR>s : Set α<VAR>x : α<VAR>h : f =ᶠ[𝓝[s] x] g<VAR>hx : f x = g x<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>h : IsIntegral F α<VAR>x : { x // x ∈ (minpoly F α).aroots K }<GOAL>(aeval ↑x) (minpoly F (adjoin.powerBasis h).gen) = 0
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>h : IsIntegral F α<VAR>x : { x // x ∈ (minpoly F α).aroots K }<GOAL>(aeval ↑x) (minpoly F α) = 0
<VAR>C : Type u_1<VAR>D : Type ?u.40512<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Category.{?u.40520, ?u.40512} D<VAR>K : Coverage C<GOAL>toGrothendieck C K = sInf {J | K ≤ ofGrothendieck C J}
<VAR>C : Type u_1<VAR>D : Type ?u.40512<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Category.{?u.40520, ?u.40512} D<VAR>K : Coverage C<GOAL>toGrothendieck C K ≤ sInf {J | K ≤ ofGrothendieck C J}
<VAR>C : Type u_1<VAR>D : Type ?u.40512<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Category.{?u.40520, ?u.40512} D<VAR>K : Coverage C<GOAL>sInf {J | K ≤ ofGrothendieck C J} ≤ toGrothendieck C K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x y : ℝ<VAR>hxy : x ≤ y<GOAL>stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x y : ℝ<VAR>hxy : x ≤ y<VAR>this : Nonempty { r' // y < ↑r' }<GOAL>stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x y : ℝ<VAR>hxy : x ≤ y<VAR>this : Nonempty { r' // y < ↑r' }<GOAL>⨅ q, f a ↑q ≤ ⨅ q, f a ↑q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x y : ℝ<VAR>hxy : x ≤ y<VAR>this : Nonempty { r' // y < ↑r' }<VAR>r : { q' // y < ↑q' }<GOAL>BddBelow (range fun q => f a ↑q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x y : ℝ<VAR>hxy : x ≤ y<VAR>this : Nonempty { r' // y < ↑r' }<VAR>r : { q' // y < ↑q' }<GOAL>{ q' // x < ↑q' }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x y : ℝ<VAR>hxy : x ≤ y<VAR>this : Nonempty { r' // y < ↑r' }<VAR>r : { q' // y < ↑q' }<GOAL>f a ↑?refine_2 = f a ↑r
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>R₄ : Type u_4<VAR>inst✝¹² : Semiring R₁<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : CommSemiring R₃<VAR>inst✝⁹ : CommSemiring R₄<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₁₄ : R₁ →+* R₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>M₄ : Type u_8<VAR>inst✝⁸ : TopologicalSpace M₁<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : TopologicalSpace M₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : TopologicalSpace M₃<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : TopologicalSpace M₄<VAR>inst✝¹ : AddCommGroup M₄<VAR>inst✝ : TopologicalAddGroup M₄<VAR>f g : M₁ → M₄<VAR>hf : IsCompactOperator f<VAR>hg : IsCompactOperator g<GOAL>IsCompactOperator (f - g)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>R₄ : Type u_4<VAR>inst✝¹² : Semiring R₁<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : CommSemiring R₃<VAR>inst✝⁹ : CommSemiring R₄<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₁₄ : R₁ →+* R₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>M₄ : Type u_8<VAR>inst✝⁸ : TopologicalSpace M₁<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : TopologicalSpace M₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : TopologicalSpace M₃<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : TopologicalSpace M₄<VAR>inst✝¹ : AddCommGroup M₄<VAR>inst✝ : TopologicalAddGroup M₄<VAR>f g : M₁ → M₄<VAR>hf : IsCompactOperator f<VAR>hg : IsCompactOperator g<GOAL>IsCompactOperator (f + -g)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<VAR>n : ℕ<GOAL>take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.121835 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.127286 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂) = pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁵ : Ring k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq P<VAR>inst✝ : DecidableEq V<VAR>s : Finset P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k ↑s = Submodule.span k ↑(Finset.image (fun x => x -ᵥ p) (s.erase p))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<VAR>ts : t ⊆ s<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<VAR>t_closure : closure t = Icc b a<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<VAR>t_closure : closure t = Icc b a<VAR>t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<VAR>t_closure : closure t = Icc b a<VAR>t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y<VAR>t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))<GOAL>HasDerivWithinAt f e (Iic a) a