ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[cocompact ℝ] fun x => |x| ^ (-b)<VAR>K : Compacts ℝ<VAR>r : ℝ<VAR>hr : ↑K ⊆ Icc (-r) r<VAR>this : ∀ (x : ℝ), ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖<GOAL>(fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x => |x| ^ (-b)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>K : Compacts ℝ<VAR>r : ℝ<VAR>hr : ↑K ⊆ Icc (-r) r<VAR>this : ∀ (x : ℝ), ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖<VAR>hf : (⇑f =O[atBot] fun x => |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x => |x| ^ (-b)<GOAL>((fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atBot] fun x => |x| ^ (-b)) ∧ (fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atTop] fun x => |x| ^ (-b)
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : Unique J<VAR>f : J → C<VAR>j : J<GOAL>default = j
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : Unique J<VAR>f : J → C<VAR>j : J<GOAL>j = default
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace ℝ E<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace ℝ F<VAR>inst✝¹¹ : NormedAddCommGroup F'<VAR>inst✝¹⁰ : NormedSpace ℝ F'<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : ↥(Lp G' 1 μ)<VAR>hfg : f ≤ g<GOAL>(setToL1 hT) f ≤ (setToL1 hT) g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace ℝ E<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace ℝ F<VAR>inst✝¹¹ : NormedAddCommGroup F'<VAR>inst✝¹⁰ : NormedSpace ℝ F'<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : ↥(Lp G' 1 μ)<VAR>hfg : 0 ≤ g - f<GOAL>0 ≤ (setToL1 hT) g - (setToL1 hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace ℝ E<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace ℝ F<VAR>inst✝¹¹ : NormedAddCommGroup F'<VAR>inst✝¹⁰ : NormedSpace ℝ F'<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : ↥(Lp G' 1 μ)<VAR>hfg : 0 ≤ g - f<GOAL>0 ≤ (setToL1 hT) (g - f)
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>n : ℤ<VAR>s : Set G<VAR>hs : (fun x => x ^ n) ⁻¹' s = s<VAR>g : G<VAR>j : ℕ<VAR>hg : g ^ n ^ j = 1<GOAL>g • s = s
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>n : ℤ<VAR>s : Set G<VAR>hs : (fun x => x ^ n) ⁻¹' s = s<VAR>g : G<VAR>j : ℕ<VAR>hg : g ^ n ^ j = 1<GOAL>∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>n : ℤ<VAR>s : Set G<VAR>hs : (fun x => x ^ n) ⁻¹' s = s<VAR>g : G<VAR>j : ℕ<VAR>hg : g ^ n ^ j = 1<GOAL>∀ {g' : G}, g' ^ n ^ j = 1 → g' • (fun x => x ^ n)^[j] ⁻¹' s ⊆ (fun x => x ^ n)^[j] ⁻¹' s
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>n : ℤ<VAR>s : Set G<VAR>hs : (fun x => x ^ n) ⁻¹' s = s<VAR>g : G<VAR>j : ℕ<VAR>hg : g ^ n ^ j = 1<VAR>g' y : G<VAR>hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s<VAR>hg' : (⇑(zpowGroupHom n))^[j] g' = 1<GOAL>(⇑(zpowGroupHom n))^[j] (g' * y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>a : M<GOAL>a * a ^ (n - 1) = a ^ n
<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>hx' : x' ∈ (chartAt H x).source<GOAL>ContMDiffAt I I' n f x' ↔ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ.prod ν) s = 0 ↔ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>x✝ : ∃ s, s.card = n ∧ LinearIndependent R Subtype.val<VAR>s : Finset M<VAR>h₁ : s.card = n<VAR>h₂ : LinearIndependent R Subtype.val<GOAL>↑n ≤ Module.rank R M
<VAR>α β : BddOrd<VAR>e : ↑α.toPartOrd ≃o ↑β.toPartOrd<VAR>x✝ : (forget BddOrd).obj α<GOAL>(↑e ≫ ↑e.symm) x✝ = (𝟙 α) x✝
<VAR>α β : BddOrd<VAR>e : ↑α.toPartOrd ≃o ↑β.toPartOrd<VAR>x✝ : (forget BddOrd).obj β<GOAL>(↑e.symm ≫ ↑e) x✝ = (𝟙 β) x✝
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>i j : Ordinal.{u}<VAR>hij : i ≤ j<GOAL>⋃ j, ball (p.c (p.index ↑j)) (p.r (p.index ↑j)) ≤ ⋃ j_1, ball (p.c (p.index ↑j_1)) (p.r (p.index ↑j_1))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SSameSide p₃ p₄<VAR>h : ¬p₁ = p₂<VAR>sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SSameSide p₃ p₄<VAR>h : ¬p₁ = p₂<VAR>sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}<VAR>hc : IsConnected sp<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SSameSide p₃ p₄<VAR>h : ¬p₁ = p₂<VAR>sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}<VAR>hc : IsConnected sp<VAR>hf : ContinuousOn (fun p => ∡ p.1 p.2.1 p.2.2) sp<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SSameSide p₃ p₄<VAR>h : ¬p₁ = p₂<VAR>sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}<VAR>hc : IsConnected sp<VAR>hf : ContinuousOn (fun p => ∡ p.1 p.2.1 p.2.2) sp<VAR>hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ ↑π<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SSameSide p₃ p₄<VAR>h : ¬p₁ = p₂<VAR>sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}<VAR>hc : IsConnected sp<VAR>hf : ContinuousOn (fun p => ∡ p.1 p.2.1 p.2.2) sp<VAR>hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ ↑π<VAR>hp₃ : (p₁, p₃, p₂) ∈ sp<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SSameSide p₃ p₄<VAR>h : ¬p₁ = p₂<VAR>sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}<VAR>hc : IsConnected sp<VAR>hf : ContinuousOn (fun p => ∡ p.1 p.2.1 p.2.2) sp<VAR>hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ ↑π<VAR>hp₃ : (p₁, p₃, p₂) ∈ sp<VAR>hp₄ : (p₁, p₄, p₂) ∈ sp<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>g : R →+* P<VAR>T : Submonoid P<VAR>hy : M ≤ Submonoid.comap g T<VAR>Q : Type u_4<VAR>inst✝³ : CommRing Q<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization T Q<VAR>inst✝ : IsLocalization M S<VAR>x : S<VAR>a : Set R<GOAL>x ∈ Ideal.span (⇑(algebraMap R S) '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>g : R →+* P<VAR>T : Submonoid P<VAR>hy : M ≤ Submonoid.comap g T<VAR>Q : Type u_4<VAR>inst✝³ : CommRing Q<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization T Q<VAR>inst✝ : IsLocalization M S<VAR>x : S<VAR>a : Set R<GOAL>(∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>inst✝ : CommMonoid α<VAR>S : Multiset (Multiset α)<GOAL>S.join.prod = (map prod S).prod
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>hc : c ≠ 0<GOAL>a / c ≤ b ↔ a ≤ b * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f g : α → Option β<VAR>x : Option α<VAR>h : ∀ (a : α), a ∈ x → f a = g a<GOAL>x.bind f = x.bind g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>e : X ≃ᵈ Y<VAR>e' : Y ≃ᵈ Z<VAR>hX : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤<GOAL>ratio (e.trans e') = ratio e * ratio e'
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<GOAL>𝓕 (iteratedDeriv n f) x = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<VAR>A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume<GOAL>𝓕 (iteratedDeriv n f) x = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<VAR>A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume<GOAL>𝓕 (fun x => iteratedDeriv n f x) x = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<VAR>A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume<GOAL>((fourierPowSMulRight (-innerSL ℝ) (𝓕 f) x n) fun x => 1) = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ C<VAR>c : (k : K) → LimitCone (F.flip.obj k)<VAR>j₁ j₂ : J<VAR>g : j₁ ⟶ j₂<VAR>k : K<GOAL>(((const J).obj { obj := fun k => (c k).cone.pt, map := fun {k₁ k₂} f => (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f }, map_id := ⋯, map_comp := ⋯ }).map g ≫ (fun j => { app := fun k => (c k).cone.π.app j, naturality := ⋯ }) j₂).app k = ((fun j => { app := fun k => (c k).cone.π.app j, naturality := ⋯ }) j₁ ≫ F.map g).app k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Option α ≃ Option β<VAR>x : α<VAR>h : ∃ x', e (some x) = some x'<GOAL>some (e.removeNone_aux x) = e (some x)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<GOAL>M.Coindep X ↔ ∃ B, M.Base B ∧ X ⊆ M.E \ B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<GOAL>(∃ B, M.Base B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ B, M.Base B ∧ X ⊆ M.E ∧ Disjoint X B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a✝ : α<VAR>b✝ : β<VAR>p : α → Prop<VAR>q : β → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>a : α<VAR>b : β<GOAL>(a, b) ∈ filter (fun x => p x.1 ∧ q x.2) (s ×ˢ t) ↔ (a, b) ∈ filter p s ×ˢ filter q t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>h : (↑s).Nonempty<VAR>v : V<GOAL>v ∈ s.direction ↔ ∃ p1 ∈ s, ∃ p2 ∈ s, v = p1 -ᵥ p2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>h : (↑s).Nonempty<VAR>v : V<GOAL>(∃ x ∈ ↑s, ∃ y ∈ ↑s, x -ᵥ y = v) ↔ ∃ p1 ∈ s, ∃ p2 ∈ s, v = p1 -ᵥ p2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : iUnion U = univ<GOAL>Surjective f ↔ ∀ (i : ι), Surjective ((U i).restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : iUnion U = univ<VAR>H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)<VAR>x : β<GOAL>∃ a, f a = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : iUnion U = univ<VAR>H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)<VAR>x : β<VAR>i : ι<VAR>hi : x ∈ U i<GOAL>∃ a, f a = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f✝ g : α → E<VAR>s t : Set α<VAR>μ✝ ν : Measure α<VAR>l l' : Filter α<VAR>inst✝ : MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<VAR>μ : Measure β<GOAL>IntegrableAtFilter f (map e l) μ ↔ IntegrableAtFilter (f ∘ e) l (Measure.comap e μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f✝ g : α → E<VAR>s t : Set α<VAR>μ✝ ν : Measure α<VAR>l l' : Filter α<VAR>inst✝ : MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<VAR>μ : Measure β<GOAL>(∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(starRingEnd ℂ) (↑x).cot = (↑x).cot
<VAR>v : PrimeMultiset<GOAL>↑v.prod = v.toNatMultiset.prod
<VAR>v : PrimeMultiset<VAR>h : ↑v.prod = (Multiset.map Coe.coe (Multiset.map Coe.coe v)).prod := MonoidHom.map_multiset_prod PNat.coeMonoidHom v.toPNatMultiset<GOAL>↑v.prod = v.toNatMultiset.prod
<VAR>v : PrimeMultiset<VAR>h : ↑v.prod = (Multiset.map (Coe.coe ∘ Coe.coe) v).prod<GOAL>↑v.prod = v.toNatMultiset.prod
<VAR>v : PrimeMultiset<VAR>h : ↑v.prod = (Multiset.map (Coe.coe ∘ Coe.coe) v).prod<VAR>this : Coe.coe ∘ Coe.coe = Coe.coe<GOAL>↑v.prod = v.toNatMultiset.prod
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a✝ b : Γ<VAR>r✝ : R<VAR>a : Γ<VAR>r : R<GOAL>((single a) r).leadingCoeff = r
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a✝ b : Γ<VAR>r✝ : R<VAR>a : Γ<VAR>r : R<GOAL>(if h : r = 0 then 0 else ((single a) r).coeff (⋯.min ⋯)) = r
<VAR>A : Type v<VAR>inst✝ : Ring A<VAR>h₁ : (Std.Commutative fun x x_1 => x * x_1) ↔ ∀ (a b : A), a * b = b * a<GOAL>(Std.Commutative fun x x_1 => x * x_1) ↔ IsLieAbelian A
<VAR>A : Type v<VAR>inst✝ : Ring A<VAR>h₁ : (Std.Commutative fun x x_1 => x * x_1) ↔ ∀ (a b : A), a * b = b * a<VAR>h₂ : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0<GOAL>(Std.Commutative fun x x_1 => x * x_1) ↔ IsLieAbelian A
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>s t : Finset α<GOAL>Eₘ[s, t] = Eₘ[t, s]
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>s t : Finset α<GOAL>(filter ((fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ∘ ⇑(Equiv.prodComm (α × α) (α × α)).symm) (map (Equiv.prodComm (α × α) (α × α)).toEmbedding ((s ×ˢ s) ×ˢ t ×ˢ t))).card = Eₘ[t, s]
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>inst✝ : HasKernel f'<VAR>p : X ≅ X'<VAR>q : Y ≅ Y'<VAR>w : f ≫ q.hom = p.hom ≫ f'<GOAL>f' ≫ q.inv = p.inv ≫ f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>inst✝ : HasKernel f'<VAR>p : X ≅ X'<VAR>q : Y ≅ Y'<VAR>w : f ≫ q.hom = p.hom ≫ f'<GOAL>(f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<GOAL>Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = 0
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<GOAL>Polynomial.eval x (Polynomial.map (subfield G F).subtype (minpoly G F x)) = Polynomial.eval x (prodXSubSMul G F x)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>inst✝ : Semiring T<GOAL>eval₂ f x (X * p) = eval₂ f x p * x
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<GOAL>{ toQuot := Quot.mk (Rel r) 1 } = RingQuot.one r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : ↥(Lp.simpleFunc E 1 μ)<GOAL>Integrable (↑(Lp.simpleFunc.toSimpleFunc f)) μ