ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<GOAL>((addBottom L).nth n).2 = L.nth n
<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 Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>(P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<GOAL>UniformConvexOn s φ (-f)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>-(a • (-f) x + b • (-f) y - a * b * φ ‖x - y‖) ≤ -(-f) (a • x + b • y)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β✝ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β✝<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>S : Set (Set β)<VAR>hS : ∀ s ∈ S, IsOpen s<GOAL>IsOpen (⋂₀ S)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β✝ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β✝<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>S : Set (Set β)<VAR>hS : ∀ s ∈ S, IsOpen s<GOAL>IsOpen (⋂ t ∈ S, f ⁻¹' t)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>U : Opens X<VAR>hU : Nonempty ↥U<VAR>y : Y<VAR>hy : y ∈ (e.subtypeRestr hU).target<GOAL>↑e.symm y = (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>U : Opens X<VAR>hU : Nonempty ↥U<VAR>y : Y<VAR>hy : y ∈ (e.subtypeRestr hU).target<GOAL>↑e ((Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y) = y
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>U : Opens X<VAR>hU : Nonempty ↥U<VAR>y : Y<VAR>hy : y ∈ (e.subtypeRestr hU).target<GOAL>(Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source
<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>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : ¬MDifferentiableWithinAt I I' f s x<GOAL>mfderivWithin I I' f s x = 0
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝⁸ : CommRing S✝<VAR>S : Type u_3<VAR>T : Type u_4<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : CommRing T<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsFractionRing R T<VAR>hM : M ≤ nonZeroDivisors R<GOAL>IsFractionRing S T
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝⁸ : CommRing S✝<VAR>S : Type u_3<VAR>T : Type u_4<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : CommRing T<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsFractionRing R T<VAR>hM : M ≤ nonZeroDivisors R<VAR>this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T<GOAL>IsFractionRing S T
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝⁸ : CommRing S✝<VAR>S : Type u_3<VAR>T : Type u_4<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : CommRing T<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsFractionRing R T<VAR>hM : M ≤ nonZeroDivisors R<VAR>this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T<GOAL>Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝⁸ : CommRing S✝<VAR>S : Type u_3<VAR>T : Type u_4<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : CommRing T<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsFractionRing R T<VAR>hM : M ≤ nonZeroDivisors R<VAR>this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T<GOAL>∀ (x : ↥(nonZeroDivisors S)), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>|edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>edgeDensity r s₁ t₁ - edgeDensity r s₂ t₂ ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>edgeDensity (fun x y => ¬r x y) s₂ t₂ - edgeDensity (fun x y => ¬r x y) s₁ t₁ ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x y : (i : ι) → A i<GOAL>(mul ((tprod R) x)) ((tprod R) y) = (tprod R) (x * y)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x✝¹ x✝ : α<VAR>H : of x✝¹ = of x✝<GOAL>x✝¹ = x✝
<VAR>α : Type u<VAR>L L₁✝ L₂ L₃ L₄ : List (α × Bool)<VAR>x✝¹ x✝ : α<VAR>H : of x✝¹ = of x✝<VAR>L₁ : List (α × Bool)<VAR>hx : Red [(x✝¹, true)] L₁<VAR>hy : Red [(x✝, true)] L₁<GOAL>x✝¹ = x✝
<VAR>α : Type u<VAR>L L₁✝ L₂ L₃ L₄ : List (α × Bool)<VAR>x✝¹ x✝ : α<VAR>H : of x✝¹ = of x✝<VAR>L₁ : List (α × Bool)<VAR>hx : L₁ = [(x✝¹, true)]<VAR>hy : L₁ = [(x✝, true)]<GOAL>x✝¹ = x✝
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<VAR>h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<VAR>h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<VAR>h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f' i a) atTop (𝓝 (F' a))<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<VAR>h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a<GOAL>AEMeasurable 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✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<VAR>h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a<GOAL>∫⁻ (a : α), F' a ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<VAR>h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f' i a) atTop (𝓝 (F' a))<VAR>a : α<VAR>ha : Tendsto (fun i => f' i a) atTop (𝓝 (F' a))<VAR>ha_mono : Monotone fun i => f i a<VAR>ha_bound : ∀ (i : ℕ), f i a ≤ F a<GOAL>Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<VAR>h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f' i a) atTop (𝓝 (F' a))<VAR>a : α<VAR>ha : Tendsto (fun i => f' i a) atTop (𝓝 (F' a))<VAR>ha_mono : Monotone fun i => f i a<VAR>ha_bound : ∀ (i : ℕ), f i a ≤ F a<VAR>h1 : (fun i => f i a) = fun i => (f' i a).toReal + f 0 a<VAR>h2 : F a = (F' a).toReal + f 0 a<GOAL>Tendsto (fun i => (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF_int : Integrable F μ<VAR>hf_tendsto : Tendsto (fun i => ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>f' : ℕ → α → ℝ≥0∞ := fun n a => ENNReal.ofReal (f n a - f 0 a)<VAR>F' : α → ℝ≥0∞ := fun a => ENNReal.ofReal (F a - f 0 a)<VAR>hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)<VAR>h_tendsto : Tendsto (fun i => ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))<VAR>h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f' i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a<VAR>h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f' i a) atTop (𝓝 (F' a))<VAR>a : α<VAR>ha : Tendsto (fun i => f' i a) atTop (𝓝 (F' a))<VAR>ha_mono : Monotone fun i => f i a<VAR>ha_bound : ∀ (i : ℕ), f i a ≤ F a<VAR>h1 : (fun i => f i a) = fun i => (f' i a).toReal + f 0 a<VAR>h2 : F a = (F' a).toReal + f 0 a<GOAL>Tendsto (fun i => (f' i a).toReal) atTop (𝓝 (F' a).toReal)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(p * X ^ n).degree = p.degree + ↑n
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>nd₁ : l₁.NodupKeys<VAR>nd₂ : l₂.NodupKeys<GOAL>(l₁.kunion l₂).NodupKeys