ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>c : Set (Lifts F E K)<VAR>hc✝ : IsChain (fun x x_1 => x ≤ x_1) c<VAR>t : ↑(insert ⊥ c) → IntermediateField F E := fun i => (↑i).carrier<VAR>t' : ↑(insert ⊥ c) → Subalgebra F E := fun i => (t i).toSubalgebra<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) (insert ⊥ c)<VAR>dir : Directed (fun x x_1 => x ≤ x_1) t<GOAL>∃ ub, ∀ a ∈ c, a ≤ ub
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>c : Set (Lifts F E K)<VAR>hc✝ : IsChain (fun x x_1 => x ≤ x_1) c<VAR>t : ↑(insert ⊥ c) → IntermediateField F E := fun i => (↑i).carrier<VAR>t' : ↑(insert ⊥ c) → Subalgebra F E := fun i => (t i).toSubalgebra<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) (insert ⊥ c)<VAR>dir : Directed (fun x x_1 => x ≤ x_1) t<VAR>i j : ↑(insert ⊥ c)<VAR>h : t' i ≤ t' j<GOAL>(fun i => (↑i).emb) i = ((fun i => (↑i).emb) j).comp (Subalgebra.inclusion h)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>c : Set (Lifts F E K)<VAR>hc✝ : IsChain (fun x x_1 => x ≤ x_1) c<VAR>t : ↑(insert ⊥ c) → IntermediateField F E := fun i => (↑i).carrier<VAR>t' : ↑(insert ⊥ c) → Subalgebra F E := fun i => (t i).toSubalgebra<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) (insert ⊥ c)<VAR>dir : Directed (fun x x_1 => x ≤ x_1) t<VAR>L : Lifts F E K<VAR>hL✝ : L ∈ c<VAR>hL : L ∈ insert ⊥ c<VAR>x : ↥L.carrier<GOAL>{ carrier := iSup t, emb := (Subalgebra.iSupLift t' dir (fun i => (↑i).emb) ⋯ (iSup t') ⋯).comp ↑((iSup t).equivOfEq (⨆ i, (t i).toSubalgebra) ⋯) }.emb ((inclusion ⋯) x) = L.emb x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<GOAL>MonotoneOn (dist x) (Ici x)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁴ : CanonicallyOrderedCommSemiring α<VAR>a✝ b✝ c : α<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a - 1) * b = a * b - b
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>H : Function.Surjective ⇑f<VAR>x : S'<GOAL>∃ a, (IsLocalization.map S' f ⋯) a = x
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>H : Function.Surjective ⇑f<VAR>x : S<VAR>s : R<VAR>hs : s ∈ ↑M<GOAL>∃ a, (IsLocalization.map S' f ⋯) a = IsLocalization.mk' S' x ⟨f s, ⋯⟩
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>H : Function.Surjective ⇑f<VAR>s : R<VAR>hs : s ∈ ↑M<VAR>y : R<GOAL>∃ a, (IsLocalization.map S' f ⋯) a = IsLocalization.mk' S' (f y) ⟨f s, ⋯⟩
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>H : Function.Surjective ⇑f<VAR>s : R<VAR>hs : s ∈ ↑M<VAR>y : R<GOAL>(IsLocalization.map S' f ⋯) (IsLocalization.mk' R' y ⟨s, hs⟩) = IsLocalization.mk' S' (f y) ⟨f s, ⋯⟩
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>wittZero p n = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>(map (Int.castRingHom ℚ)) (wittZero p n) = (map (Int.castRingHom ℚ)) 0
<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>f : ℝ → E<VAR>a b : ℝ<VAR>f' g : ℝ → E<VAR>fdiff : DifferentiableOn ℝ f (Icc a b)<VAR>gdiff : DifferentiableOn ℝ g (Icc a b)<VAR>hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)<VAR>hi : f a = g a<GOAL>∀ y ∈ Icc a b, f y = g y
<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>f : ℝ → E<VAR>a b : ℝ<VAR>f' g : ℝ → E<VAR>fdiff : DifferentiableOn ℝ f (Icc a b)<VAR>gdiff : DifferentiableOn ℝ g (Icc a b)<VAR>hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)<VAR>hi : f a = g a<VAR>A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y<GOAL>∀ y ∈ Icc a b, f y = g y
<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>f : ℝ → E<VAR>a b : ℝ<VAR>f' g : ℝ → E<VAR>fdiff : DifferentiableOn ℝ f (Icc a b)<VAR>gdiff : DifferentiableOn ℝ g (Icc a b)<VAR>hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)<VAR>hi : f a = g a<VAR>A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y<VAR>B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y<GOAL>∀ y ∈ Icc a b, f y = g y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>x : K<VAR>hx : x ≠ 0<GOAL>spanSingleton R₁⁰ x / spanSingleton R₁⁰ x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a b c : Associates α<VAR>ha : a ≠ 0<VAR>d : Associates α<VAR>hd : a * c = a * b * d<GOAL>a * c = a * (b * d)
<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>inst✝²⁶ : SmoothManifoldWithCorners I 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>inst✝²⁰ : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>f✝ f₁ : M → M'<VAR>s✝ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : E → E'<VAR>s : Set E<GOAL>∀ (a : E), a ∈ s → ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s a ↔ a ∈ s → ContDiffWithinAt 𝕜 n f s a
<VAR>z y x : ℝ<VAR>n : ℕ<GOAL>(fun x => cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n
<VAR>z y x : ℝ<GOAL>(fun x => cexp x - ∑ i ∈ Finset.range 0, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ 0
<VAR>z y x : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(fun x => cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>hf : FinStronglyMeasurable f μ<GOAL>FinStronglyMeasurable (-f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>hf : FinStronglyMeasurable f μ<VAR>n : ℕ<GOAL>μ (support ↑((fun n => -hf.approx n) n)) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>hf : FinStronglyMeasurable f μ<VAR>n : ℕ<GOAL>μ (support fun x => -↑(hf.approx n) x) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>hf : FinStronglyMeasurable f μ<VAR>n : ℕ<GOAL>μ (support ↑(hf.approx n)) < ⊤
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>n m : ℕ<GOAL>((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)
<VAR>n b : ℕ<VAR>hb : 2 ≤ b<VAR>hn : 0 < n<GOAL>b.digits n = n % b :: b.digits (n / b)
<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>f : E → F<VAR>f' : E →L[ℝ] F<VAR>x : E<VAR>L : Filter E<GOAL>Tendsto (fun x' => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0) ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)
<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>f : E → F<VAR>f' : E →L[ℝ] F<VAR>x : E<VAR>L : Filter E<GOAL>Tendsto (fun e => ‖‖e - x‖⁻¹ • (f e - f x - f' (e - x)) - 0‖) L (𝓝 0) ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)
<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>f : E → F<VAR>f' : E →L[ℝ] F<VAR>x : E<VAR>L : Filter E<VAR>x' : E<GOAL>‖‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x)) - 0‖ = ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B A : Matrix n n α<GOAL>IsUnit A⁻¹.det ↔ IsUnit A.det
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hF_meas : AEMeasurable 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>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hF_meas : AEMeasurable 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>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>this : ∀ (n : ℕ), ∃ g, Measurable g ∧ g ≤ f n ∧ ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g a ∂μ<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hF_meas : AEMeasurable 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>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>g : ℕ → α → ℝ≥0∞<VAR>gmeas : ∀ (n : ℕ), Measurable (g n)<VAR>gf : ∀ (n : ℕ), g n ≤ f n<VAR>hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>g' : ℕ → α → ℝ≥0∞ := fun t => Nat.rec (motive := fun x => α → ℝ≥0∞) (g 0) (fun n I x => max (g (n + 1) x) (I x)) t<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hF_meas : AEMeasurable 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>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>g : ℕ → α → ℝ≥0∞<VAR>gmeas : ∀ (n : ℕ), Measurable (g n)<VAR>gf : ∀ (n : ℕ), g n ≤ f n<VAR>hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>g' : ℕ → α → ℝ≥0∞ := fun t => Nat.rec (motive := fun x => α → ℝ≥0∞) (g 0) (fun n I x => max (g (n + 1) x) (I x)) t<VAR>M : ∀ (n : ℕ), Measurable (g' n)<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hF_meas : AEMeasurable 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>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>g : ℕ → α → ℝ≥0∞<VAR>gmeas : ∀ (n : ℕ), Measurable (g n)<VAR>gf : ∀ (n : ℕ), g n ≤ f n<VAR>hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>g' : ℕ → α → ℝ≥0∞ := fun t => Nat.rec (motive := fun x => α → ℝ≥0∞) (g 0) (fun n I x => max (g (n + 1) x) (I x)) t<VAR>M : ∀ (n : ℕ), Measurable (g' n)<VAR>I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hF_meas : AEMeasurable 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>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>g : ℕ → α → ℝ≥0∞<VAR>gmeas : ∀ (n : ℕ), Measurable (g n)<VAR>gf : ∀ (n : ℕ), g n ≤ f n<VAR>hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>g' : ℕ → α → ℝ≥0∞ := fun t => Nat.rec (motive := fun x => α → ℝ≥0∞) (g 0) (fun n I x => max (g (n + 1) x) (I x)) t<VAR>M : ∀ (n : ℕ), Measurable (g' n)<VAR>I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x<VAR>I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hF_meas : AEMeasurable 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>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>g : ℕ → α → ℝ≥0∞<VAR>gmeas : ∀ (n : ℕ), Measurable (g n)<VAR>gf : ∀ (n : ℕ), g n ≤ f n<VAR>hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>g' : ℕ → α → ℝ≥0∞ := fun t => Nat.rec (motive := fun x => α → ℝ≥0∞) (g 0) (fun n I x => max (g (n + 1) x) (I x)) t<VAR>M : ∀ (n : ℕ), Measurable (g' n)<VAR>I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x<VAR>I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x<VAR>Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ<VAR>this : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => g' i a) atTop (𝓝 (F a))<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : Measure α<VAR>hF_meas : AEMeasurable 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>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<VAR>g : ℕ → α → ℝ≥0∞<VAR>gmeas : ∀ (n : ℕ), Measurable (g n)<VAR>gf : ∀ (n : ℕ), g n ≤ f n<VAR>hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ<VAR>g' : ℕ → α → ℝ≥0∞ := fun t => Nat.rec (motive := fun x => α → ℝ≥0∞) (g 0) (fun n I x => max (g (n + 1) x) (I x)) t<VAR>M : ∀ (n : ℕ), Measurable (g' n)<VAR>I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x<VAR>I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x<VAR>Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ<VAR>this : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => g' i a) atTop (𝓝 (F a))<VAR>x : α<VAR>hx : Tendsto (fun i => g' i x) atTop (𝓝 (F x))<VAR>h'x : ∀ (n : ℕ), g' n x ≤ f n x<VAR>h''x : ∀ (i : ℕ), f i x ≤ F x<GOAL>Tendsto (fun i => f i x) atTop (𝓝 (F x))
<VAR>s n step : Nat<GOAL>range' s n step = [] ↔ n = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>w₁ w₂ : ι → ℝ<VAR>p : ι → P<VAR>h₁ : ∑ i ∈ s, w₁ i = 1<VAR>h₂ : ∑ i ∈ s, w₂ i = 1<GOAL>dist ((Finset.affineCombination ℝ s p) w₁) ((Finset.affineCombination ℝ s p) w₂) * dist ((Finset.affineCombination ℝ s p) w₁) ((Finset.affineCombination ℝ s p) w₂) = (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>w₁ w₂ : ι → ℝ<VAR>p : ι → P<VAR>h₁ : ∑ i ∈ s, w₁ i = 1<VAR>h₂ : ∑ i ∈ s, w₂ i = 1<GOAL>RCLike.re ⟪(s.weightedVSub p) (w₁ - w₂), (s.weightedVSub p) (w₁ - w₂)⟫_ℝ = (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>w₁ w₂ : ι → ℝ<VAR>p : ι → P<VAR>h₁ : ∑ i ∈ s, w₁ i = 1<VAR>h₂ : ∑ i ∈ s, w₂ i = 1<VAR>h : ∑ i ∈ s, (w₁ - w₂) i = 0<GOAL>RCLike.re ⟪(s.weightedVSub p) (w₁ - w₂), (s.weightedVSub p) (w₁ - w₂)⟫_ℝ = (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
<VAR>b o : Ordinal.{u_1}<VAR>hb : b ≤ 1<VAR>ho : o ≠ 0<GOAL>CNF b o = [(0, o)]
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<VAR>hb : 0 ≤ 1<GOAL>CNF 0 o = [(0, o)]
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<VAR>hb : 1 ≤ 1<GOAL>CNF 1 o = [(0, o)]
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<GOAL>↑(ℑ (I • a)) = ↑(ℜ a)
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<GOAL>2⁻¹ • -I • (I • a - star (I • a)) = 2⁻¹ • (a + star a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a - b ≤ c ↔ a - c ≤ b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝ : SeminormedAddCommGroup E<VAR>s t : Set α<VAR>f✝ : α → E<VAR>a✝ : α<VAR>h : s ⊆ t<VAR>f : α → E<VAR>a : α<GOAL>‖s.indicator f a‖ ≤ ‖t.indicator f a‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝ : SeminormedAddCommGroup E<VAR>s t : Set α<VAR>f✝ : α → E<VAR>a✝ : α<VAR>h : s ⊆ t<VAR>f : α → E<VAR>a : α<GOAL>s.indicator (fun a => ‖f a‖) a ≤ t.indicator (fun a => ‖f a‖) a
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<GOAL>((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<GOAL>((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<GOAL>w ∈ closure (ball c R \ s)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>t : Set ℂ<VAR>ht : t ∈ 𝓝 w<GOAL>(t ∩ (ball c R \ s)).Nonempty
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>t : Set ℂ<VAR>ht : t ∈ 𝓝 w<VAR>g : ℝ → ℂ := fun x => w + ofReal x<GOAL>(t ∩ (ball c R \ s)).Nonempty