ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<GOAL>eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>h✝ : IsEmpty β<GOAL>eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>h✝ : Nonempty β<GOAL>eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>h✝ : Nonempty β<VAR>ψ : α → β := Function.invFunOn φ t<GOAL>eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>h✝ : Nonempty β<VAR>ψ : α → β := Function.invFunOn φ t<VAR>ψφs : EqOn (φ ∘ ψ) id (φ '' t)<GOAL>eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>h✝ : Nonempty β<VAR>ψ : α → β := Function.invFunOn φ t<VAR>ψφs : EqOn (φ ∘ ψ) id (φ '' t)<VAR>ψts : MapsTo ψ (φ '' t) t<GOAL>eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>h✝ : Nonempty β<VAR>ψ : α → β := Function.invFunOn φ t<VAR>ψφs : EqOn (φ ∘ ψ) id (φ '' t)<VAR>ψts : MapsTo ψ (φ '' t) t<VAR>hψ : MonotoneOn ψ (φ '' t)<GOAL>eVariationOn f (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>h✝ : Nonempty β<VAR>ψ : α → β := Function.invFunOn φ t<VAR>ψφs : EqOn (φ ∘ ψ) id (φ '' t)<VAR>ψts : MapsTo ψ (φ '' t) t<VAR>hψ : MonotoneOn ψ (φ '' t)<GOAL>eVariationOn (f ∘ id) (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : MonotoneOn φ t<VAR>h✝ : Nonempty β<VAR>ψ : α → β := Function.invFunOn φ t<VAR>ψφs : EqOn (φ ∘ ψ) id (φ '' t)<VAR>ψts : MapsTo ψ (φ '' t) t<VAR>hψ : MonotoneOn ψ (φ '' t)<GOAL>eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<GOAL>HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<VAR>A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)<GOAL>HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<VAR>A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)<GOAL>HasFDerivWithinAt (⇑(continuousMultilinearCurryFin0 𝕜 E F) ∘ fun x => p x 0) ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<VAR>A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)<GOAL>HasFDerivWithinAt (fun x => p x 0) ((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1))) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<VAR>A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)<VAR>this : ↑0 < n<GOAL>HasFDerivWithinAt (fun x => p x 0) ((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1))) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<VAR>A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)<VAR>this : ↑0 < n<GOAL>(↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) = (p x (Nat.succ 0)).curryLeft
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<VAR>A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)<VAR>this : ↑0 < n<VAR>y : E<VAR>v : Fin 0 → E<VAR>i : Fin (0 + 1)<GOAL>snoc 0 y i = cons y v i
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<VAR>A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0)<VAR>this : ↑0 < n<VAR>y : E<VAR>v : Fin 0 → E<VAR>i : Fin (0 + 1)<GOAL>snoc 0 y default = cons y v default
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors<GOAL>a.factors = b.factors
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<GOAL>a.factors = b.factors
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h_sb : b.factors = ↑sb<GOAL>a.factors = b.factors
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb<VAR>h_sb : b.factors = ↑sb<GOAL>↑sa = ↑sb
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb<VAR>h_sb : b.factors = ↑sb<GOAL>sa = sb
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb<VAR>h_sb : b.factors = ↑sb<VAR>h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb<GOAL>sa = sb
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb<VAR>h_sb : b.factors = ↑sb<VAR>h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb<GOAL>toFinsupp sa = toFinsupp sb
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb<VAR>h_sb : b.factors = ↑sb<VAR>h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>(toFinsupp sa) ⟨p, hp⟩ = (toFinsupp sb) ⟨p, hp⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<GOAL>IsBounded {x}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<GOAL>{x}ᶜ ∈ cobounded α
<VAR>n m a b : ℕ<VAR>han : a ≤ n<VAR>hbn : b ≤ n<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>n m a b : ℕ<VAR>han : a < n.succ<VAR>hbn : b < n.succ<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : 0 < (sort (fun x x_1 => x ≤ x_1) s).length<GOAL>0 < s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>h : s₂ ⊆ s₁<VAR>h₂ : MeasurableSet s₂<VAR>h_fin : μ s₂ ≠ ⊤<GOAL>μ (s₁ \ s₂) = μ s₁ - μ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>f : α → ℝ≥0<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) (ae μ) f<VAR>r : ℝ≥0∞<GOAL>r ≤ ⨅ a ∈ fun x => (map f (ae μ)).sets {x_1 | (fun x_2 => (fun x x_3 => x ≤ x_3) x_2 x) x_1}, ↑a ↔ r ≤ essSup (fun x => ↑(f x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>f : α → ℝ≥0<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) (ae μ) f<VAR>r : ℝ≥0∞<GOAL>(∀ i ∈ fun x => (map f (ae μ)).sets {x_1 | x_1 ≤ x}, r ≤ ↑i) ↔ ∀ (r_1 : ℝ≥0), (∀ᵐ (a : α) ∂μ, f a ≤ r_1) → r ≤ ↑r_1
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>hr' : 0 < ↑r<GOAL>count (fun x => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>hr' : 0 < ↑r<GOAL>⌈(↑b - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>hr' : 0 < ↑r<GOAL>↑(b / r) + ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>hr' : 0 < ↑r<GOAL>⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(if v % r < b % r then 1 else 0)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>hU : IsOpen U<GOAL>μ U = 0 ↔ U = ∅
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>H : J ⥤ K ⥤ C<VAR>inst✝ : HasColimitsOfShape J C<VAR>k : K<VAR>W : C<VAR>f g : (colimit H).obj k ⟶ W<VAR>w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g<GOAL>f = g
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>H : J ⥤ K ⥤ C<VAR>inst✝ : HasColimitsOfShape J C<VAR>k : K<VAR>W : C<VAR>f g : (colimit H).obj k ⟶ W<VAR>w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g<GOAL>(colimitObjIsoColimitCompEvaluation H k).inv ≫ f = (colimitObjIsoColimitCompEvaluation H k).inv ≫ g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>ht : μ t = 0<GOAL>s ∩ t ⊆ t
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<GOAL>g.TerminatedAt n ↔ g.s.get? n = none
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup H<VAR>inst✝⁸ : Module 𝕜 H<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑ofFun ∘ ⇑φ)<VAR>h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup H<VAR>inst✝⁸ : Module 𝕜 H<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑ofFun ∘ ⇑φ)<VAR>h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))<VAR>this : TopologicalAddGroup H<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup H<VAR>inst✝⁸ : Module 𝕜 H<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑ofFun ∘ ⇑φ)<VAR>h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))<VAR>this : TopologicalAddGroup H<VAR>hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup H<VAR>inst✝⁸ : Module 𝕜 H<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑ofFun ∘ ⇑φ)<VAR>h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))<VAR>this : TopologicalAddGroup H<VAR>hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}<GOAL>∀ {i : Set E}, i ∈ 𝓝 0 → ∃ V ∈ 𝓝 0, ∃ j ∈ 𝓝 0, V • {u | ∀ (x : α), φ u x ∈ j} ⊆ {u | ∀ (x : α), φ u x ∈ i}
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup H<VAR>inst✝⁸ : Module 𝕜 H<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑ofFun ∘ ⇑φ)<VAR>h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))<VAR>this : TopologicalAddGroup H<VAR>hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}<GOAL>∀ (x₀ : 𝕜) {i : Set E}, i ∈ 𝓝 0 → ∃ j ∈ 𝓝 0, Set.MapsTo (fun x => x₀ • x) {u | ∀ (x : α), φ u x ∈ j} {u | ∀ (x : α), φ u x ∈ i}
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup H<VAR>inst✝⁸ : Module 𝕜 H<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑ofFun ∘ ⇑φ)<VAR>h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))<VAR>this : TopologicalAddGroup H<VAR>hb : (𝓝 0).HasBasis (fun x => x ∈ 𝓝 0) fun V => {u | ∀ (x : α), φ u x ∈ V}<GOAL>∀ (m₀ : H) {i : Set E}, i ∈ 𝓝 0 → ∀ᶠ (x : 𝕜) in 𝓝 0, x • m₀ ∈ {u | ∀ (x : α), φ u x ∈ i}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional ℝ F<GOAL>Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ) = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional ℝ F<GOAL>∀ (x : F ≃ₗᵢ[ℝ] F), x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional ℝ F<VAR>φ : F ≃ₗᵢ[ℝ] F<GOAL>φ ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional ℝ F<VAR>l : List F<VAR>left✝ : l.length ≤ finrank ℝ F<GOAL>(List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional ℝ F<VAR>l : List F<VAR>left✝ : l.length ≤ finrank ℝ F<GOAL>∀ x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l, x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional ℝ F<VAR>l : List F<VAR>left✝ : l.length ≤ finrank ℝ F<VAR>x : F ≃ₗᵢ[ℝ] F<VAR>hx : x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l<GOAL>x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional ℝ F<VAR>l : List F<VAR>left✝¹ : l.length ≤ finrank ℝ F<VAR>x : F ≃ₗᵢ[ℝ] F<VAR>hx : x ∈ List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l<VAR>a : F<VAR>left✝ : a ∈ l<VAR>hax : reflection (Submodule.span ℝ {a})ᗮ = x<GOAL>x ∈ Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v})ᗮ)