ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ<VAR>A : Set ℝ<VAR>A_finmeas : volume A ≠ ⊤<VAR>μ : ProbabilityMeasure Ω<GOAL>Tendsto (fun ε => ∫ (t : ℝ) in A, (↑(μ (thickening ε {a | t ≤ f a}))).toReal) (𝓝[>] 0) (𝓝 (∫ (t : ℝ) in A, (↑(μ {a | t ≤ f a})).toReal))
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ<VAR>A : Set ℝ<VAR>A_finmeas : volume A ≠ ⊤<VAR>μ : ProbabilityMeasure Ω<GOAL>∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (fun t => ↑(μ (thickening n {a | t ≤ f a}))) (volume.restrict A)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ<VAR>A : Set ℝ<VAR>A_finmeas : volume A ≠ ⊤<VAR>μ : ProbabilityMeasure Ω<GOAL>∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : ℝ) ∂volume.restrict A, ‖↑(μ (thickening n {a_1 | a ≤ f a_1}))‖ ≤ 1 a
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ<VAR>A : Set ℝ<VAR>A_finmeas : volume A ≠ ⊤<VAR>μ : ProbabilityMeasure Ω<GOAL>Integrable 1 (volume.restrict A)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ<VAR>A : Set ℝ<VAR>A_finmeas : volume A ≠ ⊤<VAR>μ : ProbabilityMeasure Ω<GOAL>∀ᵐ (a : ℝ) ∂volume.restrict A, Tendsto (fun n => ↑(μ (thickening n {a_1 | a ≤ f a_1}))) (𝓝[>] 0) (𝓝 ↑(μ {a_1 | a ≤ f a_1}))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A✝ B✝ : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>A B : Finset G<VAR>aG bG : G<VAR>aH bH : H<VAR>hae : f aG = aH<VAR>hbe : f bG = bH<VAR>huH : UniqueMul (image (⇑f) A) (image (⇑f) B) aH bH<VAR>huG : UniqueMul (filter (fun x => f x = aH) A) (filter (fun x => f x = bH) B) aG bG<VAR>a b : G<VAR>ha : a ∈ A<VAR>hb : b ∈ B<VAR>he : a * b = aG * bG<GOAL>a = aG ∧ b = bG
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A✝ B✝ : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>A B : Finset G<VAR>aG bG : G<VAR>aH bH : H<VAR>hae : f aG = aH<VAR>hbe : f bG = bH<VAR>huG : UniqueMul (filter (fun x => f x = aH) A) (filter (fun x => f x = bH) B) aG bG<VAR>a b : G<VAR>ha : a ∈ A<VAR>hb : b ∈ B<VAR>he : a * b = aG * bG<VAR>huH : f a * f b = aH * bH → f a = aH ∧ f b = bH<GOAL>a = aG ∧ b = bG
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A✝ B✝ : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>A B : Finset G<VAR>aG bG : G<VAR>aH bH : H<VAR>hae : f aG = aH<VAR>hbe : f bG = bH<VAR>huG : UniqueMul (filter (fun x => f x = aH) A) (filter (fun x => f x = bH) B) aG bG<VAR>a b : G<VAR>ha : a ∈ A<VAR>hb : b ∈ B<VAR>he : a * b = aG * bG<VAR>huH : aH * bH = aH * bH → f a = aH ∧ f b = bH<GOAL>a = aG ∧ b = bG
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A✝ B✝ : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>A B : Finset G<VAR>aG bG : G<VAR>aH bH : H<VAR>hae : f aG = aH<VAR>hbe : f bG = bH<VAR>huG : UniqueMul (filter (fun x => f x = aH) A) (filter (fun x => f x = bH) B) aG bG<VAR>a b : G<VAR>ha : a ∈ A<VAR>hb : b ∈ B<VAR>he : a * b = aG * bG<VAR>huH : aH * bH = aH * bH → f a = aH ∧ f b = bH<GOAL>a ∈ A ∧ f a = aH
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A✝ B✝ : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>A B : Finset G<VAR>aG bG : G<VAR>aH bH : H<VAR>hae : f aG = aH<VAR>hbe : f bG = bH<VAR>huG : UniqueMul (filter (fun x => f x = aH) A) (filter (fun x => f x = bH) B) aG bG<VAR>a b : G<VAR>ha : a ∈ A<VAR>hb : b ∈ B<VAR>he : a * b = aG * bG<VAR>huH : aH * bH = aH * bH → f a = aH ∧ f b = bH<GOAL>b ∈ B ∧ f b = bH
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hq : q ≠ 0<GOAL>(p.mod q).degree < q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hq : q ≠ 0<GOAL>(p.mod q).degree < (q * C q.leadingCoeff⁻¹).degree
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g✝ : E → F<VAR>f' f₀' f₁' g'✝ e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>g : F → G<VAR>g' : F →L[𝕜] G<VAR>hg : HasStrictFDerivAt g g' (f x)<VAR>hf : HasStrictFDerivAt f f' x<GOAL>(fun x => g' (((fun p => (f p.1, f p.2)) x).1 - ((fun p => (f p.1, f p.2)) x).2) - (g'.comp f') (x.1 - x.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2
<VAR>n m : ℕ<VAR>i : Fin (n + 2)<VAR>hi : i ≠ last (n + 1)<GOAL>(last n).predAbove i = i.castPred hi
<VAR>n m : ℕ<VAR>i : Fin (n + 2)<VAR>hi✝ : i ≠ last (n + 1)<VAR>hi : ∃ j, j.castSucc = i<GOAL>(last n).predAbove i = i.castPred hi✝
<VAR>n m : ℕ<VAR>y : Fin (n + 1)<VAR>hi : y.castSucc ≠ last (n + 1)<GOAL>(last n).predAbove y.castSucc = y.castSucc.castPred hi
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>Icc a b ⊆ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : StrictMonoOn f (Ici 0)<GOAL>StrictMono f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : StrictMonoOn f (Ici 0)<VAR>x : G<VAR>hx : x ∈ Iic 0<VAR>y : G<VAR>hy : y ∈ Iic 0<VAR>hxy : x < y<GOAL>-f y < -f x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : StrictMonoOn f (Ici 0)<VAR>x : G<VAR>hx : x ∈ Iic 0<VAR>y : G<VAR>hy : y ∈ Iic 0<VAR>hxy : x < y<GOAL>f (-y) < f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : DivisionSemiring α<VAR>inst✝ : Neg β<VAR>h : Antiperiodic f c<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Antiperiodic (fun x => f (x / a)) (c * a)
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y✝ : F<VAR>hx : x ≠ 0<VAR>y : F<VAR>hy : y ∈ {y | SameRay ℝ x y}<VAR>z : F<VAR>hz : z ∈ {y | SameRay ℝ x y}<VAR>h : ‖y‖ = ‖z‖<GOAL>y = z
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>hx : x ≠ 0<VAR>z : F<VAR>hz : z ∈ {y | SameRay ℝ x y}<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>hy : r • x ∈ {y | SameRay ℝ x y}<VAR>h : ‖r • x‖ = ‖z‖<GOAL>r • x = z
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>hx : x ≠ 0<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>hy : r • x ∈ {y | SameRay ℝ x y}<VAR>s : ℝ<VAR>hs : 0 ≤ s<VAR>hz : s • x ∈ {y | SameRay ℝ x y}<VAR>h : ‖r • x‖ = ‖s • x‖<GOAL>r • x = s • x
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>hx : x ≠ 0<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>hy : r • x ∈ {y | SameRay ℝ x y}<VAR>s : ℝ<VAR>hs : 0 ≤ s<VAR>hz : s • x ∈ {y | SameRay ℝ x y}<VAR>h : r = s<GOAL>r • x = s • x
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>fa : α → α<VAR>fb : β → β<VAR>g : α → β<VAR>hg : Measurable g<VAR>hfg : Semiconj g fa fb<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>fa ⁻¹' (g ⁻¹' s) = g ⁻¹' s
<VAR>p : ℕ →. Bool<VAR>n : ℕ<VAR>x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m<VAR>h₁ : true ∈ p n<VAR>h₂ : ∀ {m : ℕ}, m < n → false ∈ p m<GOAL>n ∈ rfind p
<VAR>p : ℕ →. Bool<VAR>n : ℕ<VAR>x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m<VAR>h₁ : true ∈ p n<VAR>h₂ : ∀ {m : ℕ}, m < n → false ∈ p m<VAR>m : ℕ<VAR>hm : m ∈ rfind p<GOAL>n ∈ rfind p
<VAR>p : ℕ →. Bool<VAR>n : ℕ<VAR>x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m<VAR>h₁ : true ∈ p n<VAR>h₂ : ∀ {m : ℕ}, m < n → false ∈ p m<VAR>m : ℕ<VAR>hm : m ∈ rfind p<VAR>h : m < n<GOAL>n ∈ rfind p
<VAR>p : ℕ →. Bool<VAR>n : ℕ<VAR>x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m<VAR>h₁ : true ∈ p n<VAR>h₂ : ∀ {m : ℕ}, m < n → false ∈ p m<VAR>m : ℕ<VAR>hm : m ∈ rfind p<VAR>h : m = n<GOAL>n ∈ rfind p
<VAR>p : ℕ →. Bool<VAR>n : ℕ<VAR>x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m<VAR>h₁ : true ∈ p n<VAR>h₂ : ∀ {m : ℕ}, m < n → false ∈ p m<VAR>m : ℕ<VAR>hm : m ∈ rfind p<VAR>h : n < m<GOAL>n ∈ rfind p
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<GOAL>IsUnit p
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<GOAL>IsUnit p
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑⟨c, c0⟩ • p<GOAL>IsUnit p
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p<GOAL>IsUnit p
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p<GOAL>IsUnit (?intro.intro.intro.intro.mk.x * p)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p<GOAL>K[X]
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p<GOAL>∃ r, IsUnit r ∧ C r = map (algebraMap R K) (C ((integerNormalization R⁰ p).content * ↑u))
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p<VAR>con : (algebraMap R K) ((integerNormalization R⁰ p).content * ↑u) = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p<VAR>con : (integerNormalization R⁰ p).content * ↑u = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : K[X]<VAR>h0 : p ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ p).primPart<VAR>u : Rˣ<VAR>hu : C ↑u = (integerNormalization R⁰ p).primPart<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p<VAR>con : p = 0 ∨ ↑u = 0<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a n : ℕ<VAR>ha : a ≠ 0<GOAL>p ^ n ∣ a ↔ n ≤ padicValNat p a
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>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>ρ : Measure (α × β)<GOAL>(map Prod.swap ρ).fst = ρ.snd
<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>ρ : Measure (α × β)<GOAL>map (Prod.fst ∘ Prod.swap) ρ = ρ.snd
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>h : B.SeparatingRight<GOAL>B.polar Set.univ = {0}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>h : B.SeparatingRight<GOAL>0 ∈ B.polar Set.univ ∧ ∀ x ∈ B.polar Set.univ, x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>h : B.SeparatingRight<VAR>y : F<VAR>hy : y ∈ B.polar Set.univ<VAR>x : E<GOAL>(B x) y = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>h : B.SeparatingRight<VAR>y : F<VAR>hy : y ∈ B.polar Set.univ<VAR>x : E<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>‖(B x) y‖ ≤ ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>h : B.SeparatingRight<VAR>y : F<VAR>hy : y ∈ B.polar Set.univ<VAR>x : E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>c : 𝕜<VAR>hc : 0 < ‖c‖<VAR>hcε : ‖c‖ < ε<GOAL>‖(B x) y‖ ≤ ε
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>(X * p).natDegree = p.natDegree + 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>hn : n ∈ (p * q).support<GOAL>p.trailingDegree + q.trailingDegree ≤ ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0<GOAL>p.trailingDegree + q.trailingDegree ≤ ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0<VAR>i j : ℕ<VAR>hij : (i, j) ∈ antidiagonal n<VAR>hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0<GOAL>p.trailingDegree + q.trailingDegree ≤ ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0<VAR>i j : ℕ<VAR>hij : (i, j) ∈ antidiagonal n<VAR>hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0<GOAL>↑(i, j).1 + ↑(i, j).2 = ↑n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<GOAL>G.IsLocalization (W fun x => x ∈ Set.range F.obj)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<GOAL>G.IsLocalization ((MorphismProperty.isomorphisms C).inverseImage G)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>hs : s.Subsingleton<GOAL>diam s = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g g' : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn g (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1<VAR>g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g g' : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn g (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1<VAR>g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y = (taylorWithinEval f n (Icc x₀ x) x x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g g' : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn g (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1<VAR>g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y = (taylorWithinEval f n (Icc x₀ x) x x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y<GOAL>f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g g' : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn g (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1<VAR>g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y = (f x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y<GOAL>f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g g' : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn g (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1<VAR>g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y = f x - taylorWithinEval f n (Icc x₀ x) x₀ x<GOAL>f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c < 0<GOAL>a ≤ b / c ↔ b ≤ a * c
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>(E.variableChange C).Δ'⁻¹ = C.u ^ 12 * E.Δ'⁻¹
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>f : α → β<VAR>h : Injective f<GOAL>map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>f : α → β<VAR>h : Injective f<GOAL>map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>f : α → β<VAR>h : Injective f<VAR>h2 : map f l₁ ⊆ map f l₂<VAR>x : α<VAR>hx : x ∈ l₁<GOAL>x ∈ l₂
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>f : α → β<VAR>h : Injective f<VAR>h2 : map f l₁ ⊆ map f l₂<VAR>x : α<VAR>hx : x ∈ l₁<VAR>x' : α<VAR>hx' : x' ∈ l₂<VAR>hxx' : f x' = f x<GOAL>x ∈ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁷ : Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A✝ A' B B' : C<VAR>inst✝⁶ : HasBinaryCoproduct A✝ B<VAR>inst✝⁵ : HasBinaryCoproduct A' B'<VAR>inst✝⁴ : HasBinaryCoproduct (F.obj A✝) (F.obj B)<VAR>inst✝³ : HasBinaryCoproduct (F.obj A') (F.obj B')<VAR>inst✝² : HasBinaryCoproducts C<VAR>inst✝¹ : HasBinaryCoproducts D<VAR>A : C<VAR>inst✝ : ∀ (B : C), IsIso (coprodComparison F A B)<GOAL>F ⋙ coprod.functor.obj (F.obj A) ≅ coprod.functor.obj A ⋙ F