ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>f : M →ₗ[R] M<GOAL>((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace = ((toMatrix c c) ((f ∘ₗ id) ∘ₗ id)).trace
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>f : M →ₗ[R] M<GOAL>((toMatrix c c) ((f ∘ₗ id) ∘ₗ id)).trace = ((toMatrix c c) f).trace
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>legendreSym p 1 = 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : Cofork f g<VAR>W : C<VAR>k l : s.pt ⟶ W<VAR>h : s.π ≫ k = s.π ≫ l<GOAL>s.ι.app zero ≫ k = s.ι.app zero ≫ l
<VAR>α : Type u<VAR>x y : FreeRing α<GOAL>↑(x - y) = ↑x - ↑y
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>W X Y Z : TopCat<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>hf : Inducing ⇑f<VAR>hg : Inducing ⇑g<GOAL>(W ⨯ Y).topologicalSpace_coe = induced (⇑(prod.map f g)) (X ⨯ Z).topologicalSpace_coe
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>W X Y Z : TopCat<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>hf : Inducing ⇑f<VAR>hg : Inducing ⇑g<GOAL>induced (⇑prod.fst) W.str ⊓ induced (⇑prod.snd) Y.str = induced (⇑prod.fst) (induced (⇑f) X.str) ⊓ induced (⇑prod.snd) (induced (⇑g) Z.str)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>W X Y Z : TopCat<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>hf : Inducing ⇑f<VAR>hg : Inducing ⇑g<GOAL>induced (⇑prod.fst) W.str ⊓ induced (⇑prod.snd) Y.str = induced (⇑prod.fst) W.topologicalSpace_coe ⊓ induced (⇑prod.snd) Y.topologicalSpace_coe
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℂ<GOAL>(𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>this : b ≠ 0<GOAL>(𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>this : b ≠ 0<VAR>h : (-↑π * b).re < 0<GOAL>(𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>this : b ≠ 0<VAR>h : (-↑π * b).re < 0<VAR>t : ℝ<GOAL>𝓕 (fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) t = 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>this : b ≠ 0<VAR>h : (-↑π * b).re < 0<VAR>t : ℝ<GOAL>∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + -↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) = 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>this✝ : b ≠ 0<VAR>h : (-↑π * b).re < 0<VAR>t : ℝ<VAR>this : ∀ (x : ℝ), ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x = -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0<GOAL>∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + -↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) = 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>this✝ : b ≠ 0<VAR>h : (-↑π * b).re < 0<VAR>t : ℝ<VAR>this : ∀ (x : ℝ), ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x = -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0<GOAL>(↑π / (↑π * b)) ^ (1 / 2) * cexp (0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b))) = 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
<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✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L✝ : E →L[𝕜] E' →L[𝕜] F<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>s : Set P<VAR>v : P → G<VAR>hv : ContDiffOn 𝕜 n v s<VAR>f : G → E<VAR>g : P → G → E'<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ univ)<GOAL>ContDiffOn 𝕜 n (fun x => (f ⋆[L, μ] g x) (v x)) s
<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✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L✝ : E →L[𝕜] E' →L[𝕜] F<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>s : Set P<VAR>v : P → G<VAR>hv : ContDiffOn 𝕜 n v s<VAR>f : G → E<VAR>g : P → G → E'<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ univ)<GOAL>s ⊆ (fun x => (_root_.id x, v x)) ⁻¹' s ×ˢ univ
<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✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L✝ : E →L[𝕜] E' →L[𝕜] F<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>s : Set P<VAR>v : P → G<VAR>hv : ContDiffOn 𝕜 n v s<VAR>f : G → E<VAR>g : P → G → E'<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ univ)<VAR>x : P<VAR>hx : x ∈ s<GOAL>x ∈ (fun x => (_root_.id x, v x)) ⁻¹' s ×ˢ univ
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>IsZero T.obj₃ ↔ IsIso T.mor₁
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>IsZero T.obj₃ ↔ IsZero T.invRotate.obj₁
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>IsZero T.obj₃ ↔ IsZero ((CategoryTheory.shiftFunctor C (-1)).obj T.obj₃)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : (i : ι) → AddZeroClass (β i)<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>f g : Π₀ (i : ι), β i<VAR>i✝ : ι<GOAL>(filter p (f + g)) i✝ = (filter p f + filter p g) i✝
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDerivWithin 𝕜 (n + 1) f s x) m = ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F) ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) x) m
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>m : Fin (n + 1) → E<GOAL>((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n)) = ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F) ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) x) m
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>x n : ℕ<VAR>h : x.Coprime n<GOAL>x ^ φ n ≡ 1 [MOD n]
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>x n : ℕ<VAR>h : x.Coprime n<GOAL>↑(x ^ φ n) = ↑1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>x n : ℕ<VAR>h : x.Coprime n<VAR>x' : (ZMod n)ˣ := unitOfCoprime x h<GOAL>↑(x ^ φ n) = ↑1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>x n : ℕ<VAR>h : x.Coprime n<VAR>x' : (ZMod n)ˣ := unitOfCoprime x h<VAR>this : x' ^ φ n = 1<GOAL>↑(x ^ φ n) = ↑1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>x n : ℕ<VAR>h : x.Coprime n<VAR>x' : (ZMod n)ˣ := unitOfCoprime x h<VAR>this : ↑(x' ^ φ n) = ↑1<GOAL>↑(x ^ φ n) = ↑1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<GOAL>(Finsupp.total ι M R ⇑b) (b.repr x) = x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<GOAL>↑b.repr.symm (b.repr x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<GOAL>s.encard ≤ ↑k ↔ s.Finite ∧ s.ncard ≤ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<GOAL>s.Finite → ((∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k) ↔ s.ncard ≤ k)
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<GOAL>(p ^ 0).smeval x = p.smeval x ^ 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<VAR>n : ℕ<GOAL>(p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>Disjoint (⋃₀ ↑I) (⋃₀ ↑(hC.diffFinset₀ hs hI))
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>Disjoint (⋃₀ ↑I) (s \ ⋃₀ ↑I)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y ε x : α<VAR>n : ℤ<VAR>h : ↑n < x<GOAL>↑↑n < x
<VAR>x y : ℝ<GOAL>1 ≤ √x ↔ 1 ≤ x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>r s : R<VAR>m : PolynomialModule R M<GOAL>{ toFun := fun p => Finsupp.sum p fun i m => r ^ i • m, map_add' := ⋯ }.toFun (s • m) = (RingHom.id R) s • { toFun := fun p => Finsupp.sum p fun i m => r ^ i • m, map_add' := ⋯ }.toFun m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>r s : R<VAR>m : PolynomialModule R M<GOAL>∀ (i : ℕ), r ^ i • 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>r s : R<VAR>m : PolynomialModule R M<GOAL>(Finsupp.sum m fun i c => r ^ i • s • c) = (RingHom.id R) s • { toFun := fun p => Finsupp.sum p fun i m => r ^ i • m, map_add' := ⋯ }.toFun m
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>H1 : UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (UniformFun.uniformSpace (↑K) α)<GOAL>UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>H1 : UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (UniformFun.uniformSpace (↑K) α)<VAR>H2 : UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α) = ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (Pi.uniformSpace fun i => α)<GOAL>UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>H1 : UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (UniformFun.uniformSpace (↑K) α)<VAR>H2 : UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α) = ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (Pi.uniformSpace fun i => α)<VAR>H3 : ∀ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (UniformFun.uniformSpace (↑K) α) = UniformSpace.comap (K.restrict ∘ F) (Pi.uniformSpace fun i => α)<GOAL>UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f : E → A<VAR>z : E<VAR>hf : AnalyticAt 𝕜 f z<VAR>n : ℕ<GOAL>AnalyticAt 𝕜 (fun x => f x ^ n) z
<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>f g : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n fun x => f x - g x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>s s' : Set A<GOAL>zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 ↑(Ideal.span s ⊓ Ideal.span s')
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>s s' : Set A<GOAL>zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 ↑(Ideal.span s) ∪ zeroLocus 𝒜 ↑(Ideal.span s')
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>d : σ →₀ ℕ<VAR>n : N<VAR>e : σ →₀ ℕ<GOAL>coeff e (((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap ∘ₗ monomial d) 1) n) = coeff e (((AlgebraTensorModule.curry ↑rTensor ∘ₗ monomial d) 1) n)
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>d : σ →₀ ℕ<VAR>n : N<VAR>e : σ →₀ ℕ<GOAL>coeff e (rTensorAlgHom ((monomial d) 1 ⊗ₜ[R] n)) = coeff e (↑rTensor ((monomial d) 1 ⊗ₜ[R] n))
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>d : σ →₀ ℕ<VAR>n : N<VAR>e : σ →₀ ℕ<GOAL>coeff e ((monomial d) 1) ⊗ₜ[R] n = coeff e (↑rTensor ((monomial d) 1 ⊗ₜ[R] n))
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>d : σ →₀ ℕ<VAR>n : N<VAR>e : σ →₀ ℕ<GOAL>((monomial d) 1) e ⊗ₜ[R] n = (↑rTensor ((monomial d) 1 ⊗ₜ[R] n)) e
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>s : R<GOAL>(xgcd 0 s).2 = 1
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>j : ℕ<GOAL>↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₗ[R] B<VAR>a : A<VAR>r : R<GOAL>f (a * (algebraMap R A) r) = f a * (algebraMap R B) r
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<GOAL>rank 0 = 0
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ s₁ s₂ t₁ t₂ u : Set E<VAR>x y : E<VAR>s : Set E<VAR>t : ι → Set E<GOAL>convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i)
<VAR>x : EReal<VAR>n : ℕ<GOAL>(↑n * x).exp = x.exp ^ n
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>abs (cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial) ≤ abs x ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(cauSeqAbs (exp' x + -const (⇑abs) (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤ abs x ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>↑(cauSeqAbs (exp' x + -const (⇑abs) (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤ ↑(const _root_.abs (abs x ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>↑(cauSeqAbs (exp' x - const (⇑abs) (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤ ↑(const _root_.abs (abs x ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>abs (∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial) ≤ abs x ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
<VAR>x : ℂ<VAR>hx : abs x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>abs (∑ k ∈ filter (fun k => n ≤ k) (range j), x ^ k / ↑k.factorial) ≤ abs x ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>n : ℕ<GOAL>χ ^ (2 * n + 1) = χ
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>(of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>i : σ<VAR>m : σ →₀ ℕ<GOAL>coeff m (X i) = if Finsupp.single i 1 = m then 1 else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<GOAL>Integrable (fun x => 0) μ
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>G'.deleteEdges s ≤ G'