ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<GOAL>Measure.toFinite 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : Integrable f μ<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, ↑↑(condexpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : Integrable f μ<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) (Integrable.toL1 f hf)) x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hf : Integrable f μ<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, ↑↑(Integrable.toL1 f hf) x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ<VAR>hfint : Integrable f μ<VAR>hfint' : 0 ≤ ∫ (x : α), f x ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r<GOAL>eLpNorm f 1 μ ≤ 2 * μ univ * ENNReal.ofReal r
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ<VAR>hfint : Integrable f μ<VAR>hfint' : 0 ≤ ∫ (x : α), f x ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r<GOAL>∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r.toNNReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>r : ℝ<VAR>hfint : Integrable f μ<VAR>hfint' : 0 ≤ ∫ (x : α), f x ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r<GOAL>∀ᵐ (ω : α) ∂μ, f ω ≤ r ∨ f ω ≤ 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s✝ : Set α<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>ab : a ≤ b<GOAL>variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Icc a b → edist (f x) (f y) = 0
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>this : ∀ (f : ℕ → ℕ), Nat.Primrec f → Primrec' fun v => f v.head<VAR>hf : Primrec f<VAR>i : Vector ℕ n<GOAL>((fun m => encode (Option.map f (decode m))) (encode i)).pred = f i
<VAR>n : ℕ<VAR>f✝ : Vector ℕ n → ℕ<VAR>f : ℕ → ℕ<VAR>hf : Nat.Primrec f<GOAL>Primrec' fun v => f v.head
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>hxy : x ≠ y<VAR>hyz : y ≠ z<VAR>hxz : x ≠ z<GOAL>{x, y, z}.infsep = dist x y ⊓ dist x z ⊓ dist y z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<VAR>h : dist x z < ε + δ<GOAL>∃ y, dist x y < δ ∧ dist y z ≤ ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<VAR>h : dist x z < ε + δ<VAR>y : E<VAR>yz : dist z y ≤ ε<VAR>xy : dist y x < δ<GOAL>∃ y, dist x y < δ ∧ dist y z ≤ ε
<VAR>x y : ℝ<GOAL>↑(cos x - cos y) = ↑(-2 * sin ((x + y) / 2) * sin ((x - y) / 2))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s t : Set α<VAR>f₁ f₂ : Filter (Filter α)<VAR>x : Set α<GOAL>x ∈ f₁.join ⊔ f₂.join ↔ x ∈ (f₁ ⊔ f₂).join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : Preorder α<VAR>inst✝¹ : IsEmpty ι<VAR>inst✝ : InfSet α<VAR>f : ι → WithTop α<GOAL>⨅ i, f i = ⊤
<VAR>a b c d a' b' : Ordinal.{u}<VAR>ha : a' ≤ a<VAR>hb : b' ≤ b<GOAL>a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
<VAR>a b c d a' b' : Ordinal.{u}<VAR>ha✝ : a' ≤ a<VAR>hb : b' ≤ b<VAR>ha : a' < a<GOAL>a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
<VAR>b c d a' b' : Ordinal.{u}<VAR>hb : b' ≤ b<VAR>ha : a' ≤ a'<GOAL>a' ⨳ b ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a' ⨳ b'
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>g₁ g₂ : N →ₗ[S] Q<VAR>e : ∀ (x : M), g₁ (f x) = g₂ (f x)<VAR>x : N<GOAL>g₁ x = g₂ x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>g₁ g₂ : N →ₗ[S] Q<VAR>e : ∀ (x : M), g₁ (f x) = g₂ (f x)<VAR>x : N<GOAL>g₁ 0 = g₂ 0
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>g₁ g₂ : N →ₗ[S] Q<VAR>e : ∀ (x : M), g₁ (f x) = g₂ (f x)<VAR>x : N<GOAL>∀ (m : M), g₁ (f m) = g₂ (f m)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>g₁ g₂ : N →ₗ[S] Q<VAR>e : ∀ (x : M), g₁ (f x) = g₂ (f x)<VAR>x : N<GOAL>∀ (s : S) (n : N), g₁ n = g₂ n → g₁ (s • n) = g₂ (s • n)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>g₁ g₂ : N →ₗ[S] Q<VAR>e : ∀ (x : M), g₁ (f x) = g₂ (f x)<VAR>x : N<GOAL>∀ (n₁ n₂ : N), g₁ n₁ = g₂ n₁ → g₁ n₂ = g₂ n₂ → g₁ (n₁ + n₂) = g₂ (n₁ + n₂)
<VAR>α : Type u_1<VAR>I : Type ?u.57896<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>m n : ℕ<VAR>H : IsRelPrime x y<GOAL>IsRelPrime (x ^ m) y
<VAR>α : Type u_1<VAR>I : Type ?u.57896<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>m n : ℕ<VAR>H : IsRelPrime x y<GOAL>IsRelPrime (∏ _x ∈ Finset.range m, x) y
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist p₂ ((homothety p₁ c) p₂) = ‖1 - c‖ * dist p₁ p₂
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MulAction G β<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : SMulCommClass G α β<VAR>a : α<VAR>b : β<GOAL>stabilizer G (a⁻¹ • a • b) = stabilizer G b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>f : F<GOAL>f (s.noncommProd comm) = (map (⇑f) s).noncommProd ⋯
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>a✝ : List α<VAR>comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute<GOAL>f (noncommProd ⟦a✝⟧ comm) = (map ⇑f ⟦a✝⟧).noncommProd ⋯
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<GOAL>ζ⁻¹ ^ k = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℕ<VAR>hl : ζ⁻¹ ^ l = 1<GOAL>k ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℕ<VAR>hl : ζ⁻¹ ^ l = 1<GOAL>ζ ^ l = 1
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>b * a ≤ b * b⁻¹ ↔ b * a ≤ 1
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>h : S.RightHomologyData<GOAL>(S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).inv ≫ S.rightHomologyIso.inv ≫ S.rightHomologyι = h.ι ≫ h.opcyclesIso.inv
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>i : σ<GOAL>i ∈ p.degrees ↔ ∃ d, coeff d p ≠ 0 ∧ i ∈ d.support
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : Opens G<VAR>hU : μ.outerMeasure ↑U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure ↑K + ↑ε
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>K : Compacts G<VAR>h1K : ↑K ⊆ ↑U<VAR>h2K : μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>w : List (α × Bool)<GOAL>reduce (invRev w) = invRev (reduce w)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>w : List (α × Bool)<GOAL>Red (reduce (invRev w)) (invRev (reduce w))
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>w : List (α × Bool)<GOAL>Red (invRev (reduce (invRev w))) (reduce w)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>w : List (α × Bool)<GOAL>Red w (invRev (reduce (invRev w)))
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>w : List (α × Bool)<VAR>this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))<GOAL>Red w (invRev (reduce (invRev w)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<GOAL>s.antidiagonal = map (fun t => (s - t, t)) s.powerset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<GOAL>antidiagonal 0 = map (fun t => (0 - t, t)) (powerset 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>hs : s.antidiagonal = map (fun t => (s - t, t)) s.powerset<GOAL>(a ::ₘ s).antidiagonal = map (fun t => (a ::ₘ s - t, t)) (a ::ₘ s).powerset
<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>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Algebra S A'<VAR>inst✝ : Algebra S B<VAR>g : R →ₐ[S] A'<VAR>y x✝ : A'<GOAL>(aevalTower (Algebra.ofId S A') x✝) X = (aeval x✝) X
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>ι : Type u_7<VAR>m : ι → Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f (sum m)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(map f (sum m)) s = (sum fun i => map f (m i)) s
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>ι : Type u_7<VAR>m : ι → Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f (sum m)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>ι : Type u_7<VAR>m : ι → Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f (sum m)<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>M : ∀ (i : ι), AEMeasurable f (m i)<GOAL>∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n a b : ℕ<VAR>f g : R⟦X⟧<VAR>ha : n < a<VAR>hb : n < b<GOAL>(coeff R n) (↑(trunc a f) * ↑(trunc b g)) = (coeff R n) (f * g)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<GOAL>¬Q.Anisotropic ↔ ∃ x, x ≠ 0 ∧ Q x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f ×ˢ g = map (fun p => (p.2, p.1)) (g ×ˢ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<GOAL>Prod.swap <$> (g ×ˢ f) = map (fun p => (p.2, p.1)) (g ×ˢ f)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<VAR>h : x ∈ evenOdd Q 0<GOAL>involute x = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>A : ι → Type u_3<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GMonoid A<VAR>l : List α<VAR>fι : α → ι<VAR>fA : (a : α) → A (fι a)<GOAL>mk (l.dProdIndex fι) (l.dProd fι fA) = (List.map (fun a => mk (fι a) (fA a)) l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<VAR>p : β → Prop<GOAL>(∃ y ∈ f.range, p y) ↔ ∃ x, p (↑f x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>b₃ : B.Nondegenerate<GOAL>B.orthogonal W = ⊥ ↔ W = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>b₃ : B.Nondegenerate<VAR>h : W = ⊤<GOAL>B.orthogonal W = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>b₃ : B.Nondegenerate<VAR>h : W = ⊤<GOAL>B.orthogonal ⊤ ≤ ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>m n : ℤ<GOAL>a ^ (m + n) = a ^ m * a ^ n
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℕ<VAR>c d : 𝕜<VAR>hc : c ≠ 0<GOAL>Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>r : R<GOAL>spectrum R ((algebraMap R A) r) ⊆ {r}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>r : R<GOAL>(fun x => r) '' spectrum R 0 ⊆ {r}
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f₁ f₂ : X' ⟶ Y'<VAR>g : Y' ⟶ Z'<GOAL>add W eX eY f₁ f₂ ≫ g = add W eX eZ (f₁ ≫ g) (f₂ ≫ g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f₂ : X' ⟶ Y'<VAR>g : Y' ⟶ Z'<VAR>f₁ : L.obj X ⟶ L.obj Y<GOAL>add W eX eY ((homEquiv eX eY).symm f₁) f₂ ≫ g = add W eX eZ ((homEquiv eX eY).symm f₁ ≫ g) (f₂ ≫ g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>g : Y' ⟶ Z'<VAR>f₁ f₂ : L.obj X ⟶ L.obj Y<GOAL>add W eX eY ((homEquiv eX eY).symm f₁) ((homEquiv eX eY).symm f₂) ≫ g = add W eX eZ ((homEquiv eX eY).symm f₁ ≫ g) ((homEquiv eX eY).symm f₂ ≫ g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>g : L.obj Y ⟶ L.obj Z<GOAL>add W eX eY ((homEquiv eX eY).symm f₁) ((homEquiv eX eY).symm f₂) ≫ (homEquiv eY eZ).symm g = add W eX eZ ((homEquiv eX eY).symm f₁ ≫ (homEquiv eY eZ).symm g) ((homEquiv eX eY).symm f₂ ≫ (homEquiv eY eZ).symm g)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hG : IsPGroup p G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>ϕ : H →* G<VAR>hϕ : Function.Injective ⇑ϕ<GOAL>IsPGroup p H