ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : AffineSpace V2 P2<VAR>inst✝⁷ : AddCommGroup V3<VAR>inst✝⁶ : AffineSpace V3 P3<VAR>inst✝⁵ : Module k V1<VAR>inst✝⁴ : Module k V2<VAR>inst✝³ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommGroup (φv i)<VAR>inst✝¹ : (i : ι) → Module k (φv i)<VAR>inst✝ : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<GOAL>(∀ (p : P1) (a : ι), (fv a) p = 0 p a) ↔ ∀ (i : ι) (p : P1), (fv i) p = 0 p
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s : R<VAR>x✝ y : M<VAR>a b : R<VAR>h : a + b = 1<VAR>x : M<GOAL>a • x + b • x = x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<GOAL>Y ^ 2 + C (C (map W f).toAffine.a₁ * X + C (map W f).toAffine.a₃) * Y - C (X ^ 3 + C (map W f).toAffine.a₂ * X ^ 2 + C (map W f).toAffine.a₄ * X + C (map W f).toAffine.a₆) = Polynomial.map (mapRingHom f) (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : BooleanAlgebra α<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>(s.inf fun b => f b \ a) = s.inf f \ a
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>𝕜₁ : Type u_7<VAR>𝕜₂ : Type u_8<VAR>inst✝⁹ : NormedDivisionRing 𝕜₁<VAR>inst✝⁸ : NormedDivisionRing 𝕜₂<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜₁ E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜₂ F<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalSpace F<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>s : Set E<VAR>hs : IsVonNBounded 𝕜₁ s<VAR>f : E →SL[σ] F<GOAL>IsVonNBounded 𝕜₂ (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>𝕜₁ : Type u_7<VAR>𝕜₂ : Type u_8<VAR>inst✝⁹ : NormedDivisionRing 𝕜₁<VAR>inst✝⁸ : NormedDivisionRing 𝕜₂<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜₁ E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜₂ F<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalSpace F<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>s : Set E<VAR>hs : IsVonNBounded 𝕜₁ s<VAR>f : E →SL[σ] F<VAR>σ_iso : Isometry ⇑σ<GOAL>IsVonNBounded 𝕜₂ (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>𝕜₁ : Type u_7<VAR>𝕜₂ : Type u_8<VAR>inst✝⁹ : NormedDivisionRing 𝕜₁<VAR>inst✝⁸ : NormedDivisionRing 𝕜₂<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜₁ E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜₂ F<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalSpace F<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>s : Set E<VAR>hs : IsVonNBounded 𝕜₁ s<VAR>f : E →SL[σ] F<VAR>σ_iso : Isometry ⇑σ<VAR>this : map (⇑σ) (𝓝 0) = 𝓝 0<GOAL>IsVonNBounded 𝕜₂ (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>𝕜₁ : Type u_7<VAR>𝕜₂ : Type u_8<VAR>inst✝⁹ : NormedDivisionRing 𝕜₁<VAR>inst✝⁸ : NormedDivisionRing 𝕜₂<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜₁ E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜₂ F<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalSpace F<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>s : Set E<VAR>hs : IsVonNBounded 𝕜₁ s<VAR>f : E →SL[σ] F<VAR>σ_iso : Isometry ⇑σ<VAR>this : map (⇑σ) (𝓝 0) = 𝓝 0<VAR>hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)<GOAL>IsVonNBounded 𝕜₂ (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>𝕜₁ : Type u_7<VAR>𝕜₂ : Type u_8<VAR>inst✝⁹ : NormedDivisionRing 𝕜₁<VAR>inst✝⁸ : NormedDivisionRing 𝕜₂<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜₁ E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜₂ F<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalSpace F<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>s : Set E<VAR>f : E →SL[σ] F<VAR>σ_iso : Isometry ⇑σ<VAR>this : map (⇑σ) (𝓝 0) = 𝓝 0<VAR>hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)<VAR>hs : Tendsto (fun x => x • s) (𝓝 0) (𝓝 0).smallSets<GOAL>Tendsto ((fun x => x • ⇑f '' s) ∘ ⇑σ) (𝓝 0) (𝓝 0).smallSets
<VAR>x : ℝ<VAR>hx : x ∈ Icc (-(π / 2)) (π / 2)<GOAL>0 ≤ x + π / 2
<VAR>x : ℝ<VAR>hx : x ∈ Icc (-(π / 2)) (π / 2)<GOAL>x + π / 2 ≤ π
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ : α → ℝ<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
<VAR>X Y Z : Type u<VAR>f g : X ⟶ Y<VAR>π : Y ⟶ Z<VAR>e : f ≫ π = g ≫ π<VAR>h : IsColimit (Cofork.ofπ π e)<VAR>U : Set Y<VAR>H : f ⁻¹' U = g ⁻¹' U<GOAL>π ⁻¹' (π '' U) = U
<VAR>X Y Z : Type u<VAR>f g : X ⟶ Y<VAR>π : Y ⟶ Z<VAR>e : f ≫ π = g ≫ π<VAR>h : IsColimit (Cofork.ofπ π e)<VAR>U : Set Y<VAR>H : f ⁻¹' U = g ⁻¹' U<VAR>lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)<GOAL>π ⁻¹' (π '' U) = U
<VAR>X Y Z : Type u<VAR>f g : X ⟶ Y<VAR>π : Y ⟶ Z<VAR>e : f ≫ π = g ≫ π<VAR>h : IsColimit (Cofork.ofπ π e)<VAR>U : Set Y<VAR>H : f ⁻¹' U = g ⁻¹' U<VAR>lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)<VAR>eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U<GOAL>π ⁻¹' (π '' U) = U
<VAR>a✝ b✝ c✝ d m n a b c : ℤ<GOAL>a ≤ b ↔ a = b ∨ a < b
<VAR>a✝ b✝ c✝ d m n a b c : ℤ<GOAL>a ≤ b ↔ a ≤ b ∧ (b ≤ a ∨ ¬b ≤ a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (Metric.ball 0 ↑r')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n<GOAL>TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (Metric.ball 0 ↑r')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ x_1 ∈ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>L : Tendsto (fun n => C * a ^ n) atTop (𝓝 (C * 0))<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ x_1 ∈ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>L : Tendsto (fun n => C * a ^ n) atTop (𝓝 0)<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ x_1 ∈ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>L : Tendsto (fun n => C * a ^ n) atTop (𝓝 0)<VAR>n : ℕ<VAR>hn : C * a ^ n < ε<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<GOAL>dist (f (x + y)) (p.partialSum n y) < ε
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>-(((u * v) ^ 2) ^ 3 * W'.negAddY P Q) - W'.a₁ * (((u * v) ^ 2) ^ 2 * W'.addX P Q) * ((u * v) ^ 2 * addZ P Q) - W'.a₃ * ((u * v) ^ 2 * addZ P Q) ^ 3 = ((u * v) ^ 2) ^ 3 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Finset α<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).sym2 = image (fun b => s(a, b)) (insert a s) ∪ s.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Finset α<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∈ s<GOAL>(insert a s).sym2 = image (fun b => s(a, b)) (insert a s) ∪ s.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Finset α<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<GOAL>(insert a s).sym2 = image (fun b => s(a, b)) (insert a s) ∪ s.sym2
<VAR>z : ℂ<GOAL>HasSum (fun n => z ^ (2 * n) / ↑(2 * n)!) (cosh z)
<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 : UnifTight f p μ<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (g i)) p μ ≤ ↑ε
<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 : UnifTight f p μ<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε<VAR>n : ι<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 : UnifTight f p μ<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε<VAR>n : ι<VAR>x : α<VAR>hx : f n x = g n x<GOAL>sᶜ.indicator (g n) x = sᶜ.indicator (f n) x
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>P : (Fin n → α) → Prop<VAR>hf : P f<VAR>h : ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n), i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))<VAR>this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => toLex (f ∘ ⇑σ)<VAR>σ : Fin n ≃ Fin n<VAR>hσ : (fun σ => f ∘ ⇑σ) σ ≠ (fun σ => f ∘ ⇑σ) (sort f)<VAR>hfσ : P ((fun σ => f ∘ ⇑σ) σ)<GOAL>∃ c < σ, P ((fun σ => f ∘ ⇑σ) c)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>P : (Fin n → α) → Prop<VAR>hf : P f<VAR>h : ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n), i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))<VAR>this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => toLex (f ∘ ⇑σ)<VAR>σ : Fin n ≃ Fin n<VAR>hσ : (fun σ => f ∘ ⇑σ) σ ≠ (fun σ => f ∘ ⇑σ) (sort f)<VAR>hfσ : P ((fun σ => f ∘ ⇑σ) σ)<VAR>i j : Fin n<VAR>hij₁ : i < j<VAR>hij₂ : (f ∘ ⇑σ) j < (f ∘ ⇑σ) i<GOAL>∃ c < σ, P ((fun σ => f ∘ ⇑σ) c)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<GOAL>derivative ((expand R p) f) = (expand R p) (derivative f) * (↑p * X ^ (p - 1))
<GOAL>deriv arcsin = fun x => 1 / √(1 - x ^ 2)
<VAR>x : ℝ<GOAL>deriv arcsin x = 1 / √(1 - x ^ 2)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y : ↥S<VAR>w z : N<GOAL>z = w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ ↔ z * f ↑y = w
<VAR>s : Set Surreal<VAR>inst✝ : Small.{u, u + 1} ↑s<GOAL>BddBelow s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<GOAL>Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = nndist x y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.96057, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : W.LeftFraction X Y<GOAL>homMk f = f.map (Q W) ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.96057, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : W.LeftFraction X Y<VAR>this : IsIso ((Q W).map f.s)<GOAL>homMk f = f.map (Q W) ⋯
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<VAR>y : (n : ℕ) → E n<GOAL>y ∈ ⋃ k, cylinder (update x n k) (n + 1) ↔ y ∈ cylinder x n
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>n : ℕ<VAR>y : (n : ℕ) → E n<GOAL>(∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1) ↔ ∀ i < n, y i = x i
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.16313, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ F G : ComposableArrows C n<VAR>app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i<VAR>w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi<GOAL>∀ ⦃X Y : Fin (n + 1)⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.16313, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ F G : ComposableArrows C n<VAR>app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i<VAR>w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi<GOAL>∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<VAR>i : ℕ<GOAL>i ∈ p.restriction.support ↔ i ∈ p.support
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<VAR>i : ℕ<GOAL>p.restriction.coeff i = 0 ↔ p.coeff i = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<VAR>i : ℕ<GOAL>p.restriction.coeff i = 0 ↔ ↑(p.restriction.coeff i) = 0
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>f : M ≃[L] N<GOAL>f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup u f < a<VAR>hb : limsup v f < b<GOAL>limsup (u + v) f < a + b
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup u f < a<VAR>hb : limsup v f < b<VAR>c : EReal<VAR>hc : limsup u f < c<VAR>hca : c < a<GOAL>limsup (u + v) f < a + b
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup u f < a<VAR>hb : limsup v f < b<VAR>c : EReal<VAR>hc : limsup u f < c<VAR>hca : c < a<VAR>d : EReal<VAR>hd : limsup v f < d<VAR>hdb : d < b<GOAL>limsup (u + v) f < a + b
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>Injective R (CharacterModule M) ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → Function.Injective ⇑(rTensor M L)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>(∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y] (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X) (x_1 : M), (h (f x)) x_1 = (g x) x_1) ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → ∀ (b : N →ₗ[R] CharacterModule M), ∃ a, ∀ (x : N) (x_1 : M), (((lcomp R (CharacterModule M) L) a) x) x_1 = (b x) x_1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>Chain r ↑[a] ↔ r a a
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>multichoose (-↑n) (n + 1) = 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>(fun x => ?m.78773.factorial • x) (multichoose (-↑n) (n + 1)) = (fun x => ?m.78773.factorial • x) 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>?m.78773.factorial • multichoose (-↑n) (n + 1) = ?m.78773.factorial • 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>inst✝ : NoZeroDivisors R<VAR>n : ℤ<VAR>hn : 1 < n.natAbs<VAR>h : ↑n ≠ 0<GOAL>0 < (W.ΨSq n).natDegree
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit c<GOAL>a = b / c ↔ a * c = b
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v✝ : E<VAR>v : ↑(sphere 0 1)<GOAL>↑(stereographic ⋯) (-v) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∉ s<VAR>hb : b ∉ s<GOAL>{ ofColex := insert a s } < { ofColex := insert b s } ↔ a < b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝²⁰ : CommSemiring R<VAR>inst✝¹⁹ : AddCommMonoid M<VAR>inst✝¹⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁷ : CommRing R₁<VAR>inst✝¹⁶ : AddCommGroup M₁<VAR>inst✝¹⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : AddCommGroup V<VAR>inst✝¹² : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝¹¹ : AddCommMonoid M'✝<VAR>inst✝¹⁰ : AddCommMonoid M''<VAR>inst✝⁹ : Module R M'✝<VAR>inst✝⁸ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : FiniteDimensional K V<VAR>ι✝ : Type u_10<VAR>inst✝⁴ : DecidableEq ι✝<VAR>inst✝³ : Finite ι✝<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB' : B.IsSymm<VAR>ι : Type u_11<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : FiniteDimensional K V<VAR>b : Basis ι K V<GOAL>B.dualBasis hB (B.dualBasis hB b) = b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝²⁰ : CommSemiring R<VAR>inst✝¹⁹ : AddCommMonoid M<VAR>inst✝¹⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁷ : CommRing R₁<VAR>inst✝¹⁶ : AddCommGroup M₁<VAR>inst✝¹⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : AddCommGroup V<VAR>inst✝¹² : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝¹¹ : AddCommMonoid M'✝<VAR>inst✝¹⁰ : AddCommMonoid M''<VAR>inst✝⁹ : Module R M'✝<VAR>inst✝⁸ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : FiniteDimensional K V<VAR>ι✝ : Type u_10<VAR>inst✝⁴ : DecidableEq ι✝<VAR>inst✝³ : Finite ι✝<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB' : B.IsSymm<VAR>ι : Type u_11<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : FiniteDimensional K V<VAR>b : Basis ι K V<GOAL>B = B.flip
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<GOAL>s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<VAR>h : s ⊂ t<GOAL>∃ a ∈ t, s ⊆ t.erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b : α<VAR>s t : Finset α<VAR>h : s ⊂ t<VAR>a : α<VAR>ht : a ∈ t<VAR>hs : a ∉ s<GOAL>∃ a ∈ t, s ⊆ t.erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : Fintype ι<VAR>f : ι → α<GOAL>Independent f ↔ Finset.univ.SupIndep f
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Preorder α<VAR>a b✝ c : α<VAR>inst✝ : NoMinOrder α<VAR>b : α<GOAL>⋃ a, Ioo a b = Iio b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>f : G ≃* N<VAR>K : Subgroup G<VAR>x : N<GOAL>x ∈ map f.toMonoidHom K ↔ f.symm x ∈ K
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>f : G ≃* N<VAR>K : Subgroup G<VAR>x : N<GOAL>f.symm x ∈ ↑K ↔ f.symm x ∈ K
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>f : R[X]<VAR>inst✝ : IsDomain R<VAR>h : f.degree ≠ 0<GOAL>span {f} ≠ ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>f : R[X]<VAR>inst✝ : IsDomain R<VAR>h : f.degree ≠ 0<GOAL>∀ (x : R), IsUnit x → ¬C x = f
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : R<VAR>hx : IsUnit x<VAR>h : (C x).degree ≠ 0<GOAL>False