ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>x y : ℕ → α<VAR>n : ℕ<VAR>ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n<VAR>h : ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m<GOAL>res x (n + 1) = res y (n + 1)
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>x y : ℕ → α<VAR>n : ℕ<VAR>ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n<VAR>h : ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m<GOAL>x n = y n ∧ res x n = res y n
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>x y : ℕ → α<VAR>n : ℕ<VAR>ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n<VAR>h : ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m<VAR>m : ℕ<VAR>hm : m < n<GOAL>x m = y m
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : PartialOrder γ<VAR>j i : γ<VAR>hj : IsLUB (Iio i) j<GOAL>j = i ∨ Iio i = Iic j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : PartialOrder γ<VAR>j i : γ<VAR>hj : IsLUB (Iio i) j<VAR>hj_eq_i : j = i<GOAL>j = i ∨ Iio i = Iic j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : PartialOrder γ<VAR>j i : γ<VAR>hj : IsLUB (Iio i) j<VAR>hj_lt_i : j < i<GOAL>j = i ∨ Iio i = Iic j
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>IsOpen (id '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t s : Multiset α<VAR>a : α<GOAL>s.toFinset = {a} ↔ card s ≠ 0 ∧ s = card s • {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t s : Multiset α<VAR>a : α<VAR>H : s.toFinset = {a}<VAR>h : card s = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t s : Multiset α<VAR>a : α<VAR>H : s.toFinset = {a}<VAR>x : α<GOAL>count x s = count x (card s • {a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t s : Multiset α<VAR>a : α<VAR>H : card s ≠ 0 ∧ s = card s • {a}<GOAL>s.toFinset = {a}
<VAR>G : Type w<VAR>H : Type x<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>α : Type u_1<VAR>l : Filter α<VAR>x : G<VAR>u : α → G<VAR>A : Tendsto (fun x_1 => x) l (𝓝 x)<VAR>h : Tendsto (fun x_1 => u x_1 / x) l (𝓝 1)<GOAL>Tendsto u l (𝓝 x)
<VAR>G : Type w<VAR>H : Type x<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>α : Type u_1<VAR>l : Filter α<VAR>x : G<VAR>u : α → G<VAR>A : Tendsto (fun x_1 => x) l (𝓝 x)<VAR>h : Tendsto u l (𝓝 x)<GOAL>Tendsto (fun x_1 => u x_1 / x) l (𝓝 1)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>x y : FreeGroup α<GOAL>(x * y).norm = (mk (x.toWord ++ y.toWord)).norm
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>σ : Perm α<VAR>h0 : n.Coprime (Fintype.card α)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x : α<GOAL>closure {σ, swap x ((σ ^ n) x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>σ : Perm α<VAR>h0 : n.Coprime (orderOf σ)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x : α<GOAL>closure {σ, swap x ((σ ^ n) x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>σ : Perm α<VAR>h0 : n.Coprime (orderOf σ)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x : α<VAR>m : ℕ<VAR>hm : (σ ^ n) ^ m = σ<GOAL>closure {σ, swap x ((σ ^ n) x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>σ : Perm α<VAR>h0 : n.Coprime (orderOf σ)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x : α<VAR>m : ℕ<VAR>hm : (σ ^ n) ^ m = σ<VAR>h2' : (σ ^ n).support = ⊤<GOAL>closure {σ, swap x ((σ ^ n) x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>σ : Perm α<VAR>h0 : n.Coprime (orderOf σ)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x : α<VAR>m : ℕ<VAR>hm : (σ ^ n) ^ m = σ<VAR>h2' : (σ ^ n).support = ⊤<VAR>h1' : ((σ ^ n) ^ ↑m).IsCycle<GOAL>closure {σ, swap x ((σ ^ n) x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>σ : Perm α<VAR>h0 : n.Coprime (orderOf σ)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x : α<VAR>m : ℕ<VAR>hm : (σ ^ n) ^ m = σ<VAR>h2' : (σ ^ n).support = ⊤<VAR>h1' : (σ ^ n).IsCycle<GOAL>closure {σ, swap x ((σ ^ n) x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>σ : Perm α<VAR>h0 : n.Coprime (orderOf σ)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = univ<VAR>x : α<VAR>m : ℕ<VAR>hm : (σ ^ n) ^ m = σ<VAR>h2' : (σ ^ n).support = ⊤<VAR>h1' : (σ ^ n).IsCycle<GOAL>σ ^ n ∈ ↑(closure {σ, swap x ((σ ^ n) x)}) ∧ {swap x ((σ ^ n) x)} ⊆ ↑(closure {σ, swap x ((σ ^ n) x)})
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : BooleanAlgebra α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b c : α<GOAL>a ∈ sᶜˢ ↔ aᶜ ∈ s
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>s : Set α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>hs : s.Finite<GOAL>(↑(lowerClosure s)).Finite
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>s : Set α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>hs : s.Finite<GOAL>(⋃ a ∈ s, Iic a).Finite
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a✝ : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b✝ a b : k<VAR>ha : a ≠ 0<GOAL>fract (b / a) * a + ⌊b / a⌋ • a = b
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.dblU P = -3 * P x ^ 2
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.a₁ * P y * 0 - (3 * P x ^ 2 + 2 * W'.a₂ * P x * 0 ^ 2 + W'.a₄ * 0 ^ 4) = -3 * P x ^ 2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>f : α →ₛ ℝ<VAR>hf : Integrable (↑f) μ<VAR>h_pos : 0 ≤ᶠ[ae μ] ↑f<GOAL>integral μ f = (∫⁻ (a : α), ENNReal.ofReal (↑f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>f : α →ₛ ℝ<VAR>hf : Integrable (↑f) μ<VAR>h_pos : 0 ≤ᶠ[ae μ] ↑f<VAR>this : ↑f =ᶠ[ae μ] ↑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)<GOAL>integral μ f = (∫⁻ (a : α), ENNReal.ofReal (↑f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>f : α →ₛ ℝ<VAR>hf : Integrable (↑f) μ<VAR>h_pos : 0 ≤ᶠ[ae μ] ↑f<VAR>this : ↑f =ᶠ[ae μ] ↑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)<GOAL>integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>f : α →ₛ ℝ<VAR>hf : Integrable (↑f) μ<VAR>h_pos : 0 ≤ᶠ[ae μ] ↑f<VAR>this : ↑f =ᶠ[ae μ] ↑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)<GOAL>ENNReal.ofReal 0 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>f : α →ₛ ℝ<VAR>hf : Integrable (↑f) μ<VAR>h_pos : 0 ≤ᶠ[ae μ] ↑f<VAR>this : ↑f =ᶠ[ae μ] ↑(map (ENNReal.toReal ∘ ENNReal.ofReal) f)<GOAL>∀ (b : ℝ), ENNReal.ofReal b ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>ι : Type u_3<VAR>f : ι → Set α<VAR>inst✝ : Finite ι<VAR>hf : ∀ (i : ι), NoetherianSpace ↑(f i)<GOAL>NoetherianSpace ↑(⋃ i, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>ι : Type u_3<VAR>f : ι → Set α<VAR>inst✝ : Finite ι<VAR>hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t<GOAL>∀ t ⊆ ⋃ i, f i, IsCompact t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>ι : Type u_3<VAR>f : ι → Set α<VAR>inst✝ : Finite ι<VAR>hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t<VAR>t : Set α<VAR>ht : t ⊆ ⋃ i, f i<GOAL>IsCompact t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>ι : Type u_3<VAR>f : ι → Set α<VAR>inst✝ : Finite ι<VAR>hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t<VAR>t : Set α<VAR>ht : t ⊆ ⋃ i, f i<GOAL>IsCompact (⋃ i, t ∩ f i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝³ : (i : ι) → Module R (M₁ i)<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>h : m i = 0<GOAL>f m = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>S : Sieve X<VAR>f : Y ⟶ X<GOAL>⊤.Covers S f
<VAR>α : Type u_1<VAR>inst✝² : Bornology α<VAR>s t : Set α<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Nonempty α<GOAL>IsBounded s ↔ BddBelow s ∧ BddAbove s
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : SeminormedCommRing S<VAR>inst✝¹² : SeminormedRing R<VAR>inst✝¹¹ : SeminormedAddCommGroup M<VAR>inst✝¹⁰ : Algebra S R<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module Rᵐᵒᵖ M<VAR>inst✝⁶ : BoundedSMul S R<VAR>inst✝⁵ : BoundedSMul S M<VAR>inst✝⁴ : BoundedSMul R M<VAR>inst✝³ : BoundedSMul Rᵐᵒᵖ M<VAR>inst✝² : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S Rᵐᵒᵖ M<VAR>x : tsze R M<GOAL>↑‖x‖₊ = ↑(‖x.fst‖₊ + ‖x.snd‖₊)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hut' : UnifTight (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hut' : UnifTight (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hut' : UnifTight (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)<VAR>hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hut' : UnifTight (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)<VAR>hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯<VAR>hg'' : Memℒp (AEStronglyMeasurable.mk g ⋯) p μ<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hut' : UnifTight (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ<VAR>hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)<VAR>hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯<VAR>hg'' : Memℒp (AEStronglyMeasurable.mk g ⋯) p μ<VAR>haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)<VAR>hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯<VAR>hg'' : Memℒp (AEStronglyMeasurable.mk g ⋯) p μ<VAR>haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))<VAR>f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable f' p μ<VAR>hut' : UnifTight f' p μ<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable f' p μ<VAR>hut' : UnifTight f' p μ<VAR>g' : α → β := AEStronglyMeasurable.mk g ⋯<VAR>hg : StronglyMeasurable g'<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hg'' : Memℒp g' p μ<VAR>haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable f' p μ<VAR>hut' : UnifTight f' p μ<VAR>g' : α → β := AEStronglyMeasurable.mk g ⋯<VAR>hg : StronglyMeasurable g'<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hg'' : Memℒp g' p μ<VAR>haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))<VAR>haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable f' p μ<VAR>hut' : UnifTight f' p μ<VAR>g' : α → β := AEStronglyMeasurable.mk g ⋯<VAR>hg : StronglyMeasurable g'<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hg'' : Memℒp g' p μ<VAR>haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))<VAR>haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'<VAR>hsnfg : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)