ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : 1 < x<GOAL>P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>hx : 0 < 1<GOAL>P.f_modif (1 / 1) = (P.ε * ↑(1 ^ P.k)) • P.g_modif 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : x < 1<GOAL>P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)
<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✝⁴ : Fintype m<VAR>inst✝³ : Field R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>A : Matrix m n R<GOAL>(A * Aᴴ).rank = A.rank
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ✝ ν✝ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>μ ν : Measure α<GOAL>eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ✝ ν✝ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>μ ν : Measure α<GOAL>∫⁻ (x : α), ↑‖f x‖₊ ∂(μ + ν) = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ + ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
<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>s : Set (M × N)<VAR>p : M × N<GOAL>ContMDiffWithinAt (I.prod J) I n Prod.fst s p
<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>s : Set (M × N)<VAR>p : M × N<GOAL>ContinuousWithinAt Prod.fst s p ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I p.1) ∘ Prod.fst ∘ ↑(extChartAt (I.prod J) p).symm) ((extChartAt (I.prod J) p).target ∩ ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source)) (↑(extChartAt (I.prod J) p) p)
<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>s : Set (M × N)<VAR>p : M × N<VAR>y : E × F<VAR>hy : y ∈ (extChartAt (I.prod J) p).target ∩ ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source)<GOAL>(↑(extChartAt I p.1) ∘ Prod.fst ∘ ↑(extChartAt (I.prod J) p).symm) y = y.1
<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>s : Set (M × N)<VAR>p : M × N<GOAL>(↑(extChartAt I p.1) ∘ Prod.fst ∘ ↑(extChartAt (I.prod J) p).symm) (↑(extChartAt (I.prod J) p) p) = (↑(extChartAt (I.prod J) p) p).1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>MellinConvergent (fun t => f (t ^ a)) s ↔ MellinConvergent f (s / ↑a)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>MellinConvergent (fun t => f (t ^ a)) s ↔ IntegrableOn (fun x => x ^ (a - 1) • ↑(x ^ a) ^ (s / ↑a - 1) • f (x ^ a)) (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>IntegrableOn (fun t => ↑t ^ (s - 1) • f (t ^ a)) (Ioi 0) volume ↔ IntegrableOn (fun x => x ^ (a - 1) • ↑(x ^ a) ^ (s / ↑a - 1) • f (x ^ a)) (Ioi 0) volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : a ≠ 0<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑t ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)
<VAR>a : ℕ<VAR>h : a % 2 = 0<GOAL>a.minFac = ↑2
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>inst✝ : Nonempty ι<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>volume s = 0
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>inst✝ : Nonempty ι<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>s ⊆ frontier s
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>inst✝ : Nonempty ι<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>s ⊆ closure s
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<GOAL>(trinomial k m n u v w).coeff n = w
<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>f : M →ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<VAR>h : IsUnit ((toMatrix v v') f).det<VAR>x : M<GOAL>((toLin v' v) ((toMatrix v v') f)⁻¹) (f x) = ((toLin v v) (((toMatrix v v') f)⁻¹ * (toMatrix v v') f)) 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>f : M →ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<VAR>h : IsUnit ((toMatrix v v') f).det<VAR>x : M'<GOAL>f (((toLin v' v) ((toMatrix v v') f)⁻¹) x) = ((toLin v' v') ((toMatrix v v') f * ((toMatrix v v') f)⁻¹)) x
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>inst✝ : NumberField L<VAR>f : K ≃ₐ[ℚ] L<VAR>f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv<GOAL>discr K = discr L
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>inst✝ : NumberField L<VAR>f : K ≃ₐ[ℚ] L<VAR>f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv<GOAL>Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = ↑(Algebra.discr ℤ ⇑((RingOfIntegers.basis K).map f₀))
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>inst✝ : NumberField L<VAR>f : K ≃ₐ[ℚ] L<VAR>f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv<GOAL>Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = (algebraMap ℤ ℚ) (Algebra.discr ℤ ⇑((RingOfIntegers.basis K).map f₀))
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>inst✝ : NumberField L<VAR>f : K ≃ₐ[ℚ] L<VAR>f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv<GOAL>Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ ℤ⁰ L ((RingOfIntegers.basis K).map f₀))
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>inst✝ : NumberField L<VAR>f : K ≃ₐ[ℚ] L<VAR>f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv<VAR>x✝ : Module.Free.ChooseBasisIndex ℤ (𝓞 K)<GOAL>(⇑f ∘ ⇑(integralBasis K)) x✝ = (Basis.localizationLocalization ℚ ℤ⁰ L ((RingOfIntegers.basis K).map f₀)) x✝
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>inst✝ : NumberField L<VAR>f : K ≃ₐ[ℚ] L<VAR>f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv<VAR>x✝ : Module.Free.ChooseBasisIndex ℤ (𝓞 K)<GOAL>f ((algebraMap (𝓞 K) K) ((RingOfIntegers.basis K) x✝)) = (algebraMap (𝓞 L) L) (f₀ ((RingOfIntegers.basis K) x✝))
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : ¬f.IsClosable<GOAL>f ≤ f.closure
<VAR>α✝ : Type u<VAR>a : α✝<VAR>inst✝¹ : Group α✝<VAR>α : Type u<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Nat.card α ∣ p<GOAL>IsCyclic α
<VAR>α✝ : Type u<VAR>a : α✝<VAR>inst✝¹ : Group α✝<VAR>α : Type u<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Nat.card α ∣ p<VAR>this : Finite α<GOAL>IsCyclic α
<VAR>α✝ : Type u<VAR>a : α✝<VAR>inst✝¹ : Group α✝<VAR>α : Type u<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h✝ : Nat.card α ∣ p<VAR>this : Finite α<VAR>h : Nat.card α = 1<GOAL>IsCyclic α
<VAR>α✝ : Type u<VAR>a : α✝<VAR>inst✝¹ : Group α✝<VAR>α : Type u<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h✝ : Nat.card α ∣ p<VAR>this : Finite α<VAR>h : Nat.card α = p<GOAL>IsCyclic α
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f✝ f : ι →₀ μ<GOAL>f ∈ ∅.finsuppAntidiag 0 ↔ f ∈ {0}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ⇨ b = ⊤ ↔ a ≤ b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x y : R<VAR>p : R[X][Y]<GOAL>eval y (map (evalRingHom x) p) = evalEval x y p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<GOAL>(Forall₂ fun x x_1 => x = x_1) = Eq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>a b : List α<GOAL>Forall₂ (fun x x_1 => x = x_1) a b = (a = b)
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>x y : R✝<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p : Submodule R M<VAR>hf : MapsTo ⇑f ↑p ↑p<VAR>n : ℕ<VAR>hn : f ^ n = 0<GOAL>IsNilpotent (f.restrict hf)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>n : ℕ<GOAL>(a + b) ^ (n + 2) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>n : ℕ<GOAL>(a + b) ^ (n + 1) * (a + b) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>n : ℕ<GOAL>a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : CommSemiring A'<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R A'<VAR>inst✝² : Algebra R B<VAR>p✝ q : R[X]<VAR>x✝ : A<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : AlgHomClass F R A B<VAR>f : F<VAR>x : A<VAR>p : R[X]<GOAL>(aeval (f x)) p = f ((aeval x) p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : CommSemiring A'<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R A'<VAR>inst✝² : Algebra R B<VAR>p✝¹ q✝ : R[X]<VAR>x✝ : A<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : AlgHomClass F R A B<VAR>f : F<VAR>x : A<VAR>p✝ p q : R[X]<VAR>hp : (aeval (f x)) p = f ((aeval x) p)<VAR>hq : (aeval (f x)) q = f ((aeval x) q)<GOAL>(aeval (f x)) (p + q) = f ((aeval x) (p + q))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>g : γ → α<VAR>e : ↑(mulSupport f) ≃ ↑(mulSupport g)<VAR>he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x<GOAL>HasProd f a ↔ HasProd g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>g : γ → α<VAR>e : ↑(mulSupport f) ≃ ↑(mulSupport g)<VAR>he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x<VAR>this : (g ∘ Subtype.val) ∘ ⇑e = f ∘ Subtype.val<GOAL>HasProd f a ↔ HasProd g a
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S : IntermediateField K L<VAR>x : L<VAR>hx : x ∈ (algebraMap K L).fieldRange<GOAL>x ∈ Set.range ⇑(algebraMap K L)
<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>x y : V<VAR>r₁ r₂ : ℝ<GOAL>(o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign
<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>x y : V<VAR>r₁ r₂ : ℝ<GOAL>(o.oangle x (-r₁ • x + (r₁ • x + r₂ • y))).sign = SignType.sign r₂ * (o.oangle x y).sign
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>f : α → β<VAR>l : Filter β<VAR>p : α → Prop<VAR>s : Set α<GOAL>s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l
<VAR>R✝ : Type u<VAR>inst✝¹ : EuclideanDomain R✝<VAR>R : Type u_1<VAR>inst✝ : EuclideanDomain R<VAR>a b : R<GOAL>b * (a / b) + a % b - b * (a / b) = a - b * (a / b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝³ : Semiring 𝕜<VAR>inst✝² : Algebra ℝ≥0 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : ContinuousSMul ℝ≥0 𝕜<GOAL>Tendsto (⇑(algebraMap ℝ≥0 𝕜) ∘ fun n => (↑n)⁻¹) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝³ : Semiring 𝕜<VAR>inst✝² : Algebra ℝ≥0 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : ContinuousSMul ℝ≥0 𝕜<GOAL>0 = (algebraMap ℝ≥0 𝕜) 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f✝ f : α → β<VAR>s : Set α<VAR>this : TopologicalSpace α := induced f t<GOAL>IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁷ : CommRing R₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i✝ : ι<VAR>j : ι'<VAR>N : Type u_9<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι'<VAR>i : ι'<VAR>j✝ : ι<GOAL>(toMatrix b b') id i j✝ = b'.toMatrix (⇑b) i j✝
<VAR>α : Type u<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b c : α<GOAL>a < a⁻¹ ↔ a < 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<VAR>this : ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<GOAL>∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n