ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>r : M₀<VAR>n : ℕ<GOAL>inverse r ^ (n + 1) = inverse (r ^ (n + 1))
<VAR>K : Type u_1<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : TopologicalSpace K<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : TopologicalRing 𝕜<VAR>a b : 𝕜<VAR>h : a ≠ 0<VAR>x : 𝕜<GOAL>(fun y => (y - b) / a) ((fun x => a * x + b) x) = x
<VAR>K : Type u_1<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : TopologicalSpace K<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : TopologicalRing 𝕜<VAR>a b : 𝕜<VAR>h : a ≠ 0<VAR>x : 𝕜<GOAL>a * x / a = x
<VAR>K : Type u_1<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : TopologicalSpace K<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : TopologicalRing 𝕜<VAR>a b : 𝕜<VAR>h : a ≠ 0<VAR>y : 𝕜<GOAL>(fun x => a * x + b) ((fun y => (y - b) / a) y) = y
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<GOAL>f.Disjoint g ↔ _root_.Disjoint f.support g.support
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ * ‖1‖ < ‖k‖<GOAL>k ∈ ρ a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ * ‖1‖ < ‖k‖<GOAL>IsUnit (k • 1 - a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ * ‖1‖ < ‖k‖<VAR>a✝ : Nontrivial A<GOAL>IsUnit (k • 1 - a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ * ‖1‖ < ‖k‖<VAR>a✝ : Nontrivial A<VAR>hk : k ≠ 0<GOAL>IsUnit (k • 1 - a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ * ‖1‖ < ‖k‖<VAR>a✝ : Nontrivial A<VAR>hk : k ≠ 0<VAR>ku : Aˣ := (Units.map ↑↑ₐ) (Units.mk0 k hk)<GOAL>IsUnit (k • 1 - a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ < ‖1‖⁻¹ * ‖k‖<VAR>a✝ : Nontrivial A<VAR>hk : k ≠ 0<VAR>ku : Aˣ := (Units.map ↑↑ₐ) (Units.mk0 k hk)<GOAL>IsUnit (k • 1 - a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ < ‖1‖⁻¹ * ‖k‖<VAR>a✝ : Nontrivial A<VAR>hk : k ≠ 0<VAR>ku : Aˣ := (Units.map ↑↑ₐ) (Units.mk0 k hk)<VAR>hku : ‖-a‖ < ‖↑ku⁻¹‖⁻¹<GOAL>IsUnit (k • 1 - a)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.prod ν) (s ×ˢ t) = μ s * ν t
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>((traceForm R L M) ⁅x, y⁆) z = -((traceForm R L M) ⁅y, x⁆) z
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>-((traceForm R L M) ⁅y, x⁆) z = -((traceForm R L M) y) ⁅x, z⁆
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.45702, u_1} C<VAR>inst✝⁵ : Category.{?u.45706, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : h.left.IsPreservedBy F<VAR>inst✝ : h.right.IsPreservedBy F<GOAL>(h.left.map F).π ≫ (F.mapIso h.iso).hom ≫ (h.right.map F).ι = (h.left.map F).i ≫ (h.right.map F).p
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝³ : DecidableRel r<VAR>inst✝² : IsTrans α r<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTotal α r<VAR>s : Multiset α<VAR>a : α<GOAL>a ∈ sort r s ↔ a ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>n : ℕ<VAR>p q : R[X]<VAR>pn : p.natDegree ≤ n<GOAL>(p + q).natDegree ≤ n ↔ q.natDegree ≤ n
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>n : ℕ<VAR>p q : R[X]<VAR>pn : p.natDegree ≤ n<GOAL>(q + p).natDegree ≤ n ↔ q.natDegree ≤ n
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : Semigroup S<VAR>a✝ b c : S<VAR>hbc : Commute b c<VAR>a d : S<GOAL>a * b * (c * d) = a * c * (b * d)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<GOAL>⨅ k, lowerCentralSeries R L M k = posFittingComp R L M
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<GOAL>⨅ k, lowerCentralSeries R L M k ≤ posFittingComp R L M
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<GOAL>IsNilpotent R L (M ⧸ posFittingComp R L M)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<GOAL>∀ (x : L), _root_.IsNilpotent ((toEnd R L (M ⧸ posFittingComp R L M)) x)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>x : L<GOAL>_root_.IsNilpotent ((toEnd R L (M ⧸ posFittingComp R L M)) x)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>x : L<VAR>k : ℕ<VAR>hk : ∀ b ≥ k, ⨅ m, LinearMap.range ((toEnd R L M) x ^ m) = LinearMap.range ((toEnd R L M) x ^ b)<GOAL>_root_.IsNilpotent ((toEnd R L (M ⧸ posFittingComp R L M)) x)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>x : L<VAR>k : ℕ<VAR>hk : ∀ b ≥ k, ⨅ m, LinearMap.range ((toEnd R L M) x ^ m) = LinearMap.range ((toEnd R L M) x ^ b)<GOAL>(toEnd R L (M ⧸ posFittingComp R L M)) x ^ k = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>x : L<VAR>k : ℕ<VAR>hk : ∀ b ≥ k, ⨅ m, LinearMap.range ((toEnd R L M) x ^ m) = LinearMap.range ((toEnd R L M) x ^ b)<VAR>m : M<VAR>F : LieSubmodule R L M := posFittingComp R L M<VAR>x✝ : M ⧸ F<GOAL>((toEnd R L (M ⧸ F)) x ^ k) (Quot.mk Setoid.r m) = 0 (Quot.mk Setoid.r m)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>x : L<VAR>k : ℕ<VAR>m : M<VAR>F : LieSubmodule R L M := posFittingComp R L M<VAR>x✝ : M ⧸ F<VAR>hk : ((toEnd R L M) x ^ k) m ∈ F<GOAL>((toEnd R L (M ⧸ F)) x ^ k) (Quot.mk Setoid.r m) = 0 (Quot.mk Setoid.r m)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>x : L<VAR>k : ℕ<VAR>m : M<VAR>F : LieSubmodule R L M := posFittingComp R L M<VAR>x✝ : M ⧸ F<VAR>hk : ((toEnd R L M) x ^ k) m ∈ F<GOAL>((toEnd R L (M ⧸ F)) x ^ k) (LieSubmodule.Quotient.mk m) = LieSubmodule.Quotient.mk (((toEnd R L M) x ^ k) m)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>x : L<VAR>k : ℕ<VAR>m : M<VAR>F : LieSubmodule R L M := posFittingComp R L M<VAR>x✝ : M ⧸ F<VAR>hk : ((toEnd R L M) x ^ k) m ∈ F<VAR>this : (((toEnd R L (M ⧸ F)) x ^ k) ∘ₗ ↑(LieSubmodule.Quotient.mk' F)) m = (↑(LieSubmodule.Quotient.mk' F) ∘ₗ (toEnd R L M) x ^ k) m<GOAL>((toEnd R L (M ⧸ F)) x ^ k) (LieSubmodule.Quotient.mk m) = LieSubmodule.Quotient.mk (((toEnd R L M) x ^ k) m)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>p : Submodule K V<VAR>f : End K V<VAR>inst✝ : FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<GOAL>p = ⨆ μ, ⨆ k, p ⊓ (f.genEigenspace μ) k
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>u : Set α<VAR>hu : u.IsPWO<VAR>x : α × α<GOAL>x.swap ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u} → Ordinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{u}<GOAL>lift.{u, u} #ι < c
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<GOAL>μ s = μ t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : S<VAR>he : e ∈ f.range<VAR>he' : IsIdempotentElem e<GOAL>∃! e', IsIdempotentElem e' ∧ f e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e' : R<VAR>he₂ : IsIdempotentElem e'<VAR>he : f e' ∈ f.range<VAR>he' : IsIdempotentElem (f e')<GOAL>∃! e'_1, IsIdempotentElem e'_1 ∧ f e'_1 = f e'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>hy : y ∈ closure K<GOAL>∃ x ∈ K, Inseparable x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>hy : ∀ x ∈ K, ¬Inseparable x y<GOAL>y ∉ closure K
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>hy : ∀ x ∈ K, ¬Inseparable x y<VAR>this : Disjoint (𝓝 y) (𝓝ˢ K)<GOAL>y ∉ closure K
<VAR>R : Type u<VAR>inst₁ inst₂ : NonAssocSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonAssocSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring<VAR>h_zero : Zero.zero = Zero.zero<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonAssocSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring<VAR>h_zero : Zero.zero = Zero.zero<VAR>h_one' : MulOneClass.toOne = MulOneClass.toOne<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : NonAssocSemiring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring<VAR>h_zero : Zero.zero = Zero.zero<VAR>h_one' : MulOneClass.toOne = MulOneClass.toOne<VAR>h_one : One.one = One.one<GOAL>inst₁ = inst₂
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ✝ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ✝<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>ρ : Measure α := μ.withDensity f<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ✝ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ✝<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>ρ : Measure α := μ.withDensity f<VAR>this : IsFiniteMeasure ρ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ✝ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ✝<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>ρ : Measure α := μ.withDensity f<VAR>this : IsFiniteMeasure ρ<VAR>x : α<VAR>hx : Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))<VAR>h'x : (μ.withDensity f).rnDeriv μ x = f x<GOAL>Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ✝ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ✝<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>ρ : Measure α := μ.withDensity f<VAR>this : IsFiniteMeasure ρ<VAR>x : α<VAR>hx : Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))<VAR>h'x : (μ.withDensity f).rnDeriv μ x = f x<GOAL>Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 ((μ.withDensity f).rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ✝ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ✝<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>ρ : Measure α := μ.withDensity f<VAR>this : IsFiniteMeasure ρ<VAR>x : α<VAR>hx : Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))<VAR>h'x : (μ.withDensity f).rnDeriv μ x = f x<GOAL>(fun a => ρ a / μ a) =ᶠ[v.filterAt x] fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ✝ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ✝<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>ρ : Measure α := μ.withDensity f<VAR>this : IsFiniteMeasure ρ<VAR>x : α<VAR>hx : Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))<VAR>h'x : (μ.withDensity f).rnDeriv μ x = f x<VAR>a : Set α<VAR>ha : MeasurableSet a<GOAL>ρ a / μ a = (∫⁻ (y : α) in a, f y ∂μ) / μ a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<GOAL>‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y : E<VAR>r✝ : ℝ<VAR>p q : Seminorm 𝕜 E<VAR>e : E<VAR>r : ℝ<GOAL>(p ⊔ q).ball e r = p.ball e r ∩ q.ball e r
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Preorder β<VAR>inst✝⁵ : Preorder γ<VAR>inst✝⁴ : Preorder δ<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : MulOneClass β<VAR>inst✝¹ : MulOneClass γ<VAR>inst✝ : MulOneClass δ<VAR>f g✝ : α →*o β<VAR>g : β →*o γ<VAR>f₁ f₂ : α →*o β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>i : { x // x ∈ s }<GOAL>∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>i : { x // x ∈ s }<GOAL>∏ x ∈ map (Embedding.subtype fun x => x ∈ s) (s.attach.erase i), f x = ∏ j ∈ s.erase ((Embedding.subtype fun x => x ∈ s) i), f j
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>count p n = Fintype.card { k // k < n ∧ p k }
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>(Fintype.card ↑fun x => x < n ∧ p x) = Fintype.card { k // k < n ∧ p k }
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.214930}<VAR>α : Type u<VAR>s : Set α<VAR>a : α<VAR>h : a ∉ s<GOAL>#↑(insert a s) = #↑s + 1
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.214930}<VAR>α : Type u<VAR>s : Set α<VAR>a : α<VAR>h : a ∉ s<GOAL>Disjoint s {a}
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<GOAL>M.comul ≫ M.comul ▷ M.X = M.comul ≫ M.X ◁ M.comul ≫ (α_ M.X M.X M.X).inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y Z : C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>inst✝ : HasKernel f<GOAL>(kernelSubobject f).arrow ≫ f = 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y Z : C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>inst✝ : HasKernel f<GOAL>((kernelSubobjectIso f).hom ≫ kernel.ι f) ≫ f = 0
<VAR>R : Type u_1<VAR>inst✝ : CommMonoid R<VAR>x : R<VAR>h : Irreducible x<VAR>y z : R<VAR>hz : x = y * y * z<GOAL>IsUnit y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoid R<VAR>x : R<VAR>h : Irreducible x<VAR>y z : R<VAR>hz : x = y * (y * z)<GOAL>IsUnit y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoid R<VAR>x : R<VAR>h : Irreducible x<VAR>y z : R<VAR>hz : x = y * (y * z)<VAR>hu : IsUnit y<GOAL>IsUnit y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoid R<VAR>x : R<VAR>h : Irreducible x<VAR>y z : R<VAR>hz : x = y * (y * z)<VAR>hu : IsUnit (y * z)<GOAL>IsUnit y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m d : ℕ<VAR>hm : n ∣ m<VAR>hd : m ∣ d<GOAL>(changeLevel ⋯) χ = (changeLevel hd) ((changeLevel hm) χ)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hn : n ≠ 0<VAR>hs : n ≤ s.card<GOAL>∃ P, P.IsEquipartition ∧ P.parts.card = n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hn : 0 < n<VAR>hs : n ≤ s.card<GOAL>∃ P, P.IsEquipartition ∧ P.parts.card = n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hn : 0 < n<VAR>hs : n ≤ s.card<VAR>this : (n - s.card % n) * (s.card / n) + s.card % n * (s.card / n + 1) = s.card<GOAL>∃ P, P.IsEquipartition ∧ P.parts.card = n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hn : 0 < n<VAR>hs : n ≤ s.card<VAR>this : (n - s.card % n) * (s.card / n) + s.card % n * (s.card / n + 1) = s.card<GOAL>(equitabilise this).parts.card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>inst✝ : DenselyOrdered α<VAR>h₁ : a₁ < b₁<VAR>h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂<GOAL>a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>inst✝ : DenselyOrdered α<VAR>h₁ : a₁ < b₁<VAR>h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂<VAR>x : α<VAR>xa : a₁ < x<VAR>xb : x < b₁<GOAL>a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>inst✝ : DenselyOrdered α<VAR>h₁ : a₁ < b₁<VAR>h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂<VAR>x : α<VAR>xa : a₁ < x<VAR>xb : x < b₁<VAR>h' : a₁ < a₂<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>inst✝ : DenselyOrdered α<VAR>h₁ : a₁ < b₁<VAR>h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂<VAR>x : α<VAR>xa : a₁ < x<VAR>xb : x < b₁<VAR>h' : b₂ < b₁<GOAL>False