ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : NonAssocSemiring A<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : SMulCommClass R A A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : NonAssocSemiring B<VAR>inst✝² : Module R B<VAR>inst✝¹ : SMulCommClass R B B<VAR>inst✝ : IsScalarTower R B B<VAR>x : A ⊗[R] B<GOAL>(mul (1 ⊗ₜ[R] 1)) x = x
<VAR>x y : ZFSet<GOAL>(∃ z, ↑x z ∧ y ∈ z) ↔ ∃ z ∈ x, y ∈ z
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>Set.Sized (r - k) ↑(∂ ^[k] 𝒜)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>∀ ⦃x : Finset α⦄, (∃ s ∈ 𝒜, x ⊆ s ∧ (s \ x).card = k) → x.card = r - k
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>t s : Finset α<VAR>hs : s ∈ 𝒜<VAR>hts : t ⊆ s<GOAL>t.card = r - (s \ t).card
<VAR>ι✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b✝ : ι✝ → M<VAR>ι : Type u_4<VAR>inst✝ : Finite ι<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>this : DecidableEq M<GOAL>∃ n, Nonempty (Basis (Fin n) R ↥N)
<VAR>ι✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b✝ : ι✝ → M<VAR>ι : Type u_4<VAR>inst✝ : Finite ι<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>this : DecidableEq M<VAR>val✝ : Fintype ι<GOAL>∃ n, Nonempty (Basis (Fin n) R ↥N)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : ContDiffWithinAt 𝕜 n f s x₀<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hmn : m + 1 ≤ n<VAR>hx₀s : x₀ ∈ s<GOAL>s ⊆ (fun x => x) ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>x : E<VAR>c : 𝕜<GOAL>‖(toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>x : E<VAR>c : 𝕜<GOAL>‖(toSpanSingleton 𝕜 E x) c‖ = ‖c‖ * ‖x‖
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g✝ f g : Perm α<VAR>x : α<GOAL>x ∈ (f * g).support → x ∈ f.support ⊔ g.support
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g✝ f g : Perm α<VAR>x : α<GOAL>x ∈ (f * g).support → x ∈ f.support ∪ g.support
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g✝ f g : Perm α<VAR>x : α<GOAL>f x = x ∧ g x = x → f (g x) = x
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroDivisors R<VAR>q : ℕ<VAR>inst✝ : ExpChar R q<GOAL>0 < q
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroDivisors R<VAR>q : ℕ<VAR>inst✝ : ExpChar R q<VAR>h : Nat.Prime q<GOAL>0 < q
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : ExpChar R 1<GOAL>0 < 1
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * -sinZeta a s)) / (2 * I)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>x₀ : G<VAR>h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)<VAR>v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)<GOAL>ConvolutionExistsAt f g x₀ L μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>x₀ : G<VAR>h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)<VAR>v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)<GOAL>AEStronglyMeasurable g (Measure.map (fun t => ↑(toAddUnits x₀) - t) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t)))))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>x₀ : G<VAR>h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)<VAR>v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)<VAR>A : AEStronglyMeasurable (g ∘ ⇑v) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t))))<GOAL>AEStronglyMeasurable g (Measure.map (fun t => ↑(toAddUnits x₀) - t) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t)))))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>x₀ : G<VAR>h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)<VAR>v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)<VAR>A : AEStronglyMeasurable (g ∘ ⇑v) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t))))<VAR>x✝ : G<GOAL>HSub.hSub ↑(toAddUnits x₀) = ⇑v
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝¹ x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>x₀ : G<VAR>h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>u : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)<VAR>v : G ≃ₜ G := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)<VAR>A : AEStronglyMeasurable (g ∘ ⇑v) (μ.restrict (tsupport fun t => (L (f t)) (g (x₀ - t))))<VAR>x✝ x : G<GOAL>↑(toAddUnits x₀) - x = v x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : z ≠ 0<GOAL>x = y ^ z⁻¹ ↔ x ^ z = y
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : z ≠ 0<GOAL>0 ≤ y ^ z⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioc a b \ Iic c = Ioc (max a c) b
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>g : E → F<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : E<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => (f y) (g y)) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>g : E → F<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : E<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) (g y)) univ x‖ ≤ ∑ x_1 ∈ Finset.range (n + 1), ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<GOAL>‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>m : Fin n.succ → A<GOAL>‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) m‖ ≤ 1 * ∏ i : Fin n.succ, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>m : Fin n.succ → A<GOAL>‖(List.map m (List.finRange n.succ)).prod‖ ≤ (List.map (fun i => ‖m i‖) (List.finRange n.succ)).prod
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>m : Fin n.succ → A<GOAL>List.map m (List.finRange n.succ) ≠ []
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : SeminormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜 G'<VAR>n : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>m : Fin n.succ → A<GOAL>(List.map norm (List.map m (List.finRange n.succ))).prod = (List.map (fun i => ‖m i‖) (List.finRange n.succ)).prod
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>_h : 0 < 1<GOAL>‖newton_seq 1 - a‖ = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>k : ℕ<VAR>_h : 0 < k + 2<GOAL>‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>k : ℕ<VAR>_h : 0 < k + 2<GOAL>‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>k : ℕ<VAR>_h : 0 < k + 2<GOAL>Polynomial.eval a F ≠ 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>k : ℕ<VAR>_h : 0 < k + 2<VAR>hlt : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖<VAR>hne' : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ ≠ ‖newton_seq (k + 1) - a‖<GOAL>‖newton_seq (k + 2) - a‖ = ‖newton_seq (k + 2) - newton_seq (k + 1) + (newton_seq (k + 1) - a)‖
<VAR>α : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < 4
<VAR>α : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 < 3 + 1
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q a : R[X]<GOAL>a.toFinsupp = 0 ↔ a = 0
<VAR>a b c : ℕ<VAR>a1 : 1 < a<VAR>b1 : 1 < b<VAR>h : a ≡ b [MOD c]<GOAL>xn a1 1 ≡ xn b1 1 [MOD c] ∧ yn a1 1 ≡ yn b1 1 [MOD c]
<VAR>a b c : ℕ<VAR>a1 : 1 < a<VAR>b1 : 1 < b<VAR>h : a ≡ b [MOD c]<VAR>n : ℕ<GOAL>xn a1 (n + 2) + xn a1 n ≡ xn b1 (n + 2) + xn b1 n [MOD c]
<VAR>a b c : ℕ<VAR>a1 : 1 < a<VAR>b1 : 1 < b<VAR>h : a ≡ b [MOD c]<VAR>n : ℕ<GOAL>2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]
<VAR>a b c : ℕ<VAR>a1 : 1 < a<VAR>b1 : 1 < b<VAR>h : a ≡ b [MOD c]<VAR>n : ℕ<GOAL>yn a1 (n + 2) + yn ⋯ n ≡ yn b1 (n + 2) + yn ⋯ n [MOD c]
<VAR>a b c : ℕ<VAR>a1 : 1 < a<VAR>b1 : 1 < b<VAR>h : a ≡ b [MOD c]<VAR>n : ℕ<GOAL>2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>x✝ : V<GOAL>(o.rotation θ).symm x✝ = (o.rotation (-θ)) x✝
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>this : MeasurableSet {ω | τ ω ≤ π ω}<GOAL>MeasurableSet {ω | τ ω ≤ π ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>this : MeasurableSet {ω | τ ω ≤ π ω} ∧ MeasurableSet {ω | τ ω ≤ π ω}<GOAL>MeasurableSet {ω | τ ω ≤ π ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>MeasurableSet {ω | τ ω ≤ π ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>MeasurableSet (Set.univ ∩ {ω | τ ω ≤ π ω})
<VAR>a : EReal<GOAL>a * 0⁻¹ = 0
<VAR>R✝ : Type u<VAR>M✝ : Type v<VAR>N : Type w<VAR>inst✝¹⁰ : CommRing R✝<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>inst✝⁷ : Free R✝ M✝<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R✝ N<VAR>inst✝⁴ : Free R✝ N<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : _root_.Finite ι<VAR>b : Basis ι R M<GOAL>Finite R M
<VAR>R✝ : Type u<VAR>M✝ : Type v<VAR>N : Type w<VAR>inst✝¹⁰ : CommRing R✝<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>inst✝⁷ : Free R✝ M✝<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R✝ N<VAR>inst✝⁴ : Free R✝ N<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : _root_.Finite ι<VAR>b : Basis ι R M<VAR>val✝ : Fintype ι<GOAL>Finite R M
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<GOAL>variance X μ = ∫ (x : Ω), ((X - fun x => ∫ (x : Ω), X x ∂μ) ^ 2) x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<GOAL>∫ (x : Ω), (X x - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = ∫ (x : Ω), ((X - fun x => ∫ (x : Ω), X x ∂μ) ^ 2) x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<GOAL>Integrable (fun ω => (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<GOAL>0 ≤ᶠ[ae μ] fun ω => (X ω - ∫ (x : Ω), X x ∂μ) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>a : α<GOAL>𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>a : α<GOAL>(⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = (⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}) ⊓ ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>a : α<GOAL>⨅ b ∈ Iio a, 𝓟 (Ioi b) = ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>a : α<GOAL>⨅ b ∈ Ioi a, 𝓟 (Iio b) = ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>h : ∃ i, p i<VAR>f : ι → ℝ≥0∞<GOAL>(⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>h : ∃ i, p i<VAR>f : ι → ℝ≥0∞<VAR>this : Nonempty { i // p i }<GOAL>(⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a