ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<VAR>hdnf : ∀ x ∈ -Ioo a b, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<VAR>hdnf : ∀ x ∈ -Ioo a b, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ -Ioo a b, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<VAR>hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ -Ioo a b, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<VAR>hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<VAR>hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<VAR>this : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[>] (-b)) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<VAR>hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<VAR>this✝ : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[>] (-b)) l<VAR>this : Tendsto ((fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) (𝓝[<] b) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<VAR>hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<VAR>this✝ : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[>] (-b)) l<VAR>this : Tendsto (fun x => (fun x => f (-x) / g (-x)) (-x)) (𝓝[<] b) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<GOAL>μ.toFinite.withDensity μ.densityToFinite = μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : (μ.toFinite.withDensity fun a => ∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite a) = μ.toFinite.withDensity (∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite)<GOAL>μ.toFinite.withDensity μ.densityToFinite = μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : (μ.toFinite.withDensity fun a => ∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite a) = μ.toFinite.withDensity (∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite)<GOAL>(Measure.sum fun n => μ.toFinite.withDensity ((sFiniteSeq μ n).rnDeriv μ.toFinite)) = μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : (μ.toFinite.withDensity fun a => ∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite a) = μ.toFinite.withDensity (∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite)<GOAL>(Measure.sum fun n => μ.toFinite.withDensity ((sFiniteSeq μ n).rnDeriv μ.toFinite)) = Measure.sum (sFiniteSeq μ)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : (μ.toFinite.withDensity fun a => ∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite a) = μ.toFinite.withDensity (∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite)<VAR>n : ℕ<VAR>s✝ : Set α<VAR>a✝ : MeasurableSet s✝<GOAL>(μ.toFinite.withDensity ((sFiniteSeq μ n).rnDeriv μ.toFinite)) s✝ = (sFiniteSeq μ n) s✝
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SFinite μ<VAR>this : (μ.toFinite.withDensity fun a => ∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite a) = μ.toFinite.withDensity (∑' (n : ℕ), (sFiniteSeq μ n).rnDeriv μ.toFinite)<VAR>n : ℕ<VAR>s✝ : Set α<VAR>a✝ : MeasurableSet s✝<GOAL>sFiniteSeq μ n ≪ μ.toFinite
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>Disjoint (a ∆ b) (a ⊓ b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>s : Set X<GOAL>StableUnderGeneralization s ↔ ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>s : Set X<GOAL>StableUnderGeneralization s → ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>s : Set X<GOAL>(∃ S, (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = sᶜ) → ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s
<VAR>α✝ : Type u_1<VAR>cmp : α✝ → α✝ → Ordering<VAR>t : RBNode α✝<VAR>v : α✝<VAR>h : Ordered cmp t<GOAL>Ordered cmp (match t.isRed with | red => (ins cmp v t).setBlack | black => ins cmp v t)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<VAR>s : Stream' α<VAR>b : α<VAR>x✝ : a ∈ s<VAR>n : ℕ<VAR>h : (fun b => a = b) (s.get n)<GOAL>(fun b => a = b) ((b :: s).get n.succ)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f✝ f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f✝ x✝)<VAR>g' : TangentSpace I' (f✝ x✝) →L[𝕜] TangentSpace I'' (g (f✝ x✝))<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<GOAL>MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f✝ f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f✝ x✝)<VAR>g' : TangentSpace I' (f✝ x✝) →L[𝕜] TangentSpace I'' (g (f✝ x✝))<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<GOAL>ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x) ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f✝ f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f'✝ f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f✝ x✝)<VAR>g' : TangentSpace I' (f✝ x✝) →L[𝕜] TangentSpace I'' (g (f✝ x✝))<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>f' : E →L[𝕜] E'<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x) ↔ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f✝ f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f'✝ f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f✝ x✝)<VAR>g' : TangentSpace I' (f✝ x✝) →L[𝕜] TangentSpace I'' (g (f✝ x✝))<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>f' : E →L[𝕜] E'<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x) ↔ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>Integrable (fun x => (ν (Prod.mk x ⁻¹' s)).toReal) μ
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>HasFiniteIntegral (fun x => (ν (Prod.mk x ⁻¹' s)).toReal) μ
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ < ⊤
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ = (μ.prod ν) s
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>(fun a => ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal) =ᶠ[ae μ] fun a => ν (Prod.mk a ⁻¹' s)
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<VAR>x : α<VAR>hx : ν (Prod.mk x ⁻¹' s) < ⊤<GOAL>ENNReal.ofReal (ν (Prod.mk x ⁻¹' s)).toReal = ν (Prod.mk x ⁻¹' s)
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<VAR>x : α<VAR>hx : ν (Prod.mk x ⁻¹' s) ≠ ⊤<GOAL>ENNReal.ofReal (ν (Prod.mk x ⁻¹' s)).toReal = ν (Prod.mk x ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹³ : AddCommGroup N<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁹ : Module.Free R M<VAR>inst✝⁸ : Module.Finite R M<VAR>inst✝⁷ : Module.Free R N<VAR>inst✝⁶ : Module.Finite R N<VAR>inst✝⁵ : Module.Free R P<VAR>inst✝⁴ : Module.Finite R P<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>A : Type u_6<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M<VAR>b' : Basis (Module.Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b<GOAL>(trace A (A ⊗[R] M)) (baseChange A f) = ↑(algebraMap R A) ((trace R M) f)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<GOAL>¬LinearIndependent R v ↔ ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<GOAL>(¬∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0) ↔ ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>p : β → Prop<GOAL>(∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (↑e x)
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>r : R<VAR>m : M<VAR>s : ↥S<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk (r • m) s) = r • (fromLocalizedModule S f) (LocalizedModule.mk m s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b₁ : Set (Set β)<VAR>hb₁c : b₁.Countable<VAR>b₂ : Set (Set β)<VAR>hb₂c : b₂.Countable<GOAL>CountablyGenerated β
<VAR>α : Type u_1<VAR>a : α<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderBot α<VAR>x y : ↑(Iic a)<GOAL>Disjoint x y ↔ Disjoint ↑x ↑y
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.414921, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅ = app₄ ≫ g.map' 4 5 ⋯ ⋯<GOAL>2 < 5 + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Fintype α<VAR>s t : Finset α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : Fintype { a // p a }<GOAL>Finset.subtype p s = univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsPurelyInseparable F E<GOAL>sepDegree F E = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ map (Embedding.refl α) s ↔ x✝ ∈ s
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>(uniformity R).HasBasis (fun x => True) fun γ => {p | v (p.2 - p.1) < ↑γ}
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>(Filter.comap (fun x => x.2 - x.1) (𝓝 0)).HasBasis (fun x => True) fun γ => {p | v (p.2 - p.1) < ↑γ}
<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>v w : F<VAR>h : ‖v‖ = ‖w‖<VAR>R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ<GOAL>R v = w
<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>v w : F<VAR>h : ‖v‖ = ‖w‖<VAR>R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ<GOAL>R v + R v = w + w
<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>v w : F<VAR>h : ‖v‖ = ‖w‖<VAR>R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ<VAR>h₁ : R (v - w) = -(v - w)<GOAL>R v + R v = w + w
<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>v w : F<VAR>h : ‖v‖ = ‖w‖<VAR>R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ<VAR>h₁ : R (v - w) = -(v - w)<VAR>h₂ : R (v + w) = v + w<GOAL>R v + R v = w + w