ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<VAR>b : ℝ<VAR>ba : b ∈ Iio a<VAR>sab : Ico b a ⊆ s<VAR>t : Set ℝ := Ioo b a<VAR>ts : t ⊆ s<VAR>t_diff : DifferentiableOn ℝ f t<VAR>t_conv : Convex ℝ t<VAR>t_open : IsOpen t<VAR>t_closure : closure t = Icc b a<VAR>t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y<VAR>t_diff' : Tendsto (fun x => fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))<VAR>this : HasDerivWithinAt f e (Icc b a) a<GOAL>HasDerivWithinAt f e (Iic a) a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<VAR>i j : Fin n<GOAL>of (fun i j => eval (v i) (p j)) i j = (vandermonde v * of fun i j => (p j).coeff ↑i) i j
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<VAR>i j : Fin n<GOAL>((p j).sum fun e a => (RingHom.id R) a * v i ^ e) = ∑ j_1 : Fin n, vandermonde v i j_1 * of (fun i j => (p j).coeff ↑i) j_1 j
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<VAR>i j : Fin n<GOAL>((p j).sum fun e a => (RingHom.id R) a * v i ^ e) = ∑ x : Fin n, v i ^ ↑x * of (fun i j => (p j).coeff ↑i) x j
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<VAR>i j : Fin n<VAR>this : (p j).support ⊆ range n<GOAL>((p j).sum fun e a => (RingHom.id R) a * v i ^ e) = ∑ x : Fin n, v i ^ ↑x * of (fun i j => (p j).coeff ↑i) x j
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<VAR>i j : Fin n<VAR>this : (p j).support ⊆ range n<GOAL>∑ i_1 : Fin n, (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1 = ∑ x : Fin n, v i ^ ↑x * of (fun i j => (p j).coeff ↑i) x j
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<VAR>i j : Fin n<VAR>this : (p j).support ⊆ range n<VAR>k : Fin n<GOAL>(RingHom.id R) ((p j).coeff ↑k) * v i ^ ↑k = v i ^ ↑k * of (fun i j => (p j).coeff ↑i) k j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<GOAL>(s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<GOAL>1 < s.card * t.card ↔ 0 < s.card ∧ 0 < t.card ∧ (1 < s.card ∨ 1 < t.card)
<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>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a * b)<VAR>nonempty : s.Nonempty<VAR>base : ∀ x ∈ s, p (f x)<GOAL>Multiset.map (fun x => f x) s.val ≠ ∅
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x<GOAL>0 ≤ᶠ[ae (μ.restrict s)] f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).c₆ = φ W.c₆
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>-φ W.b₂ ^ 3 + 36 * φ W.b₂ * φ W.b₄ - 216 * φ W.b₆ = φ (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>inst✝ : MulOneClass M<VAR>a : M<GOAL>SemiconjBy a 1 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>m : α → ℝ≥0∞<VAR>f : Filter α<GOAL>Tendsto m f (𝓝 ⊤) ↔ ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, ↑x < m a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>hfi : IntegrableOn f (⋃ n, s n) μ<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>hfi : IntegrableOn f (⋃ n, s n) μ<VAR>hfi' : ∫⁻ (x : X) in ⋃ n, s n, ↑‖f x‖₊ ∂μ < ⊤<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hfi' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ⊤<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hfi' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ⊤<VAR>hSm : MeasurableSet S<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hfi' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ⊤<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hfi' : (μ.withDensity fun x => ↑‖f x‖₊) S < ⊤<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<GOAL>∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<GOAL>∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<GOAL>∫ (x : X) in s i, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<GOAL>↑‖∫ (x : X) in S \ s i, f x ∂μ‖₊ ≤ ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<GOAL>∫⁻ (a : X) in S \ s i, ↑‖f a‖₊ ∂μ ≤ ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<GOAL>ν S - ν (s i) ≤ ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_mono : Monotone s<VAR>S : Set X := ⋃ i, s i<VAR>hfi : IntegrableOn f S μ<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ {i : ι}, s i ⊆ S<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hfi' : ν S < ⊤<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<GOAL>ν (s i) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>S : Set (Set α)<VAR>hSo : ∀ t ∈ S, IsOpen t<VAR>hSc : S.Countable<GOAL>MeasurableSet (⋂₀ S)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : n < p.natDegree<VAR>H : p = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>mα : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (_root_.id '' s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : LinearOrderedSemifield β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<VAR>hf : StrongLT 0 f<VAR>hg : StrongLT 0 g<GOAL>Antivary f⁻¹ g⁻¹ ↔ Antivary f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>g : M → N<VAR>f : α → M<VAR>hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)<VAR>x : α<GOAL>(g ∘ f) x = 1 ↔ f x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<VAR>r : ℝ<GOAL>(r • s).rnDeriv μ =ᶠ[ae μ] r • s.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<VAR>r : ℝ<GOAL>μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Group α<VAR>a : α<GOAL>a⁺ᵐ = if 1 ≤ a then a else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Group α<VAR>a : α<GOAL>a ⊔ 1 = (fun x x_1 => x ⊔ x_1) 1 a
<VAR>α : Type u_1<VAR>I B X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<GOAL>∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
<VAR>α : Type u_1<VAR>I B X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>h : ¬∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>I : Set α<VAR>e : α<VAR>hIe : ¬Indep (insert e I)<VAR>h : ∀ I₀ ⊆ I, I₀.Finite → Indep (insert e I₀)<VAR>J : Set α<VAR>hJss : J ⊆ insert e I<VAR>hJfin : J.Finite<GOAL>Indep J
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hImax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | Indep I}<VAR>hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | Indep I}<GOAL>∃ x ∈ B \ I, Indep (insert x I)
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hImax : ∃ x, Indep x ∧ I ⊆ x ∧ ¬I = x<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<GOAL>∃ x ∈ B \ I, Indep (insert x I)
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<GOAL>∃ x ∈ B \ I, Indep (insert x I)
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<GOAL>∃ x ∈ B \ I, Indep (insert x I)
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<GOAL>∃ x ∈ B \ I, Indep (insert x I)
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<GOAL>∃ x ∈ B \ I, Indep (insert x I)
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ¬∃ x ∈ B \ I, Indep (insert x I)<GOAL>False