ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>φ₀ : E →L[𝕜] F<VAR>hφ₀ : φ₀ ∈ {L | Injective ⇑L}<VAR>K : ℝ≥0<VAR>K_pos : K > 0<VAR>H : AntilipschitzWith K ⇑↑φ₀<VAR>this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹<VAR>φ : E →L[𝕜] F<VAR>hφ : ‖φ - φ₀‖₊ < K⁻¹<GOAL>∃ K > 0, AntilipschitzWith K ⇑↑φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<GOAL>‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<VAR>this : edist y₀ (↑(approxOn f hf s y₀ h₀ n) x) ≤ edist y₀ (f x) + edist y₀ (f x)<GOAL>‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<VAR>this : ↑‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖₊ ≤ ↑‖f x - y₀‖₊ + ↑‖f x - y₀‖₊<GOAL>‖↑(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>orthogonalProjectionFn s p ∈ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑s ∩ ↑(mk' p s.directionᗮ) ⊆ ↑s
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<GOAL>Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<GOAL>Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<GOAL>Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<GOAL>Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<VAR>key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := let_fun this := algHomEquivSigma; this<GOAL>Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<VAR>key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := let_fun this := algHomEquivSigma; this<VAR>this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)<GOAL>Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<VAR>key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := let_fun this := algHomEquivSigma; this<VAR>this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)<GOAL>∑ i : K →ₐ[F] E, Fintype.card (↥K⟮x⟯ →ₐ[K] E) = Fintype.card (K →ₐ[F] E) * (minpoly K x).natDegree
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<VAR>key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := let_fun this := algHomEquivSigma; this<VAR>this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)<GOAL>∀ x_1 ∈ Finset.univ, Fintype.card (↥K⟮x⟯ →ₐ[K] E) = (minpoly K x).natDegree
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<VAR>key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := let_fun this := algHomEquivSigma; this<VAR>this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)<VAR>f : K →ₐ[F] E<VAR>a✝ : f ∈ Finset.univ<GOAL>Fintype.card (↥K⟮x⟯ →ₐ[K] E) = (minpoly K x).natDegree
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<VAR>key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := let_fun this := algHomEquivSigma; this<VAR>this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)<VAR>f : K →ₐ[F] E<VAR>a✝ : f ∈ Finset.univ<GOAL>Fintype.card (↥K⟮x⟯ →ₐ[K] E) = Fintype.card (↥K⟮x⟯ →ₐ[K] E)
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<VAR>key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := let_fun this := algHomEquivSigma; this<VAR>this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)<VAR>f : K →ₐ[F] E<VAR>a✝ : f ∈ Finset.univ<GOAL>IsSeparable K x
<VAR>F : Type u_1<VAR>inst✝⁸ : Field F<VAR>E : Type u_2<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>p : F[X]<VAR>hFE : FiniteDimensional F E<VAR>sp : Polynomial.IsSplittingField F E p<VAR>hp : p.Separable<VAR>K : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsScalarTower F K E<VAR>x : E<VAR>hx : x ∈ p.aroots E<VAR>inst✝¹ : Fintype (K →ₐ[F] E)<VAR>inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)<VAR>h : IsIntegral K x<VAR>h1 : p ≠ 0<VAR>h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p<VAR>key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := let_fun this := algHomEquivSigma; this<VAR>this : (f : K →ₐ[F] E) → Fintype (↥K⟮x⟯ →ₐ[K] E)<VAR>f : K →ₐ[F] E<VAR>a✝ : f ∈ Finset.univ<GOAL>Polynomial.Splits (algebraMap K E) (minpoly K x)
<VAR>p n k b : ℕ<VAR>hp : Prime p<VAR>hnb : log p (n + k) < b<GOAL>multiplicity p ((n + k).choose k) = ↑(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b)).card
<VAR>p n k b : ℕ<VAR>hp : Prime p<VAR>hnb : log p (n + k) < b<VAR>h₁ : multiplicity p ((n + k).choose k) + multiplicity p (k ! * n !) = ↑(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b)).card + multiplicity p (k ! * n !)<GOAL>multiplicity p ((n + k).choose k) = ↑(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b)).card
<VAR>p n k b : ℕ<VAR>hp : Prime p<VAR>hnb : log p (n + k) < b<VAR>h₁ : multiplicity p ((n + k).choose k) + multiplicity p (k ! * n !) = ↑(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b)).card + multiplicity p (k ! * n !)<GOAL>multiplicity p (k ! * n !) ≠ ⊤
<VAR>p n k b : ℕ<VAR>hp : Prime p<VAR>hnb : log p (n + k) < b<VAR>h₁ : multiplicity p ((n + k).choose k) + multiplicity p (k ! * n !) = ↑(filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Ico 1 b)).card + multiplicity p (k ! * n !)<GOAL>(multiplicity p (k ! * n !)).Dom
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf_int : Integrable f μ<GOAL>Integrable (fun ω => ∫ (y : Ω), f y ∂(condexpKernel μ m) ω) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf_int : Integrable f μ<GOAL>Integrable (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t t' : Finset β<VAR>ht : Disjoint t t'<GOAL>Disjoint (interedges r s t) (interedges r s t')
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t t' : Finset β<VAR>ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'<GOAL>∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s t'
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t t' : Finset β<VAR>ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'<VAR>a✝ : α × β<VAR>hx : a✝ ∈ interedges r s t<VAR>hy : a✝ ∈ interedges r s t'<GOAL>False
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t t' : Finset β<VAR>ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'<VAR>a✝ : α × β<VAR>hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2<VAR>hy : a✝.1 ∈ s ∧ a✝.2 ∈ t' ∧ r a✝.1 a✝.2<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝¹ : MonoidWithZero R<VAR>inst✝ : Nontrivial R<GOAL>0 < nilpotencyClass x ↔ IsNilpotent x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝¹ : MonoidWithZero R<VAR>inst✝ : Nontrivial R<VAR>hx : IsNilpotent x<VAR>hx' : nilpotencyClass x = 0<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝¹ : MonoidWithZero R<VAR>inst✝ : Nontrivial R<VAR>hx' : nilpotencyClass x = 0<VAR>hx : x ^ nilpotencyClass x = 0<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝¹ : MonoidWithZero R<VAR>inst✝ : Nontrivial R<VAR>hx' : nilpotencyClass x = 0<VAR>hx : 1 = 0<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>h : PreconnectedSpace ↑s<GOAL>IsPreconnected s
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<GOAL>IsOpen (imageOfDf f)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<GOAL>IsOpen (⋃ i, {x | f.coeff i ∉ x.asIdeal})
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f σ : Perm α<VAR>l : List (Perm α)<VAR>hn : l.Nodup<GOAL>σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f σ : Perm α<VAR>l : List (Perm α)<VAR>hn : l.Nodup<VAR>l' : List (Perm α)<VAR>hp' : l'.prod = σ<VAR>hc' : ∀ g ∈ l', g.IsCycle<VAR>hd' : List.Pairwise Disjoint l'<VAR>hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors<GOAL>σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f σ : Perm α<VAR>l : List (Perm α)<VAR>hn : l.Nodup<VAR>l' : List (Perm α)<VAR>hp' : l'.prod = σ<VAR>hc' : ∀ g ∈ l', g.IsCycle<VAR>hd' : List.Pairwise Disjoint l'<VAR>hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors<VAR>ht : σ.cycleFactorsFinset = l'.toFinset<GOAL>σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
<VAR>q : ℚ<VAR>num : ℤ<VAR>den : ℕ<VAR>hd : den ≠ 0<VAR>hdn : num.natAbs.Coprime den<VAR>n : ℕ<GOAL>den ^ n ≠ 0
<VAR>q : ℚ<VAR>num : ℤ<VAR>den : ℕ<VAR>hd : den ≠ 0<VAR>hdn : num.natAbs.Coprime den<VAR>n : ℕ<GOAL>(num ^ n).natAbs.Coprime (den ^ n)
<VAR>q : ℚ<VAR>num : ℤ<VAR>den : ℕ<VAR>hd : den ≠ 0<VAR>hdn : num.natAbs.Coprime den<VAR>n : ℕ<GOAL>(num.natAbs ^ n).Coprime (den ^ n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : CompactSpace X<VAR>S : Set X<VAR>hS : IsClosed S<VAR>hne : S.Nonempty<VAR>opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}<VAR>U : Set X<VAR>h : ∀ a ∈ opens, U ⊆ a → a = U<VAR>Uc : Sᶜ ⊆ U<VAR>Uo : IsOpen U<VAR>Ucne : Uᶜ.Nonempty<GOAL>∃ V ⊆ S, V.Nonempty ∧ IsClosed V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : CompactSpace X<VAR>S : Set X<VAR>hS : IsClosed S<VAR>hne : S.Nonempty<VAR>opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}<VAR>U : Set X<VAR>h : ∀ a ∈ opens, U ⊆ a → a = U<VAR>Uc : Sᶜ ⊆ U<VAR>Uo : IsOpen U<VAR>Ucne : Uᶜ.Nonempty<GOAL>∀ V' ⊆ Uᶜ, V'.Nonempty → IsClosed V' → V' = Uᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : CompactSpace X<VAR>S : Set X<VAR>hS : IsClosed S<VAR>hne : S.Nonempty<VAR>opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}<VAR>U : Set X<VAR>h : ∀ a ∈ opens, U ⊆ a → a = U<VAR>Uc : Sᶜ ⊆ U<VAR>Uo : IsOpen U<VAR>Ucne : Uᶜ.Nonempty<VAR>V' : Set X<VAR>V'sub : V' ⊆ Uᶜ<VAR>V'ne : V'.Nonempty<VAR>V'cls : IsClosed V'<VAR>this : V'ᶜ = U<GOAL>V' = Uᶜ
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>n ≤ l.length → l.rotate n = drop n l ++ take n l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>n ≤ l.length → l.rotate' n = drop n l ++ take n l
<VAR>α : Type u<VAR>b : Ultrafilter α<GOAL>Tendsto pure (↑b) (𝓝 b)
<VAR>α : Type u<VAR>b : Ultrafilter α<GOAL>b = joinM (map pure b)
<VAR>α : Type u<VAR>b : Ultrafilter α<VAR>s : Set α<GOAL>s ∈ b ↔ {t | s ∈ t} ∈ map pure b
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β → α<VAR>a : α<VAR>bs : List β<GOAL>foldlIdx f a bs = foldl (fun a p => f p.1 a p.2) a bs.enum
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>a' : ℝ<VAR>haa' : a < a'<VAR>ha' : 0 < a'<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>a' : ℝ<VAR>haa' : a < a'<VAR>ha' : 0 < a'<VAR>fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>a' : ℝ<VAR>haa' : a < a'<VAR>ha' : 0 < a'<VAR>fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0<VAR>fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>a' : ℝ<VAR>haa' : a < a'<VAR>ha' : 0 < a'<VAR>fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0<VAR>fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹<VAR>hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>a' : ℝ<VAR>haa' : a < a'<VAR>ha' : 0 < a'<VAR>fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0<VAR>fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹<VAR>hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x<VAR>hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>a' : ℝ<VAR>haa' : a < a'<VAR>ha' : 0 < a'<VAR>fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0<VAR>fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹<VAR>hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x<VAR>hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x<VAR>this : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[>] 0) l<GOAL>Tendsto (fun x => f x / g x) atTop l