ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>b : β<VAR>hb₁ : b ∈ {b | f b ≤ g b}<VAR>hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ<GOAL>b ∈ {b | f b = g b}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>b : β<VAR>hb₁ : b ∈ {b | f b ≤ g b}<VAR>hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ<GOAL>b ∈ closure {b | g b < f b}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>b : β<VAR>hb₁ : b ∈ {b | f b ≤ g b}<VAR>hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ<GOAL>{b | g b < f b} = {b | f b ≤ g b}ᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>b : β<VAR>hb₁ : b ∈ {b | f b ≤ g b}<VAR>hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ<GOAL>{b | ¬f b ≤ g b} = {b | f b ≤ g b}ᶜ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>CondIndepSet m' hm' s t μ ↔ μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b✝ c u : αˣ<VAR>a : α<VAR>b : αˣ<GOAL>a * ↑b * ↑b⁻¹ = a
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d✝ : 𝕜 → 𝕜'<VAR>c' d' d : 𝕜'<GOAL>deriv (fun x => c x / d) x = deriv c x / d
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>J.IsAdjointPair J A₁ A₁ ↔ J.IsSelfAdjoint A₁
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c✝ : E<VAR>f✝ : ContDiffBump c✝<VAR>x✝ : E<VAR>n : ℕ∞<VAR>c g : X → E<VAR>s : Set X<VAR>f : (x : X) → ContDiffBump (c x)<VAR>x : X<VAR>hc : ContDiffWithinAt ℝ n c s x<VAR>hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x<VAR>hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x<VAR>hg : ContDiffWithinAt ℝ n g s x<GOAL>ContDiffWithinAt ℝ n (uncurry (someContDiffBumpBase E).toFun ∘ fun x => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c✝ : E<VAR>f✝ : ContDiffBump c✝<VAR>x✝ : E<VAR>n : ℕ∞<VAR>c g : X → E<VAR>s : Set X<VAR>f : (x : X) → ContDiffBump (c x)<VAR>x : X<VAR>hc : ContDiffWithinAt ℝ n c s x<VAR>hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x<VAR>hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x<VAR>hg : ContDiffWithinAt ℝ n g s x<GOAL>Ioi 1 ×ˢ univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c✝ : E<VAR>f✝ : ContDiffBump c✝<VAR>x✝ : E<VAR>n : ℕ∞<VAR>c g : X → E<VAR>s : Set X<VAR>f : (x : X) → ContDiffBump (c x)<VAR>x : X<VAR>hc : ContDiffWithinAt ℝ n c s x<VAR>hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x<VAR>hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x<VAR>hg : ContDiffWithinAt ℝ n g s x<GOAL>ContDiffWithinAt ℝ n (fun x => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>n : ℕ<GOAL>lift.{v, u} a < ↑n ↔ a < ↑n
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>m k : R<GOAL>m / k * k + m % k = m
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>m k : R<GOAL>k * (m / k) + m % k = m
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B'✝ X✝ Y✝ Y' : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i'✝ : B✝ ⟶ B'✝<VAR>p✝ : X✝ ⟶ Y✝<VAR>p' : Y✝ ⟶ Y'<VAR>A B A' B' X Y : C<VAR>i : A ⟶ B<VAR>i' : A' ⟶ B'<VAR>e : Arrow.mk i ≅ Arrow.mk i'<VAR>p : X ⟶ Y<VAR>hip : HasLiftingProperty i p<GOAL>HasLiftingProperty i' p
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B'✝ X✝ Y✝ Y' : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i'✝ : B✝ ⟶ B'✝<VAR>p✝ : X✝ ⟶ Y✝<VAR>p' : Y✝ ⟶ Y'<VAR>A B A' B' X Y : C<VAR>i : A ⟶ B<VAR>i' : A' ⟶ B'<VAR>e : Arrow.mk i ≅ Arrow.mk i'<VAR>p : X ⟶ Y<VAR>hip : HasLiftingProperty i p<GOAL>HasLiftingProperty (e.inv.left ≫ i ≫ e.hom.right) p
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<GOAL>CotangentSpace.map (g.comp f) = ↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<GOAL>∀ (i : P.vars), (CotangentSpace.map (g.comp f)) (P.cotangentSpaceBasis i) = (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (P.cotangentSpaceBasis i)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<VAR>i : P.vars<GOAL>(CotangentSpace.map (g.comp f)) (P.cotangentSpaceBasis i) = (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (P.cotangentSpaceBasis i)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<VAR>i : P.vars<GOAL>1 ⊗ₜ[P''.Ring] (D R'' P''.Ring) ((aeval g.val) (f.val i)) = 1 ⊗ₜ[P''.Ring] (D R'' P''.Ring) (g.toAlgHom (f.val i))
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<GOAL>Mᵀ.PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>x : n → R<GOAL>0 ≤ star x ⬝ᵥ Mᵀ *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>x : n → R<GOAL>star x ⬝ᵥ Mᵀ *ᵥ x = star (star x) ⬝ᵥ M *ᵥ star x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>map p.subtype (span R {x}) = span R {↑x}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>g : G<VAR>K : Compacts G<GOAL>prehaar (↑K₀) U (Compacts.map (fun b => g * b) ⋯ K) = prehaar (↑K₀) U K
<VAR>X : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UCompactlyGeneratedSpace X<VAR>Y : Type u_1<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)<GOAL>Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g : α → M<VAR>a x : α<GOAL>x ∈ mulSupport (s.mulIndicator f) ↔ x ∈ s ∩ mulSupport f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : LocalRing R<VAR>a b : R<VAR>u : Rˣ<VAR>hu : ↑u = a + b<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : LocalRing R<VAR>a b : R<VAR>u : Rˣ<VAR>hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1<GOAL>IsUnit a ∨ IsUnit b
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : FinEnum α<GOAL>(List.map (⇑equiv.symm) (List.finRange (card α))).Nodup
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝³ : (i : ι) → Module R (M₁ i)<VAR>inst✝² : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>x : M₁ i<GOAL>f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁶ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝³ : (i : ι) → Module R (M₁ i)<VAR>inst✝² : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>x : M₁ i<VAR>this : f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) = (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x)<GOAL>f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r✝ p q : α → α → Prop<VAR>s : Set α<VAR>r : α → α → Prop<GOAL>(Pairwise fun x y => r ↑x ↑y) ↔ s.Pairwise r
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ<GOAL>(expand 1) (X f) = (AlgHom.id R (MvPolynomial σ R)) (X f)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set (IntermediateField F E)<GOAL>↑(sInf S).toSubfield = ↑(sInf (toSubfield '' S))
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<GOAL>(μ.trim hm) s = μ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<GOAL>normalize (s.gcd f) = s.gcd f
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidablePred fun x => x < c<VAR>hbc : b ≤ c<GOAL>filter (fun x => x < c) (Ico a b) = Ico a b
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>coeff m (X s * p) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>(if Finsupp.single s 1 ≤ m then 1 * coeff (m - Finsupp.single s 1) p else 0) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<GOAL>(fun x => x ^ n) =o[atTop] rexp
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedCommMonoid α<VAR>a : α<GOAL>a * a ≤ 1 ↔ a ≤ 1
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>inst✝ : Inhabited F.M<VAR>x y : F.M<VAR>H : ∀ (ps : Path F), iselect ps x = iselect ps y<GOAL>x = y
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>inst✝ : Inhabited F.M<VAR>x y : F.M<VAR>H : ∀ (ps : Path F), iselect ps x = iselect ps y<GOAL>∀ (i : ℕ), x.approx i = y.approx i
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(bind₁ onePoly) (wittPolynomial p ℤ n) = 1
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 1
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<GOAL>Part.fix ⇑f = ωSup (approxChain f)
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<GOAL>Part.fix ⇑f ≤ ωSup (approxChain f)
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<GOAL>ωSup (approxChain f) ≤ Part.fix ⇑f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>g f' : R[X]<VAR>hf : (g * f').Separable<GOAL>g.Separable
<VAR>r : ℝ<VAR>hr : r < 0<GOAL>r.sign = -1
<GOAL>IsPrincipalIdealRing (𝓞 ℚ)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n : ℕ<VAR>inst✝ : CharP R n<VAR>I : Ideal R<GOAL>CharP (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n : ℕ<VAR>inst✝ : CharP R n<VAR>I : Ideal R<VAR>x✝ : CharP (R ⧸ I) n<VAR>x : ℕ<VAR>hx : ↑x ∈ I<GOAL>↑x = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n : ℕ<VAR>inst✝ : CharP R n<VAR>I : Ideal R<VAR>x✝ : CharP (R ⧸ I) n<VAR>x : ℕ<VAR>hx : ↑x ∈ I<GOAL>n ∣ x
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Div G✝<VAR>inst✝³ : ContinuousDiv G✝<VAR>G : Type u_1<VAR>inst✝² : CommGroupWithZero G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousDiv G<VAR>b : G<VAR>hb : b ≠ 0<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<GOAL>Tendsto (fun x => f x / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Div G✝<VAR>inst✝³ : ContinuousDiv G✝<VAR>G : Type u_1<VAR>inst✝² : CommGroupWithZero G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousDiv G<VAR>b : G<VAR>hb : b ≠ 0<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<VAR>h : Tendsto (fun x => f x / b) l (𝓝 (c / b))<GOAL>Tendsto f l (𝓝 c)
<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>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>h : y + ↑n ≠ 0<GOAL>x ^ (y + ↑n) = x ^ y * x ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hp : ∀ᶠ (x : α) in f, p x<VAR>hq : ∃ᶠ (x : α) in f, q x<GOAL>∃ᶠ (x : α) in f, p x ∧ q x
<VAR>n : ℕ<VAR>α : Type u<VAR>f : Fin n → α<VAR>r : α → α → Prop<GOAL>Sorted r (ofFn f) ↔ ((fun x x_1 => x < x_1) ⇒ r) f f
<VAR>n : ℕ<VAR>α : Type u<VAR>f : Fin n → α<VAR>r : α → α → Prop<GOAL>(∀ (i j : Fin (ofFn f).length), i < j → r (f (Fin.cast ⋯ i)) (f (Fin.cast ⋯ j))) ↔ ∀ ⦃a b : Fin n⦄, a < b → r (f a) (f b)
<VAR>a b c d a' b' c' : Ordinal.{u}<VAR>ha : a' < a<VAR>hb : b' < b<VAR>hc : c' < c<GOAL>a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') < a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
<VAR>a b c d a' b' c' : Ordinal.{u}<VAR>ha : a' < a<VAR>hb : b' < b<VAR>hc : c' < c<GOAL>b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' < b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>π : Prepartition I<GOAL>∀ᶠ (t : Finset (ι × ℝ)) in atTop, π ⊓ splitMany I t = (splitMany I t).filter fun J => ↑J ⊆ π.iUnion
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>π : Prepartition I<VAR>t : Finset (ι × ℝ)<VAR>ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J<GOAL>π ⊓ splitMany I t = (splitMany I t).filter fun J => ↑J ⊆ π.iUnion
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J✝ : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>π : Prepartition I<VAR>t : Finset (ι × ℝ)<VAR>ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J<VAR>J : Box ι<VAR>hJ : J ∈ π<GOAL>(splitMany I t).restrict J ≤ ((splitMany I t).filter fun J => ↑J ⊆ π.iUnion).restrict J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J✝ : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>π : Prepartition I<VAR>t : Finset (ι × ℝ)<VAR>ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ J' ∈ splitMany I_1 t, ¬Disjoint ↑J ↑J' → J' ≤ J<VAR>J : Box ι<VAR>hJ : J ∈ (splitMany I t).filter fun J => ↑J ⊆ π.iUnion<GOAL>∃ I' ∈ π, J ≤ I'
<VAR>G' : Type u_1<VAR>inst✝¹⁰ : AddGroup G'<VAR>inst✝⁹ : MeasurableSpace G'<VAR>inst✝⁸ : TopologicalSpace G'<VAR>inst✝⁷ : TopologicalAddGroup G'<VAR>inst✝⁶ : BorelSpace G'<VAR>μ' : Measure G'<VAR>Γ' : AddSubgroup G'<VAR>inst✝⁵ : Countable ↥Γ'<VAR>inst✝⁴ : MeasurableSpace (G' ⧸ Γ')<VAR>inst✝³ : BorelSpace (G' ⧸ Γ')<VAR>𝓕' : Set G'<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ'.IsAddRightInvariant<VAR>f : G' → K<VAR>f_ℒ_1 : Integrable f μ'<VAR>g : G' ⧸ Γ' → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ'.restrict 𝓕')) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))<VAR>h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'<VAR>π : G' → G' ⧸ Γ' := mk<GOAL>∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * automorphize f x ∂Measure.map mk (μ'.restrict 𝓕')