ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.126940, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain F K m<VAR>β : Cochain G K n<VAR>h : m + 1 = n<VAR>n' : ℤ<VAR>hn' : n + 1 = n'<GOAL>δ n n' ((↑(fst φ)).comp α ⋯ + (snd φ).comp β ⋯) = (↑(fst φ)).comp (δ m n α + n'.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯ + (snd φ).comp (δ n n' β) ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.126940, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain F K m<VAR>β : Cochain G K n<VAR>h : m + 1 = n<VAR>n' : ℤ<VAR>hn' : n + 1 = n'<GOAL>(↑(fst φ)).comp (δ m n α) ⋯ + ((snd φ).comp (δ n n' β) ⋯ + -(n.negOnePow • (↑(fst φ)).comp ((Cochain.ofHom φ).comp β ⋯) ⋯)) = (↑(fst φ)).comp (δ m n α) ⋯ + -(n.negOnePow • (↑(fst φ)).comp ((Cochain.ofHom φ).comp β ⋯) ⋯) + (snd φ).comp (δ n n' β) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ f₃ : α → E'<VAR>h : (fun x => f₁ x - f₂ x) =o[l] g<GOAL>(fun x => f₂ x - f₁ x) =o[l] g
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : Monic 0<GOAL>p /ₘ 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>this✝ : DecidableEq R := Classical.decEq R<VAR>h : Monic 0<VAR>this : Subsingleton R<GOAL>p /ₘ 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬Monic 0<GOAL>(if h : Monic 0 then (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then let z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0); let_fun _wf := ⋯; let dm := (p - 0 * z).divModByMonicAux ⋯; (z + dm.1, dm.2) else (0, p)).1 else 0) = 0
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : E<VAR>hx : DifferentiableAt 𝕜 f x<VAR>δ : ℝ := ε / 2 / 2<GOAL>∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : E<VAR>hx : DifferentiableAt 𝕜 f x<VAR>δ : ℝ := ε / 2 / 2<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖<GOAL>∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : E<VAR>hx : DifferentiableAt 𝕜 f x<VAR>δ : ℝ := ε / 2 / 2<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 R<GOAL>x ∈ A f (fderiv 𝕜 f x) r ε
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : E<VAR>hx : DifferentiableAt 𝕜 f x<VAR>δ : ℝ := ε / 2 / 2<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 R<VAR>this : r ∈ Ioc (r / 2) r<GOAL>x ∈ A f (fderiv 𝕜 f x) r ε
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : E<VAR>hx : DifferentiableAt 𝕜 f x<VAR>δ : ℝ := ε / 2 / 2<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 R<VAR>this : r ∈ Ioc (r / 2) r<VAR>y : E<VAR>hy : y ∈ ball x r<VAR>z : E<VAR>hz : z ∈ ball x r<GOAL>‖f z - f y - (fderiv 𝕜 f x) (z - y)‖ < ε * r
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp1 : 1 ≤ p<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_top : ¬∫⁻ (a : α), g a ^ p ∂μ = ⊤<VAR>h1 : ¬p = 1<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_top : ¬∫⁻ (a : α), g a ^ p ∂μ = ⊤<VAR>h1 : ¬p = 1<VAR>hp1_lt : 1 < p<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_top : ¬∫⁻ (a : α), g a ^ p ∂μ = ⊤<VAR>h1 : ¬p = 1<VAR>hp1_lt : 1 < p<VAR>hpq : p.IsConjExponent p.conjExponent<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_top : ¬∫⁻ (a : α), g a ^ p ∂μ = ⊤<VAR>h1 : ¬p = 1<VAR>hp1_lt : 1 < p<VAR>hpq : p.IsConjExponent p.conjExponent<VAR>h0 : ¬∫⁻ (a : α), (f + g) a ^ p ∂μ = 0<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤<VAR>hg_top : ¬∫⁻ (a : α), g a ^ p ∂μ = ⊤<VAR>h1 : ¬p = 1<VAR>hp1_lt : 1 < p<VAR>hpq : p.IsConjExponent p.conjExponent<VAR>h0 : ¬∫⁻ (a : α), (f + g) a ^ p ∂μ = 0<VAR>htop : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<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>hg : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 g x
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>a ≤ a * a
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>this : a * 1 ≤ a * a<GOAL>a ≤ a * a
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d : ManyOneDegree<GOAL>d ≤ d
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>p✝ : Set ℕ<GOAL>of p✝ ≤ of p✝
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p✝ : R<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsIntegrallyClosed R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommSemiring A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>Q : A[X]<VAR>p : A<VAR>x z : B<VAR>hp : p ≠ 0<VAR>hz : (aeval x) Q = p • z<VAR>f : ℕ → A<VAR>hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i<GOAL>z ∈ adjoin A {x}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p✝ : R<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsIntegrallyClosed R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommSemiring A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>Q : A[X]<VAR>p : A<VAR>x z : B<VAR>hp : p ≠ 0<VAR>hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff ↑i • x ^ ↑i = p • z<VAR>f : ℕ → A<VAR>hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i<GOAL>z ∈ adjoin A {x}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p✝ : R<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsIntegrallyClosed R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommSemiring A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>Q : A[X]<VAR>p : A<VAR>x z : B<VAR>hp : p ≠ 0<VAR>f : ℕ → A<VAR>hz : ∑ i : Fin (Q.natDegree + 1), p • f ↑i • x ^ ↑i = p • z<VAR>hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i<GOAL>z ∈ adjoin A {x}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p✝ : R<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsIntegrallyClosed R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommSemiring A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>Q : A[X]<VAR>p : A<VAR>x z : B<VAR>hp : p ≠ 0<VAR>f : ℕ → A<VAR>hz : p • ∑ x_1 : Fin (Q.natDegree + 1), f ↑x_1 • x ^ ↑x_1 = p • z<VAR>hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i<GOAL>z ∈ adjoin A {x}
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p✝ : R<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : IsIntegrallyClosed R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommSemiring A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>Q : A[X]<VAR>p : A<VAR>x z : B<VAR>hp : p ≠ 0<VAR>f : ℕ → A<VAR>hz : p • ∑ x_1 : Fin (Q.natDegree + 1), f ↑x_1 • x ^ ↑x_1 = p • z<VAR>hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i<GOAL>∑ x_1 : Fin (Q.natDegree + 1), f ↑x_1 • x ^ ↑x_1 ∈ adjoin A {x}
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>a : R<GOAL>(vandermonde fun i => v i - a).det = (vandermonde v).det
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>a : R<GOAL>(vandermonde fun i => v i - a).det = (vandermonde fun i => v i + -a).det
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NoZeroDivisors α<VAR>s : Set α<VAR>a : α<VAR>ha : a ≠ 0<VAR>hs : ThreeGPFree (a • s)<VAR>b : α<VAR>hb : b ∈ s<VAR>c : α<VAR>hc : c ∈ s<VAR>d : α<VAR>hd : d ∈ s<VAR>h : b * d = c * c<GOAL>a • b * a • d = a * c * (a * c)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<GOAL>(C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆).natDegree ≤ 3
<VAR>m n : ℕ<VAR>f : Vector ℕ m → Vector ℕ n<VAR>h : Vec f<GOAL>Primrec f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝ : Fintype ι<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h's : Pairwise (Disjoint on s)<VAR>hf : ∀ (i : ι), IntegrableOn f (s i) μ<GOAL>∫ (x : X) in ⋃ i, s i, f x ∂μ = ∑ i : ι, ∫ (x : X) in s i, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝ : Fintype ι<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h's : Pairwise (Disjoint on s)<VAR>hf : ∀ (i : ι), IntegrableOn f (s i) μ<VAR>x✝ : ι<GOAL>s x✝ = ⋃ (_ : x✝ ∈ Finset.univ), s x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝ : Fintype ι<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h's : Pairwise (Disjoint on s)<VAR>hf : ∀ (i : ι), IntegrableOn f (s i) μ<GOAL>(↑Finset.univ).Pairwise (Disjoint on s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>x : R<VAR>f : R →+* S<VAR>h : f p.leadingCoeff ≠ 0<VAR>n✝ : ℕ<GOAL>(map f (p.scaleRoots x)).coeff n✝ = ((map f p).scaleRoots (f x)).coeff n✝
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>s : Set ι<GOAL>IsOpen (Sigma.fst ⁻¹' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>s : Set ι<GOAL>IsOpen (⋃ i ∈ s, Sigma.fst ⁻¹' {i})
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>s : Set ι<GOAL>IsOpen (⋃ i ∈ s, range (Sigma.mk i))
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>q : ℚ<GOAL>im ↑q = 0
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>h₁ : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)<VAR>x : S<VAR>hx : x ∈ quasispectrum S a<GOAL>(algebraMap R S) (f x) = x
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>h₁ : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)<VAR>hx : 0 ∈ quasispectrum S a<GOAL>(algebraMap R S) (f 0) = 0
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>h₁ : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)<VAR>x : S<VAR>hx✝ : x ∈ quasispectrum S a<VAR>hx : x ∈ spectrum S a<GOAL>(algebraMap R S) (f x) = x
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<GOAL>∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * (bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<GOAL>∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * (bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<GOAL>(fun x => x * ↑n) (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * (bernstein n ↑k) x) = (fun x => x * ↑n) (↑x * (1 - ↑x) / ↑n)
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<GOAL>(fun x => x * ↑n) ((fun x => x * ↑n) (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * (bernstein n ↑k) x)) = (fun x => x * ↑n) ((fun x => x * ↑n) (↑x * (1 - ↑x) / ↑n))
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<GOAL>(∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * (bernstein n ↑k) x) * ↑n * ↑n = ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<GOAL>∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<GOAL>∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<VAR>this : ∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν = n • Polynomial.X * (1 - Polynomial.X)<GOAL>∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<VAR>this : (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν) = (Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X))<GOAL>∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<VAR>h' : ↑n ≠ 0<VAR>this : ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)<GOAL>∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u v : α → ℝ<GOAL>(IsBigOWith c l f fun x => ‖g' x‖) ↔ IsBigOWith c l f g'
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Continuous ((fun φ => φ f) ∘ toWeakDualBCNN)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Continuous fun φ => φ f
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(n - m).gcd m = n.gcd m
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>n : ℕ<VAR>hn : n < hf.toFinset.card<GOAL>nth p n = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ<VAR>hδpos : 0 < δ<VAR>hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : Memℒp f p μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ<VAR>hδpos : 0 < δ<VAR>hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal δ<GOAL>2 * ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε