ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>δ : ℝ≥0<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hs : MeasurableSet s<VAR>f' : E → E →L[ℝ] E<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>x : E<VAR>hx : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>xs : x ∈ s<VAR>z : E<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty<VAR>ρ : ℝ<VAR>ρpos : ρ > 0<VAR>hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}<VAR>B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ<GOAL>‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>δ : ℝ≥0<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hs : MeasurableSet s<VAR>f' : E → E →L[ℝ] E<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>x : E<VAR>hx : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>xs : x ∈ s<VAR>z : E<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty<VAR>ρ : ℝ<VAR>ρpos : ρ > 0<VAR>hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}<VAR>B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ<VAR>r : ℝ<VAR>y : E<VAR>ys : y ∈ s<VAR>hy : y ∈ {x} + r • closedBall z ε<VAR>rρ : {x} + r • closedBall z ε ⊆ ball x ρ<VAR>rpos : 0 < r<GOAL>‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>δ : ℝ≥0<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hs : MeasurableSet s<VAR>f' : E → E →L[ℝ] E<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>x : E<VAR>hx : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>xs : x ∈ s<VAR>z : E<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty<VAR>ρ : ℝ<VAR>ρpos : ρ > 0<VAR>hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}<VAR>B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ<VAR>r : ℝ<VAR>y : E<VAR>ys : y ∈ s<VAR>hy : y ∈ {x} + r • closedBall z ε<VAR>rρ : {x} + r • closedBall z ε ⊆ ball x ρ<VAR>rpos : 0 < r<VAR>a : E<VAR>az : a ∈ closedBall z ε<VAR>ya : y = x + r • a<GOAL>‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>δ : ℝ≥0<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hs : MeasurableSet s<VAR>f' : E → E →L[ℝ] E<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>x : E<VAR>hx : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>xs : x ∈ s<VAR>z : E<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty<VAR>ρ : ℝ<VAR>ρpos : ρ > 0<VAR>hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}<VAR>B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ<VAR>r : ℝ<VAR>y : E<VAR>ys : y ∈ s<VAR>hy : y ∈ {x} + r • closedBall z ε<VAR>rρ : {x} + r • closedBall z ε ⊆ ball x ρ<VAR>rpos : 0 < r<VAR>a : E<VAR>az : a ∈ closedBall z ε<VAR>ya : y = x + r • a<VAR>norm_a : ‖a‖ ≤ ‖z‖ + ε<GOAL>‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>δ : ℝ≥0<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hs : MeasurableSet s<VAR>f' : E → E →L[ℝ] E<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>x : E<VAR>hx : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>xs : x ∈ s<VAR>z : E<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty<VAR>ρ : ℝ<VAR>ρpos : ρ > 0<VAR>hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}<VAR>B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ<VAR>r : ℝ<VAR>y : E<VAR>ys : y ∈ s<VAR>hy : y ∈ {x} + r • closedBall z ε<VAR>rρ : {x} + r • closedBall z ε ⊆ ball x ρ<VAR>rpos : 0 < r<VAR>a : E<VAR>az : a ∈ closedBall z ε<VAR>ya : y = x + r • a<VAR>norm_a : ‖a‖ ≤ ‖z‖ + ε<VAR>I : r * ‖(f' x - A) a‖ ≤ r * (↑δ + ε) * (‖z‖ + ε)<GOAL>‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝ : LocallyCompactPair Y Z<GOAL>Continuous fun x => x.2.comp x.1
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝ : LocallyCompactPair Y Z<GOAL>∀ (x : C(X, Y) × C(Y, Z)) (K : Set X), IsCompact K → ∀ (U : Set Z), IsOpen U → MapsTo (⇑(x.2.comp x.1)) K U → ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 x, MapsTo (⇑(a.2.comp a.1)) K U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>inst✝ : LocallyCompactPair Y Z<VAR>f : C(X, Y)<VAR>g : C(Y, Z)<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set Z<VAR>hU : IsOpen U<VAR>hKU : MapsTo (⇑g ∘ ⇑f) K U<GOAL>∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>inst✝ : LocallyCompactPair Y Z<VAR>f : C(X, Y)<VAR>g : C(Y, Z)<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set Z<VAR>hU : IsOpen U<VAR>hKU : MapsTo (⇑g ∘ ⇑f) K U<VAR>L : Set Y<VAR>hKL : L ∈ 𝓝ˢ (⇑f '' K)<VAR>hLc : IsCompact L<VAR>hLU : MapsTo (⇑g) L U<GOAL>∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>inst✝ : LocallyCompactPair Y Z<VAR>f : C(X, Y)<VAR>g : C(Y, Z)<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set Z<VAR>hU : IsOpen U<VAR>hKU : MapsTo (⇑g ∘ ⇑f) K U<VAR>L : Set Y<VAR>hKL : MapsTo (⇑f) K (interior L)<VAR>hLc : IsCompact L<VAR>hLU : MapsTo (⇑g) L U<GOAL>∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
<VAR>z τ : ℂ<GOAL>∑' (n : ℤ), 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + 1) + ↑π * I * ↑n ^ 2 * τ) = ∑' (n : ℤ), 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + 1) + ↑π * I * ↑n ^ 2 * τ) = 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>h : X - C a ∣ p<GOAL>p.IsRoot a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>h : p.IsRoot a<GOAL>p = (X - C a) * (p /ₘ (X - C a))
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>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 : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>y : M'<VAR>hy : f x ∈ (chartAt H' y).source<GOAL>ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset (Option α)<VAR>p : Option α → Prop<GOAL>(∀ a ∈ eraseNone s, p (some a)) ↔ ∀ (a : α), some a ∈ s → p (some a)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 - ε ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : 0 < 1 - ε ↑n<GOAL>0 ≤ 1 - ε ↑n
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>u : ℤˣ<VAR>w : NormalWord d<GOAL>t ^ ↑u • w = unitsSMul φ u w
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hg : IsMulFreimanIso n B C g<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<GOAL>(map (g ∘ f) s).prod = (map (g ∘ f) t).prod ↔ s.prod = t.prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hg : IsMulFreimanIso n B C g<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<GOAL>(map g (map f s)).prod = (map g (map f t)).prod ↔ s.prod = t.prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hg : IsMulFreimanIso n B C g<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<GOAL>∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hg : IsMulFreimanIso n B C g<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<GOAL>∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ✝ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>δ : Type u_6<VAR>f : α → γ<VAR>g : β → δ<VAR>a : Filter α<VAR>b : Filter β<VAR>c : Filter γ<VAR>d : Filter δ<VAR>hf : Tendsto f a c<VAR>hg : Tendsto g b d<GOAL>Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ✝ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>δ : Type u_6<VAR>f : α → γ<VAR>g : β → δ<VAR>a : Filter α<VAR>b : Filter β<VAR>c : Filter γ<VAR>d : Filter δ<VAR>hf : Tendsto f a c<VAR>hg : Tendsto g b d<GOAL>map f a ×ˢ map g b ≤ c ×ˢ d
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<GOAL>eraseLead 0 = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>coeffs 1 ⊆ {1}
<VAR>V : Type u<VAR>inst✝ : Quiver V<VAR>a✝¹ b✝¹ c✝ d a b c x✝ : V<VAR>p : Path a b<VAR>q : Path b c<VAR>b✝ : V<VAR>r : Path c b✝<VAR>a✝ : b✝ ⟶ x✝<GOAL>(p.comp q).comp (r.cons a✝) = p.comp (q.comp (r.cons a✝))
<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>f✝ g✝ : α → ℝ≥0∞<VAR>f : β → ℝ≥0∞<VAR>g : β → γ<GOAL>∑' (x : γ) (b : ↑(g ⁻¹' {x})), f ↑b = ∑' (i : β), f i
<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>f✝ g✝ : α → ℝ≥0∞<VAR>f : β → ℝ≥0∞<VAR>g : β → γ<GOAL>HasSum (fun b => ∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1) (∑' (i : β), f i)
<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>f✝ g✝ : α → ℝ≥0∞<VAR>f : β → ℝ≥0∞<VAR>g : β → γ<VAR>equiv : (y : γ) × { x // g x = y } ≃ β := Equiv.sigmaFiberEquiv g<GOAL>HasSum (fun b => ∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1) (∑' (i : β), f i)
<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>f✝ g✝ : α → ℝ≥0∞<VAR>f : β → ℝ≥0∞<VAR>g : β → γ<VAR>equiv : (y : γ) × { x // g x = y } ≃ β := Equiv.sigmaFiberEquiv g<GOAL>∀ (b : γ), HasSum (fun c => (f ∘ ⇑equiv) ⟨b, c⟩) (∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_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✝ s : Set ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>a * sSup s = ⨆ i ∈ s, a * i
<VAR>α : Type u_1<VAR>inst✝¹ : FinEnum α<VAR>β : α → Type u_2<VAR>inst✝ : (a : α) → FinEnum (β a)<VAR>f : (a : α) → β a<GOAL>f ∈ enum β
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>a : ℤ<VAR>K : CochainComplex C ℤ<GOAL>(shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K = (shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)
<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>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R<VAR>h : IsUnit (a - b)<GOAL>-C ↑h.unit⁻¹ * (X - C a) + C ↑h.unit⁻¹ * (X - C b) = 1
<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>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R<VAR>h : IsUnit (a - b)<GOAL>C (↑h.unit⁻¹ * (a - b)) = 1
<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>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R<VAR>h : IsUnit (a - b)<GOAL>C (↑h.unit⁻¹ * (a - b)) = C 1
<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>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R<VAR>h : IsUnit (a - b)<GOAL>↑h.unit⁻¹ * (a - b) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedCommRing β<VAR>inst✝ : OrderTopology β<GOAL>(∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a => |k a|) fun a => |f a|
<VAR>X : Type u_1<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OpensMeasurableSpace X<GOAL>Continuous fun x => diracProba x
<VAR>X : Type u_1<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OpensMeasurableSpace X<GOAL>∀ (x : X), ContinuousAt (fun x => diracProba x) x
<VAR>X : Type u_1<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>x : X<VAR>f : X →ᵇ ℝ≥0<GOAL>Tendsto (fun i => ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) (𝓝 x) (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))
<VAR>X : Type u_1<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>x : X<VAR>f : X →ᵇ ℝ≥0<VAR>f_mble : Measurable fun X_1 => ↑(f X_1)<GOAL>Tendsto (fun i => ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) (𝓝 x) (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))
<VAR>X : Type u_1<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OpensMeasurableSpace X<VAR>x : X<VAR>f : X →ᵇ ℝ≥0<VAR>f_mble : Measurable fun X_1 => ↑(f X_1)<GOAL>Tendsto (fun i => ↑(f i)) (𝓝 x) (𝓝 ↑(f x))
<VAR>x : ℝ≥0∞<VAR>y : ℝ<GOAL>(x ^ y).log = ↑y * x.log
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>y_neg : y < 0<GOAL>(x ^ y).log = ↑y * x.log
<VAR>x : ℝ≥0∞<GOAL>(x ^ 0).log = ↑0 * x.log
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>y_pos : 0 < y<GOAL>(x ^ y).log = ↑y * x.log
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_2, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>j : I<VAR>A : C<VAR>f g : tensorObj (tensorObj X₁ X₂) X₃ j ⟶ A<VAR>H : X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g<GOAL>f = g
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_2, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>j : I<VAR>A : C<VAR>f g : tensorObj (tensorObj X₁ X₂) X₃ j ⟶ A<VAR>H : X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g<GOAL>∀ (i₁ i₂ i₃ : I) (h : r₁₂₃ (i₁, i₂, i₃) = j), ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιMapBifunctor₁₂BifunctorMapObj (curriedTensor C) (curriedTensor C) ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>𝕜' : Type u_3<VAR>inst✝⁵ : NontriviallyNormedField 𝕜'<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝³ : NormedSpace 𝕜' E<VAR>inst✝² : IsScalarTower 𝕜 𝕜' E<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>p'✝ : E → FormalMultilinearSeries 𝕜' E F<VAR>h : ContDiffWithinAt 𝕜' n f s x<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set E<VAR>u_mem : u ∈ 𝓝[insert x s] x<VAR>p' : E → FormalMultilinearSeries 𝕜' E F<VAR>hp' : HasFTaylorSeriesUpToOn (↑m) f p' u<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι ι' : Type u<VAR>r : ι → ι → Prop<VAR>r' : ι' → ι' → Prop<VAR>inst✝¹ : IsWellOrder ι r<VAR>inst✝ : IsWellOrder ι' r'<VAR>o : Ordinal.{u}<VAR>ho : type r = o<VAR>ho' : type r' = o<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>lsub (familyOfBFamily' r ho f) = lsub (familyOfBFamily' r' ho' f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>s : Set (α × β)<GOAL>sᶜ ∈ cofinite.coprod cofinite ↔ sᶜ ∈ cofinite
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<GOAL>‖deriv f x‖ = ‖fderiv 𝕜 f x‖
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<GOAL>a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<GOAL>a.natAbs ≤ b.natAbs ↔ ↑a.natAbs ≤ ↑b.natAbs
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>s : Set ι<VAR>t : ι → Set α<VAR>hc : s.Countable<VAR>this : Encodable ↑s<GOAL>μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>hg : g.SurjectiveOnStalks<VAR>hf : f.SurjectiveOnStalks<VAR>I : Ideal T<VAR>hI : I.IsPrime<GOAL>Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)