ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>xD : x ∈ D<VAR>hf : oscillationWithin f D x = 0<VAR>ε : ℝ≥0∞<VAR>S : Set F<VAR>hS : S ∈ Filter.map f (𝓝[D] x)<VAR>Sε : diam S < ε<GOAL>∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>xD : x ∈ D<VAR>hf : oscillationWithin f D x = 0<VAR>ε : ℝ≥0∞<VAR>S : Set F<VAR>hS : S ∈ Filter.map f (𝓝[D] x)<VAR>Sε : diam S < ε<VAR>y : E<VAR>hy : y ∈ f ⁻¹' S<GOAL>edist (f y) (f x) ≤ diam S
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>h : J ≤ I<GOAL>(single I J h).iUnion = ↑J
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → Set X<VAR>h : ∀ i ∈ s, IsGδ (f i)<GOAL>IsGδ (⋃ i ∈ s, f i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → Set X<VAR>h : ∀ i ∈ s, IsGδ (f i)<GOAL>IsGδ (⋃₀ (f '' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ<VAR>hδ_pos : 0 < δ<VAR>hfδ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ<VAR>hδ_pos : 0 < δ<VAR>hfδ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>n : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal δ<GOAL>s.indicator (g n) =ᶠ[ae μ] s.indicator (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ<VAR>hδ_pos : 0 < δ<VAR>hfδ : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>n : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal δ<VAR>x : α<VAR>hx : f n x = g n x<GOAL>s.indicator (g n) x = s.indicator (f n) x
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>ha : 0 < a<VAR>hb : 1 < b<GOAL>n * b < a * b ^ (n + 1)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>ha : 0 < a<VAR>hb : 1 < b<GOAL>n < a * b ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>F : α<VAR>F0 : F > 0<VAR>hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j<VAR>H : g.LimZero<VAR>i : ℕ<VAR>h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>h₁ : F ≤ ↑f j<VAR>h₂ : |↑g j| < F / 2<GOAL>F / 2 ≤ ↑(f + g) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>F : α<VAR>F0 : F > 0<VAR>hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j<VAR>H : g.LimZero<VAR>i : ℕ<VAR>h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>h₁ : F ≤ ↑f j<VAR>h₂ : |↑g j| < F / 2<VAR>this : F + -(F / 2) ≤ ↑f j + ↑g j<GOAL>F / 2 ≤ ↑(f + g) j
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>inst✝ : HasGroupoid M G<VAR>s U : Opens M<VAR>x : ↥U<VAR>e : PartialHomeomorph M H := chartAt H ↑x<GOAL>↑e.symm =ᶠ[𝓝 (↑e ↑x)] Subtype.val ∘ ↑(chartAt H x).symm
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>inst✝ : HasGroupoid M G<VAR>s U : Opens M<VAR>x : ↥U<VAR>e : PartialHomeomorph M H := chartAt H ↑x<VAR>heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)<GOAL>↑e.symm =ᶠ[𝓝 (↑e ↑x)] Subtype.val ∘ ↑(chartAt H x).symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>hf : InjOn f (loopyOn E).E<GOAL>(loopyOn E).map f hf = loopyOn (f '' E)
<VAR>x y : ℂ<GOAL>cosh x ^ 2 = sinh x ^ 2 + 1
<VAR>x y : ℂ<GOAL>cosh x ^ 2 = sinh x ^ 2 + (cosh x ^ 2 - sinh x ^ 2)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p q : R[X]<VAR>inst✝³ : CommRing T<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<GOAL>X.aroots S = {0}
<VAR>t : ℝ<VAR>ht : t ∈ Set.Icc 0 1<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
<VAR>t : ℝ<VAR>ht : 0 ≤ t ∧ t ≤ 1<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
<VAR>t : ℝ<VAR>ht : 0 ≤ t ∧ t ≤ 1<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>(abs (1 + ↑t * z))⁻¹ ≤ (1 - ‖z‖)⁻¹
<VAR>t : ℝ<VAR>ht : 0 ≤ t ∧ t ≤ 1<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>1 - ‖z‖ ≤ abs (1 + ↑t * z)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<GOAL>Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>f : E →ₗ[ℝ] F<VAR>v : ι → E<GOAL>⇑f '' parallelepiped v = parallelepiped (⇑f ∘ v)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>f : E →ₗ[ℝ] F<VAR>v : ι → E<GOAL>(⇑f ∘ fun t => ∑ i : ι, t i • v i) '' Icc 0 1 = (fun t => ∑ i : ι, t i • (⇑f ∘ v) i) '' Icc 0 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>f : E →ₗ[ℝ] F<VAR>v : ι → E<VAR>t : F<GOAL>t ∈ (⇑f ∘ fun t => ∑ i : ι, t i • v i) '' Icc 0 1 ↔ t ∈ (fun t => ∑ i : ι, t i • (⇑f ∘ v) i) '' Icc 0 1
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>n G : Type v<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>α β : Type v<VAR>inst✝² : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>K : Type u_1<VAR>k : ℕ<VAR>inst✝ : Field K<VAR>M : Matrix n n K<VAR>m : ℕ<VAR>i j : n<GOAL>(matPolyEquiv ((↑(expand K k)).mapMatrix (M ^ k).charmatrix)).coeff m i j = (X ^ k - C (M ^ k)).coeff m i j
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>n G : Type v<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>α β : Type v<VAR>inst✝² : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>K : Type u_1<VAR>k : ℕ<VAR>inst✝ : Field K<VAR>M : Matrix n n K<VAR>m : ℕ<VAR>i j : n<GOAL>((expand K k) ((M ^ k).charmatrix i j)).coeff m = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>‖⟪x, y⟫_𝕜‖ * ‖⟪x, y⟫_𝕜‖ = ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜 = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : C<VAR>inst✝ : HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : Under X<VAR>y : Under Y<VAR>u : (pushout f).obj x ⟶ y<GOAL>x.hom ≫ pushout.inl x.hom f ≫ u.right = ((map f).obj y).hom
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : C<VAR>inst✝ : HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : Under X<VAR>y : Under Y<VAR>u : (pushout f).obj x ⟶ y<GOAL>x.hom ≫ pushout.inl x.hom f ≫ u.right = f ≫ y.hom
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : C<VAR>inst✝ : HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : Under X<VAR>y : Under Y<VAR>u : (pushout f).obj x ⟶ y<GOAL>x.hom ≫ pushout.inl x.hom f ≫ u.right = f ≫ ((pushout f).obj x).hom ≫ u.right
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : C<VAR>inst✝ : HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : Under X<VAR>y : Under Y<VAR>u : (pushout f).obj x ⟶ y<GOAL>x.hom ≫ pushout.inl x.hom f ≫ u.right = f ≫ pushout.inr x.hom f ≫ u.right
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<GOAL>map f (𝓝 x) = 𝓝 (f x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<VAR>t : Set E<VAR>ht : t ∈ 𝓝 x<GOAL>f '' t ∈ 𝓝 (f x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹<VAR>t : Set E<VAR>ht : t ∈ 𝓝 x<VAR>this : f '' (s ∩ t) ∈ 𝓝 (f x)<GOAL>f '' t ∈ 𝓝 (f x)
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab' : a < b<VAR>g : ℝ → ℝ := fun x => f x - m * x<GOAL>m ∈ f' '' Ioo a b
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab' : a < b<VAR>g : ℝ → ℝ := fun x => f x - m * x<VAR>hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x<GOAL>m ∈ f' '' Ioo a b
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab' : a < b<VAR>g : ℝ → ℝ := fun x => f x - m * x<VAR>hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x<VAR>c : ℝ<VAR>cmem : c ∈ Icc a b<VAR>hc : IsMinOn g (Icc a b) c<GOAL>m ∈ f' '' Ioo a b
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab' : a < b<VAR>g : ℝ → ℝ := fun x => f x - m * x<VAR>hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x<VAR>c : ℝ<VAR>cmem : c ∈ Icc a b<VAR>hc : IsMinOn g (Icc a b) c<VAR>cmem' : c ∈ Ioo a b<GOAL>m ∈ f' '' Ioo a b
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab' : a < b<VAR>g : ℝ → ℝ := fun x => f x - m * x<VAR>hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x<VAR>c : ℝ<VAR>cmem : c ∈ Icc a b<VAR>hc : IsMinOn g (Icc a b) c<VAR>cmem' : c ∈ Ioo a b<GOAL>f' c = m
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab' : a < b<VAR>g : ℝ → ℝ := fun x => f x - m * x<VAR>hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x<VAR>c : ℝ<VAR>cmem : c ∈ Icc a b<VAR>hc : IsMinOn g (Icc a b) c<VAR>cmem' : c ∈ Ioo a b<GOAL>f' c - m = 0
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab' : a < b<VAR>g : ℝ → ℝ := fun x => f x - m * x<VAR>hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x<VAR>c : ℝ<VAR>cmem : c ∈ Icc a b<VAR>hc : IsMinOn g (Icc a b) c<VAR>cmem' : c ∈ Ioo a b<VAR>this : Icc a b ∈ 𝓝 c<GOAL>f' c - m = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>x : ℝ≥0∞<GOAL>¬x < ⊤ ↔ x = ⊤
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>closure s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<GOAL>x ∈ closure s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<VAR>f_meas : Measurable f<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<VAR>f_meas : Measurable f<VAR>A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<VAR>f_meas : Measurable f<VAR>A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})<VAR>B : ν (s ∩ f ⁻¹' {⊤}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {⊤})<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<VAR>f_meas : Measurable f<VAR>A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})<VAR>B : ν (s ∩ f ⁻¹' {⊤}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {⊤})<VAR>C : ∀ (n : ℤ), ν (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>0 ∈ lowerBounds (Set.range fun p => projectiveSeminormAux ↑p)
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>∀ x_1 ∈ Set.range fun p => projectiveSeminormAux ↑p, 0 ≤ x_1
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>∀ a ∈ x.lifts, 0 ≤ projectiveSeminormAux a
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>(o.kahler x) x = ↑‖x‖ ^ 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>IsSimpleModule R (M ⧸ m) ↔ IsCoatom m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>IsSimpleModule R (M ⧸ m) ↔ IsSimpleOrder ↑(Set.Ici m)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>Submodule R (M ⧸ m) ≃o ↑(Set.Ici m)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<GOAL>𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>key : UniformInducing ⇑(addEquiv 𝕜 A)<GOAL>𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>key : UniformInducing ⇑(addEquiv 𝕜 A)<GOAL>𝓤 (Unitization 𝕜 A) = comap (fun x => ((addEquiv 𝕜 A) x.1, (addEquiv 𝕜 A) x.2)) (𝓤 (𝕜 × A))
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>dist a b ≤ ‖a‖ + ‖b‖
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>h : ∞ ∈ s<GOAL>IsOpen s ↔ IsClosed (some ⁻¹' s)ᶜ ∧ IsCompact (some ⁻¹' s)ᶜ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<GOAL>rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>k : ℕ<GOAL>((⇑derivative)^[k] p).natDegree ≤ p.natDegree - k
<VAR>α : Type u_1<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>x✝ : α<VAR>r : Ordnode α<GOAL>(node size✝ l x✝ r).toList.length = (node size✝ l x✝ r).realSize
<VAR>α : Type u_1<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>x✝ : α<VAR>r : Ordnode α<GOAL>l.realSize + (r.realSize + 1) = (node size✝ l x✝ r).realSize
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>f : (i : ι) → β i<VAR>s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<GOAL>i ∈ { toFun := f, support' := s }.support ↔ { toFun := f, support' := s } i ≠ 0