ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>𝕜' : Type u_6<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>f : F<GOAL>HasFDerivWithinAt (fun y => c y • f) (c'.smulRight f) s x
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Module A M<VAR>inst✝ : Module A M'<VAR>b : Basis ι A M<VAR>b' : Basis ι A M'<VAR>f : M →ₗ[A] M'<GOAL>b'.det (⇑f ∘ ⇑b) = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Module A M<VAR>inst✝ : Module A M'<VAR>b : Basis ι A M<VAR>b' : Basis ι A M'<VAR>f : M →ₗ[A] M'<GOAL>(b'.toMatrix (⇑f ∘ ⇑b)).det = ((LinearMap.toMatrix b b') f).det
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Module A M<VAR>inst✝ : Module A M'<VAR>b : Basis ι A M<VAR>b' : Basis ι A M'<VAR>f : M →ₗ[A] M'<VAR>i j : ι<GOAL>b'.toMatrix (⇑f ∘ ⇑b) i j = (LinearMap.toMatrix b b') f i j
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<VAR>hxy : basisDivisor x y = 0<GOAL>x = y
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<VAR>hxy : x = y<GOAL>x = y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ Type w<VAR>a : C<VAR>x : F.obj a<VAR>y : G.obj a<GOAL>Limits.prod.fst.app a (prodMk x y) = x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β : κ<GOAL>traceMatrix A (b ᵥ* P.map ⇑(algebraMap A B)) α β = (Pᵀ * traceMatrix A b * P) α β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β : κ<GOAL>∑ y : κ, ∑ x : κ, ((traceForm A B) (b x * P.map (⇑(algebraMap A B)) x α)) (b y * P.map (⇑(algebraMap A B)) y β) = ∑ j : κ, (Pᵀ * traceMatrix A b) α j * P j β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β x : κ<GOAL>∑ x_1 : κ, ((traceForm A B) (b x_1 * P.map (⇑(algebraMap A B)) x_1 α)) (b x * P.map (⇑(algebraMap A B)) x β) = (Pᵀ * traceMatrix A b) α x * P x β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β x : κ<GOAL>∑ x_1 : κ, ((traceForm A B) (b x_1 * P.map (⇑(algebraMap A B)) x_1 α)) (b x * P.map (⇑(algebraMap A B)) x β) = ∑ i : κ, Pᵀ α i * traceMatrix A b i x * P x β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β x y : κ<GOAL>((traceForm A B) (b y * P.map (⇑(algebraMap A B)) y α)) (b x * P.map (⇑(algebraMap A B)) x β) = Pᵀ α y * traceMatrix A b y x * P x β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β x y : κ<GOAL>(trace A B) (P y α • b y * (b x * P.map (⇑(algebraMap A B)) x β)) = Pᵀ α y * traceMatrix A b y x * P x β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β x y : κ<GOAL>P y α * (trace A B) (b y * (b x * (algebraMap A B) (P x β))) = P y α * traceMatrix A b y x * P x β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β x y : κ<GOAL>P y α * (trace A B) (b y * P x β • b x) = P y α * traceMatrix A b y x * P x β
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : CommRing S<VAR>inst✝¹⁷ : CommRing T<VAR>inst✝¹⁶ : Algebra R S<VAR>inst✝¹⁵ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹¹ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁰ : Field F<VAR>inst✝⁹ : Algebra R L<VAR>inst✝⁸ : Algebra L F<VAR>inst✝⁷ : Algebra R F<VAR>inst✝⁶ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<VAR>α β x y : κ<GOAL>P y α * (trace A B) (b y * P x β • b x) = P y α * (traceMatrix A b y x * P x β)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>hab : a < b<GOAL>∀ᵐ (ω : Ω) ∂μ, upcrossings a b f ω < ⊤
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>hab : a < b<GOAL>∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ⊤
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>hab : a < b<VAR>this : ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ<GOAL>∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ⊤
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>hab : a < b<VAR>this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)<GOAL>∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ⊤
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>hab : a < b<VAR>this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ<GOAL>ENNReal.ofReal (b - a) ≠ 0 ∨ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>hab : a < b<VAR>this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ<GOAL>ENNReal.ofReal (b - a) ≠ ⊤ ∨ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ ⊤
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>x' : M<VAR>y : M'<VAR>hx : x' ∈ (chartAt H x).source<VAR>hy : f x' ∈ (chartAt H' y).source<GOAL>ContinuousWithinAt f univ x' ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I) (↑(extChartAt I x) x') ↔ ContinuousAt f x' ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ range (2 ^ n), f k ≤ f 0 + ∑ k ∈ range n, 2 ^ k • f (2 ^ k)
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ range (2 ^ n), f k = f 0 + ∑ k ∈ Ico 1 (2 ^ n), f k
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : F<VAR>t : R<GOAL>Continuous ⇑(homothety x t)
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : F<VAR>t : R<GOAL>⇑(homothety x t) = fun y => t • (y - x) + x
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : F<VAR>t : R<VAR>y : F<GOAL>(homothety x t) y = t • (y - x) + x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>f' g' : E →L[ℂ] ℂ<VAR>x : E<VAR>s : Set E<VAR>c : ℂ<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hg : HasFDerivWithinAt g g' s x<VAR>h0 : f x ∈ slitPlane<GOAL>HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>m n : ZNum<GOAL>↑m < ↑n ↔ m < n
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 F<VAR>t : TopologicalSpace F<VAR>inst✝ : LocallyConvexSpace 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>this : TopologicalSpace E := induced (⇑f) t<GOAL>LocallyConvexSpace 𝕜 E
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 F<VAR>t : TopologicalSpace F<VAR>inst✝ : LocallyConvexSpace 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>this : TopologicalSpace E := induced (⇑f) t<VAR>x : E<GOAL>(𝓝 x).HasBasis ((fun x s => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ⇑f) x)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 F<VAR>t : TopologicalSpace F<VAR>inst✝ : LocallyConvexSpace 𝕜 F<VAR>f : E →ₗ[𝕜] F<VAR>this : TopologicalSpace E := induced (⇑f) t<VAR>x : E<GOAL>(comap (⇑f) (𝓝 (f x))).HasBasis ((fun x s => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ⇑f) x)
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>(X ^ n + C a).degree ≠ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>↑n ≠ ⊥
<VAR>n : ℕ<VAR>b : Bool<GOAL>bit b n = 0 ↔ n = 0 ∧ b = false
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>inst✝ : InvariantBasisNumber R<GOAL>Nontrivial R
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>inst✝ : InvariantBasisNumber R<VAR>h : ¬Nontrivial R<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>inst✝ : InvariantBasisNumber R<VAR>h : ¬Nontrivial R<GOAL>(Fin 0 → R) ≃ₗ[R] Fin 1 → R
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>inst✝ : InvariantBasisNumber R<VAR>h : ¬Nontrivial R<VAR>this : Subsingleton R<GOAL>(Fin 0 → R) ≃ₗ[R] Fin 1 → R
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>inst✝ : InvariantBasisNumber R<VAR>h : ¬Nontrivial R<VAR>this✝ : Subsingleton R<VAR>this : Subsingleton (Fin 1 → R)<GOAL>(Fin 0 → R) ≃ₗ[R] Fin 1 → R
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>hurwitzZetaEven (↑x) (1 - 2 * ↑k) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n<GOAL>hurwitzZetaEven (↑x) (1 - 2 * ↑k) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n<VAR>h2 : 2 * ↑k ≠ 1<GOAL>hurwitzZetaEven (↑x) (1 - 2 * ↑k) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n<VAR>h2 : 2 * ↑k ≠ 1<VAR>h3 : (2 * ↑k).Gammaℂ ≠ 0<GOAL>hurwitzZetaEven (↑x) (1 - 2 * ↑k) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n<VAR>h2 : 2 * ↑k ≠ 1<VAR>h3 : (2 * ↑k).Gammaℂ ≠ 0<GOAL>Complex.cos (↑π * (2 * ↑k) / 2) * (-1) ^ (k + 1) / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n<VAR>h2 : 2 * ↑k ≠ 1<VAR>h3 : (2 * ↑k).Gammaℂ ≠ 0<GOAL>Complex.cos (↑π * (2 * ↑k) / 2) * (-1) ^ (k + 1) = -1
<VAR>K : Type u_1<VAR>L : Type ?u.603122<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>h_eq : p = q<GOAL>(algEquivOfEq hp h_eq) (root p) = root q
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝ : MetricSpace P<VAR>s₁ s₂ : Sphere P<GOAL>s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<GOAL>Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 (a - 0))<GOAL>Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)<GOAL>Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)<GOAL>∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)<GOAL>∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>n ≤ s.card ↔ ∃ t ⊆ s, t.card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>h : n ≤ s.card<GOAL>∃ t ⊆ s, t.card = n
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>f : MultilinearMap R M₁ M₂<VAR>x y : (i : ι) → M₁ i<GOAL>(∑ i : ι, f.toLinearMap x i ∘ₗ LinearMap.proj i) y = ∑ i : ι, f (update x i (y i))
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>single (f ≫ g) 1 = single f 1 ≫ single g 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>x : α<GOAL>↑(⌊x⌋ + 1) - 1 ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>x : α<GOAL>↑⌊x⌋ ≤ x