ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>G : ℝ → ℝ<VAR>G_mble : Measurable G<VAR>G_nn : 0 ≤ G<VAR>g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G<VAR>g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G<VAR>G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>G : ℝ → ℝ<VAR>G_mble : Measurable G<VAR>G_nn : 0 ≤ G<VAR>g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G<VAR>g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G<VAR>G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t<VAR>F : α → ℝ<VAR>F_mble : Measurable F<VAR>F_nn : 0 ≤ F<VAR>f_eq_F : f =ᶠ[ae μ] F<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>G : ℝ → ℝ<VAR>G_mble : Measurable G<VAR>G_nn : 0 ≤ G<VAR>g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G<VAR>g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G<VAR>G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t<VAR>F : α → ℝ<VAR>F_mble : Measurable F<VAR>F_nn : 0 ≤ F<VAR>f_eq_F : f =ᶠ[ae μ] F<VAR>eq₁ : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>G : ℝ → ℝ<VAR>G_mble : Measurable G<VAR>G_nn : 0 ≤ G<VAR>g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G<VAR>g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G<VAR>G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t<VAR>F : α → ℝ<VAR>F_mble : Measurable F<VAR>F_nn : 0 ≤ F<VAR>f_eq_F : f =ᶠ[ae μ] F<VAR>eq₁ : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)<VAR>eq₂ : ∀ᵐ (ω : α) ∂μ, ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..F ω, G t)<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>G : ℝ → ℝ<VAR>G_mble : Measurable G<VAR>G_nn : 0 ≤ G<VAR>g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G<VAR>g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G<VAR>G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t<VAR>F : α → ℝ<VAR>F_mble : Measurable F<VAR>F_nn : 0 ≤ F<VAR>f_eq_F : f =ᶠ[ae μ] F<VAR>eq₁ : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)<VAR>eq₂ : ∀ᵐ (ω : α) ∂μ, ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..F ω, G t)<GOAL>∫⁻ (a : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..F a, G t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
<VAR>α β : Type u<VAR>a : Cardinal.{u}<GOAL>1 ≤ lift.{v, u} a ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a✝ b : α<VAR>inst✝ : LE α<VAR>a : α<GOAL>↑a ≤ ⊥ ↔ ↑a = ⊥
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Subgroup G<GOAL>stabilizer G ↑s = s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Subgroup G<GOAL>∀ (x : G), (∀ (b : G), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>s : Subgroup G<VAR>a : G<VAR>h : ∀ (b : G), a • b ∈ ↑s ↔ b ∈ ↑s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<GOAL>(∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<VAR>hp_pos : 0 < p<GOAL>(∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<VAR>hp_pos : 0 < p<GOAL>∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<VAR>hp_pos : 0 < p<VAR>h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop<GOAL>∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<VAR>hp_pos : 0 < p<VAR>h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop<GOAL>∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) atTop ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<VAR>hp_pos : 0 < p<VAR>h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop<VAR>h_liminf_pow : ∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) atTop ^ p ∂μ = ∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p) atTop ∂μ<GOAL>∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) atTop ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<VAR>hp_pos : 0 < p<VAR>h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop<VAR>h_liminf_pow : ∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) atTop ^ p ∂μ = ∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p) atTop ∂μ<GOAL>∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p) atTop ∂μ ≤ (∑' (i : ℕ), B i) ^ p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<VAR>hp_pos : 0 < p<VAR>h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop<VAR>h_liminf_pow : ∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) atTop ^ p ∂μ = ∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p) atTop ∂μ<GOAL>∀ (n : ℕ), AEMeasurable (fun a => (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<VAR>hp_pos : 0 < p<VAR>h_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n => ∑ i ∈ Finset.range (n + 1), g i) atTop<VAR>h_liminf_pow : ∫⁻ (a : α), liminf (fun n => ∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) atTop ^ p ∂μ = ∫⁻ (a : α), liminf (fun n => (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p) atTop ∂μ<GOAL>liminf (fun n => ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) atTop ≤ (∑' (i : ℕ), B i) ^ p
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g : α✝ → β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>m m₂ : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Zero E<VAR>s : Set α<VAR>f : α → E<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)<VAR>hf : StronglyMeasurable f<VAR>hf_zero : ∀ x ∉ s, f x = 0<GOAL>StronglyMeasurable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g : α✝ → β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>m m₂ : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Zero E<VAR>s : Set α<VAR>f : α → E<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)<VAR>hf : StronglyMeasurable f<VAR>hf_zero : ∀ x ∉ s, f x = 0<VAR>hs_m₂ : MeasurableSet s<GOAL>StronglyMeasurable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g : α✝ → β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>m m₂ : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Zero E<VAR>s : Set α<VAR>f : α → E<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)<VAR>hf : StronglyMeasurable f<VAR>hf_zero : ∀ x ∉ s, f x = 0<VAR>hs_m₂ : MeasurableSet s<VAR>g_seq_s : ℕ → α →ₛ E<VAR>hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))<VAR>hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), ↑(g_seq_s n) x = 0<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>a b c d y : α<VAR>hya : a ≤ y<VAR>hyb : y ≤ b<VAR>z : α<VAR>hzc : c ≤ z<VAR>hzd : z ≤ d<GOAL>(fun x x_1 => x * x_1) y z ∈ Icc (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>h : (node size✝ l x r).Valid<GOAL>(node size✝ l x r).eraseMin.Valid
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>h : (node size✝ l x r).Valid<GOAL>(l.node' x r).eraseMin.Valid
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<VAR>d : DiscreteQuotient X<VAR>x✝ : Set X<GOAL>x✝ ∈ (((image fun t => t.carrier) ∘ Finset.toSet) ∘ finsetClopens X) d ↔ x✝ ∈ match d with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<VAR>d : DiscreteQuotient X<VAR>x✝ : Set X<GOAL>(∃ a, d.proj ⁻¹' {a} = x✝) ↔ ∃ y, x✝ = {x | Setoid.r x y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>IsPiSystem (⋃ a, {Iio ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>⋃ a, {Iio ↑a} = Iio '' (Rat.cast '' univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>x : Set ℝ<GOAL>x ∈ ⋃ a, {Iio ↑a} ↔ x ∈ Iio '' (Rat.cast '' univ)
<GOAL>comap re (comap Real.exp atTop) = comap re atTop
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n : ℕ<VAR>inst✝ : Fintype α<VAR>hn : n ≠ 0<GOAL>↑(univ ^ n) = ↑univ
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<GOAL>∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<GOAL>f i = ∏ x ∈ s ∩ {i}, f x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).j = E.j
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>↑C.u ^ 12 * ↑E.Δ'⁻¹ * (↑C.u⁻¹ ^ 4 * E.c₄) ^ 3 = E.j
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<VAR>hu : (↑C.u * ↑C.u⁻¹) ^ 12 = 1<GOAL>↑C.u ^ 12 * ↑E.Δ'⁻¹ * (↑C.u⁻¹ ^ 4 * E.c₄) ^ 3 = E.j
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : Module R M<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Module S N<VAR>inst✝⁹ : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝⁸ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝⁷ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>M' : Submodule R M<VAR>P : Type w<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : Module R P<VAR>Q : Type w'<VAR>inst✝⁴ : AddCommGroup Q<VAR>inst✝³ : Module R Q<VAR>inst✝² : Module S Q<VAR>inst✝¹ : IsScalarTower R S Q<VAR>f' : P →ₗ[R] Q<VAR>inst✝ : IsLocalizedModule p f'<VAR>g : M →ₗ[R] P<VAR>x✝ : N<GOAL>x✝ ∈ ker ((IsLocalizedModule.map p f f') g) ↔ x✝ ∈ Submodule.restrictScalars R (Submodule.localized' S p f (ker g))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>W_ (ZMod (p ^ (n + 1))) (n + 1) = (expand p) (W_ (ZMod (p ^ (n + 1))) n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>∑ i ∈ range (n + 1 + 1), C (↑p ^ i) * X i ^ p ^ (n + 1 - i) = (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>∀ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = (expand p) (C (↑p ^ x) * X x ^ p ^ (n - x))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>n k : ℕ<VAR>hk : k ∈ range (n + 1)<GOAL>C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = (expand p) (C (↑p ^ k) * X k ^ p ^ (n - k))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>n k : ℕ<VAR>hk : k ∈ range (n + 1)<GOAL>C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = (algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1))))) (↑p ^ k) * X k ^ p ^ (n - k + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>n k : ℕ<VAR>hk : k ∈ range (n + 1)<GOAL>n + 1 - k = n - k + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>n k : ℕ<VAR>hk : k < n + 1<GOAL>n + 1 - k = n - k + 1
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<GOAL>(X.prodIsoProd Y).inv ≫ prod.fst = prodFst
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>f : R[X]<VAR>inst✝¹ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : eval₂ i a f = 0<VAR>inst✝ : Algebra R S<VAR>ϕ : AdjoinRoot f →ₐ[R] S<GOAL>(aeval (ϕ (root f))) f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>f : R[X]<VAR>inst✝¹ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h✝ : eval₂ i a f = 0<VAR>inst✝ : Algebra R S<VAR>ϕ : AdjoinRoot f →ₐ[R] S<VAR>h : ϕ.comp (of f) = algebraMap R S<GOAL>(aeval (ϕ (root f))) f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>f : R[X]<VAR>inst✝¹ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h✝ : eval₂ i a f = 0<VAR>inst✝ : Algebra R S<VAR>ϕ : AdjoinRoot f →ₐ[R] S<VAR>h : ϕ.comp (of f) = algebraMap R S<GOAL>eval₂ (ϕ.comp (of f)) (ϕ (root f)) f = eval₂ (ϕ.comp (of f)) (ϕ.toRingHom (root f)) f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M Nᵐᵒᵖ<VAR>inst✝ : MonoidHomClass F M Nᵐᵒᵖ<VAR>f : F<VAR>l : List M<GOAL>MulOpposite.unop (f l.prod) = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>(H ⊓ K).relindex H = K.relindex H
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Group N<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<VAR>F : N ⋊[φ] G →* H<VAR>x✝¹ : G<VAR>x✝ : N<GOAL>((F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝¹))) x✝ = ((MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝¹))).comp (F.comp inl)) x✝
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Group N<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<VAR>F : N ⋊[φ] G →* H<GOAL>F = lift (F.comp inl) (F.comp inr) ⋯
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Group N<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<VAR>F : N ⋊[φ] G →* H<GOAL>∀ (x : N ⋊[φ] G), F x = (lift (F.comp inl) (F.comp inr) ⋯) x
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t : Set X<VAR>x : X<VAR>h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous f<VAR>u : Set X<VAR>hu : ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)<GOAL>IsOpen u
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t : Set X<VAR>x : X<VAR>u : Set X<VAR>hu : ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)<VAR>h : ∀ (f : X → Prop), (∀ s ∈ S, IsOpen {x | s.restrict f x}) → IsOpen {x | f x}<GOAL>IsOpen u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g✝ : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : T2Space β<VAR>h : ⋃₀ 𝔖 = univ<VAR>f g : α →ᵤ[𝔖] β<VAR>hfg : f ≠ g<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g✝ : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : T2Space β<VAR>h : ⋃₀ 𝔖 = univ<VAR>f g : α →ᵤ[𝔖] β<VAR>hfg : f ≠ g<VAR>x : α<VAR>hx : ¬f x = g x<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s✝ s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g✝ : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : T2Space β<VAR>h : ⋃₀ 𝔖 = univ<VAR>f g : α →ᵤ[𝔖] β<VAR>hfg : f ≠ g<VAR>x : α<VAR>hx : ¬f x = g x<VAR>s : Set α<VAR>hs : s ∈ 𝔖<VAR>hxs : x ∈ s<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
<VAR>α : Type u_1<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (fun x => x + c) (Ioo a b) = Ioo (a + c) (b + c)
<VAR>α : Type u_1<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(normAtPlace w) (-x) = (normAtPlace w) x
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(if hw : w.IsReal then ‖(-x).1 ⟨w, hw⟩‖ else ‖(-x).2 ⟨w, ⋯⟩‖) = if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>a : α<VAR>ha : ∀ (x : α), x ≠ a → f x = 1<GOAL>∏ᶠ (x : α), f x = f a