ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithTop α<GOAL>a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithTop α<GOAL>(if a = 0 ∨ b = 0 then 0 else map₂ (fun x x_1 => x * x_1) a b) = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : HeytingAlgebra α<VAR>a b : α<GOAL>IsRegular ⊥
<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>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hμst : μ (s ∆ t) ≠ ⊤<GOAL>μ s = ⊤ ↔ μ t = ⊤
<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>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hμst : μ (s ∆ t) ≠ ⊤<GOAL>∀ (u v : Set α), μ (u ∆ v) ≠ ⊤ → μ u = ⊤ → μ v = ⊤
<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>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hμst : μ (s ∆ t) ≠ ⊤<VAR>u v : Set α<VAR>hμuv : μ (u ∆ v) ≠ ⊤<VAR>hμu : μ u = ⊤<GOAL>μ v = ⊤
<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>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hμst : μ (s ∆ t) ≠ ⊤<VAR>u v : Set α<VAR>hμuv : μ (u ∆ v) ≠ ⊤<VAR>hμu : μ u = ⊤<VAR>hμv : μ v ≠ ⊤<GOAL>False
<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>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hμst : μ (s ∆ t) ≠ ⊤<VAR>u v : Set α<VAR>hμuv : μ (u ∆ v) ≠ ⊤<VAR>hμu : μ u = ⊤<VAR>hμv : μ v ≠ ⊤<GOAL>μ (u ∆ v) = ⊤
<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>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hμst : μ (s ∆ t) ≠ ⊤<VAR>u v : Set α<VAR>hμuv : μ (u ∆ v) ≠ ⊤<VAR>hμu : μ u = ⊤<VAR>hμv : μ v ≠ ⊤<GOAL>⊤ ≤ μ (u \ v ∪ v \ u)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>((fun x => rexp (f x)) =Θ[l] fun x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x|
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅<VAR>ι✝ : Type u<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<GOAL>∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅<VAR>ι✝ : Type u<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥<GOAL>∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅<VAR>ι✝ : Type u<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥<VAR>t : Set ι✝<VAR>ht : t.Countable ∧ s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅<GOAL>t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<GOAL>(Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<GOAL>(Polynomial.idealX K).intValuationDef P = (idealX K).intValuationDef ↑P
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<GOAL>↑(Multiplicative.ofAdd (-↑((Associates.mk (Polynomial.idealX K).asIdeal).count (Associates.mk (Ideal.span {P})).factors))) = ↑(Multiplicative.ofAdd (-↑((Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors)))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<GOAL>(Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors = (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<VAR>span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0<GOAL>(Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors = (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<VAR>span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0<VAR>span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0<GOAL>(Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors = (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<VAR>span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0<VAR>span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0<GOAL>Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) = Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P}))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<VAR>span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0<VAR>span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0<GOAL>Ideal.span {↑P} ≠ 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<VAR>span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0<VAR>span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0<GOAL>(idealX K).asIdeal.IsPrime
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<VAR>span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0<VAR>span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0<GOAL>(idealX K).asIdeal ≠ ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<VAR>span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0<VAR>span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0<GOAL>Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) = Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : K[X]<VAR>hP : ¬P = 0<VAR>span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0<VAR>span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0<GOAL>Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P})) = Multiset.count X (UniqueFactorizationMonoid.normalizedFactors ↑P)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>s : NonUnitalSubsemiring S<VAR>x : R × S<GOAL>x ∈ ⊤.prod s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (a : α), f a ≤ 1<VAR>h'f : ∀ a ∈ sᶜ, f a = 0<GOAL>∫⁻ (a : α), f a ∂μ ≤ μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (a : α), f a ≤ 1<VAR>h'f : ∀ a ∈ sᶜ, f a = 0<VAR>x : α<GOAL>f x ≤ s.indicator 1 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ filter (fun a => p a ∨ q a) s ↔ x✝ ∈ filter p s ∪ filter q s
<VAR>α : Type u_1<VAR>a : ℝ≥0<VAR>f : α → ℝ≥0<GOAL>↑(∑' (x : α), a * f x) = ↑(a * ∑' (x : α), f x)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJY : M.Basis J Y<VAR>h : M.Indep (I ∪ J)<GOAL>M.Basis (I ∪ J) (X ∪ Y)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJY : M.Basis J Y<VAR>h : M.Indep (I ∪ J)<GOAL>M.Basis (⋃ b, bif b then I else J) (⋃ b, bif b then X else Y)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJY : M.Basis J Y<VAR>h : M.Indep (I ∪ J)<GOAL>∀ (i : Bool), M.Basis (bif i then I else J) (bif i then X else Y)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJY : M.Basis J Y<VAR>h : M.Indep (I ∪ J)<GOAL>M.Indep (⋃ i, bif i then I else J)
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Rack R✝<VAR>R : Type u_2<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>act' (x ◃ y) = act' x * act' y * (act' x)⁻¹
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Rack R✝<VAR>R : Type u_2<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>act' (x ◃ y) * act' x = act' x * act' y
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Rack R✝<VAR>R : Type u_2<VAR>inst✝ : Rack R<VAR>x y z : R<GOAL>(act' (x ◃ y) * act' x) z = (act' x * act' y) z
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X✝ Y✝ : CommMon_ C<VAR>f : X✝ ⟶ Y✝<VAR>x✝² x✝¹ : Discrete PUnit.{u + 1}<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>𝟙 X✝.X ≫ f.hom = f.hom ≫ 𝟙 Y✝.X
<VAR>V : Type v<VAR>inst✝⁴ : Category.{w, v} V<VAR>inst✝³ : MonoidalCategory V<VAR>C : Type u₁<VAR>inst✝² : EnrichedCategory V C<VAR>D : Type u₂<VAR>inst✝¹ : EnrichedCategory V D<VAR>inst✝ : BraidedCategory V<VAR>F G : EnrichedFunctor V C D<VAR>X✝ Y✝ : Vᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>σ : (fun A => GradedNatTrans ((Center.ofBraided V).obj (unop A)) F G) X✝<VAR>X Y : C<GOAL>(((Center.ofBraided V).obj (unop Y✝)).snd.β (EnrichedCategory.Hom X Y)).hom ≫ (F.map X Y ⊗ (fun X => f.unop ≫ σ.app X) Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) = ((fun X => f.unop ≫ σ.app X) X ⊗ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
<VAR>V : Type v<VAR>inst✝⁴ : Category.{w, v} V<VAR>inst✝³ : MonoidalCategory V<VAR>C : Type u₁<VAR>inst✝² : EnrichedCategory V C<VAR>D : Type u₂<VAR>inst✝¹ : EnrichedCategory V D<VAR>inst✝ : BraidedCategory V<VAR>F G : EnrichedFunctor V C D<VAR>X✝ Y✝ : Vᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>σ : (fun A => GradedNatTrans ((Center.ofBraided V).obj (unop A)) F G) X✝<VAR>X Y : C<VAR>p : (((Center.ofBraided V).obj (unop X✝)).snd.β (EnrichedCategory.Hom X Y)).hom ≫ (F.map X Y ⊗ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) = (σ.app X ⊗ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)<GOAL>(((Center.ofBraided V).obj (unop Y✝)).snd.β (EnrichedCategory.Hom X Y)).hom ≫ (F.map X Y ⊗ (fun X => f.unop ≫ σ.app X) Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) = ((fun X => f.unop ≫ σ.app X) X ⊗ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
<VAR>V : Type v<VAR>inst✝⁴ : Category.{w, v} V<VAR>inst✝³ : MonoidalCategory V<VAR>C : Type u₁<VAR>inst✝² : EnrichedCategory V C<VAR>D : Type u₂<VAR>inst✝¹ : EnrichedCategory V D<VAR>inst✝ : BraidedCategory V<VAR>F G : EnrichedFunctor V C D<VAR>X✝ Y✝ : Vᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>σ : (fun A => GradedNatTrans ((Center.ofBraided V).obj (unop A)) F G) X✝<VAR>X Y : C<VAR>p : (β_ (unop X✝) (EnrichedCategory.Hom X Y)).hom ≫ (F.map X Y ⊗ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) = (σ.app X ⊗ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)<GOAL>(β_ (unop Y✝) (EnrichedCategory.Hom X Y)).hom ≫ (F.map X Y ⊗ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) = (f.unop ≫ σ.app X ⊗ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
<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>h : HasFTaylorSeriesUpTo n f p<VAR>hn : 1 ≤ n<VAR>x : E<GOAL>HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x
<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>h : HasFTaylorSeriesUpTo n f p<VAR>hn : 1 ≤ n<VAR>x : E<GOAL>HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) univ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ℚ), preCDF ρ r a ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : ρ.fst s < ⊤<GOAL>∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : ρ.fst s < ⊤<GOAL>(ρ.IicSnd ↑r) s ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : ρ.fst s < ⊤<GOAL>(ρ.IicSnd ↑r) s ≤ ρ.fst s
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p)<VAR>inst✝² : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝ : Fintype ι<VAR>x y : WithLp p ((i : ι) → β i)<GOAL>edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y) ≤ ↑1 * edist x y
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p)<VAR>inst✝² : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝ : Fintype ι<VAR>x y : WithLp p ((i : ι) → β i)<GOAL>∀ (b : ι), edist (x b) (y b) ≤ edist x y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝² : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Fact (1 ≤ ⊤)<VAR>x y : WithLp ⊤ ((i : ι) → β i)<GOAL>∀ (b : ι), edist (x b) (y b) ≤ edist x y
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p)<VAR>inst✝² : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝ : Fintype ι<VAR>x y : WithLp p ((i : ι) → β i)<VAR>h : 1 ≤ p.toReal<GOAL>∀ (b : ι), edist (x b) (y b) ≤ edist x y
<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✝³ : PseudoEMetricSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>n : ℕ<VAR>x : β<VAR>this : Nonempty ↑s<GOAL>Nat.casesOn 0 y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
<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✝³ : PseudoEMetricSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>n✝ : ℕ<VAR>x : β<VAR>this : Nonempty ↑s<VAR>n : ℕ<GOAL>Nat.casesOn (n + 1) y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>↑⌊a + b⌋ - 1 - a ≤ ↑⌊b⌋
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>↑⌊a + b⌋ - 1 - a ≤ b - 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>↑⌊a + b⌋ ≤ a + b
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<VAR>hs : Dense s<VAR>ht : Dense t<VAR>x : X × Y<GOAL>x ∈ closure (s ×ˢ t)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<VAR>hs : Dense s<VAR>ht : Dense t<VAR>x : X × Y<GOAL>x ∈ closure s ×ˢ closure t
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>f✝ : Π₀ (i : ι), β✝ i<VAR>b✝ : β✝ i✝<VAR>j✝ : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>j : ι<GOAL>(update i f b) j = (erase i f + single i b) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>f✝ : Π₀ (i : ι), β✝ i<VAR>b✝ : β✝ i✝<VAR>j : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<GOAL>(update i f b) i = (erase i f + single i b) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>f✝ : Π₀ (i : ι), β✝ i<VAR>b✝ : β✝ i✝<VAR>j✝ : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>j : ι<VAR>h : i ≠ j<GOAL>(update i f b) j = (erase i f + single i b) j
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>κ : Type u_10<VAR>q : SeminormFamily 𝕜₂ F ι'<VAR>inst✝² : UniformSpace E<VAR>inst✝¹ : UniformAddGroup E<VAR>u : UniformSpace F<VAR>hu : UniformAddGroup F<VAR>hq : WithSeminorms q<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>f : κ → E →ₛₗ[σ₁₂] F<GOAL>[EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), ∀ (i : ι'), ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p, ∀ (i : ι'), BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))].TFAE
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>κ : Type u_10<VAR>q : SeminormFamily 𝕜₂ F ι'<VAR>inst✝² : UniformSpace E<VAR>inst✝¹ : UniformAddGroup E<VAR>u : UniformSpace F<VAR>hu : UniformAddGroup F<VAR>hq : WithSeminorms q<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>f : κ → E →ₛₗ[σ₁₂] F<GOAL>[∀ (k : ι'), EquicontinuousAt (DFunLike.coe ∘ f) 0, ∀ (k : ι'), Equicontinuous (DFunLike.coe ∘ f), ∀ (k : ι'), UniformEquicontinuous (DFunLike.coe ∘ f), ∀ (i : ι'), ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p, ∀ (i : ι'), BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))].TFAE
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>κ : Type u_10<VAR>q : SeminormFamily 𝕜₂ F ι'<VAR>inst✝² : UniformSpace E<VAR>inst✝¹ : UniformAddGroup E<VAR>u : UniformSpace F<VAR>hu : UniformAddGroup F<VAR>hq : WithSeminorms q<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>f : κ → E →ₛₗ[σ₁₂] F<VAR>i : ι'<GOAL>(List.map (fun p => p i) [fun k => EquicontinuousAt (DFunLike.coe ∘ f) 0, fun k => Equicontinuous (DFunLike.coe ∘ f), fun k => UniformEquicontinuous (DFunLike.coe ∘ f), fun i => ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p, fun i => BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))]).TFAE
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>x y : Fin 1<GOAL>¬x = y → (∏ x_1 ∈ finPairsLT 1, if (if x_1.fst = x then y else if x_1.fst = y then x else x_1.fst) ≤ if x_1.snd = x then y else if x_1.snd = y then x else x_1.snd then -1 else 1) = -1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>x y : Fin (n + 2)<VAR>hxy : x ≠ y<GOAL>(swap x y).signAux = -1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>x y : Fin (n + 2)<VAR>hxy : x ≠ y<VAR>h2n : 2 ≤ n + 2<GOAL>(swap x y).signAux = -1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>x y : Fin (n + 2)<VAR>hxy : x ≠ y<VAR>h2n : 2 ≤ n + 2<GOAL>IsConj (swap x y).signAux (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux
<VAR>R : Type u_1<VAR>inst✝¹ : MonoidWithZero R<VAR>S : Submonoid R<VAR>inst✝ : OreSet S<VAR>s : ↥S<GOAL>0 /ₒ s = 0
<VAR>R : Type u_1<VAR>inst✝¹ : MonoidWithZero R<VAR>S : Submonoid R<VAR>inst✝ : OreSet S<VAR>s : ↥S<GOAL>∃ u v, u • 0 = v • 0 ∧ ↑u * ↑1 = v * ↑s
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e✝ : Sym2 V<VAR>s : Set (Sym2 V)<VAR>e : Sym2 V<GOAL>e ∈ (fromEdgeSet s).edgeSet ↔ e ∈ s \ {e | e.IsDiag}