ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>g f : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>this : ContinuousOn (g ∘ f) (spectrum R a)<VAR>sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a<GOAL>∀ (x : ↑(spectrum R a)), { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } x = ↑(?f' x)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<GOAL>count K v ↑v.asIdeal = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>hv : ↑v.asIdeal ≠ 0<GOAL>count K v ↑v.asIdeal = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>hv : ↑v.asIdeal ≠ 0<VAR>h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal<GOAL>count K v ↑v.asIdeal = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>hv : ↑v.asIdeal ≠ 0<VAR>h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal<VAR>hv_irred : Irreducible (Associates.mk v.asIdeal)<GOAL>count K v ↑v.asIdeal = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<VAR>n : ℕ<GOAL>s.drop n ~ʷ t.drop n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>r : α → α → Prop<VAR>hr : ∀ (a : α), 1 < count a l → r a a<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b<GOAL>Pairwise r l
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>r : α → α → Prop<VAR>hr : ∀ (a : α), 1 < count a l → r a a<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b<GOAL>∀ {a b : α}, [a, b] <+ l → r a b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>r : α → α → Prop<VAR>hr : ∀ (a : α), 1 < count a l → r a a<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b<VAR>a b : α<VAR>hab : [a, b] <+ l<GOAL>r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : NullMeasurableSet s μ<GOAL>s =ᶠ[ae μ] univ ↔ μ s = μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : NullMeasurableSet s μ<VAR>h : μ s = μ univ<GOAL>s =ᶠ[ae μ] univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t✝ : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : NullMeasurableSet s μ<VAR>h : μ s = μ univ<VAR>t : Set α<VAR>ht₁ : MeasurableSet t<VAR>ht₂ : t =ᶠ[ae μ] s<GOAL>s =ᶠ[ae μ] univ
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x
<VAR>f : Bool → Bool → Bool<GOAL>bitwise f = binaryRec (fun n => bif f false true then n else 0) fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)
<VAR>f : Bool → Bool → Bool<VAR>x y : ℕ<GOAL>bitwise f x y = binaryRec (fun n => bif f false true then n else 0) (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) x y
<VAR>p : Char → Bool<VAR>s : String<GOAL>(s.dropWhile p).data = List.dropWhile p s.data
<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>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁵ : AddCommMonoid M'✝<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M'✝<VAR>inst✝² : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>B : BilinForm R₁ M₁<VAR>b : B.Nondegenerate<VAR>φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁<VAR>hψ₁ : B.IsAdjointPair B ψ₁ φ<VAR>hψ₂ : B.IsAdjointPair B ψ₂ φ<VAR>v w : M₁<GOAL>((B.compLeft ψ₁) v) w = ((B.compLeft ψ₂) v) w
<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>hs : MeasurableSet s<VAR>t : Set ↑s<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : ↑s) in t, f ↑x ∂Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>∀ (x : α), x ∈ Ioc a b \ Ioi c ↔ x ∈ Ioc a (min b c)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : Fix F<GOAL>(mk ∘ dest) x = id x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x : Fix F<GOAL>∀ (x : F (Fix F)), (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x✝ : Fix F<VAR>x : F (Fix F)<GOAL>(mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x✝ : Fix F<VAR>x : F (Fix F)<GOAL>mk <$> rec (Functor.map mk) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 < b<GOAL>a / b ≤ 1 ↔ a ≤ b
<VAR>r p : ℝ<VAR>hp : 0 ≤ p<GOAL>r.toNNReal ≤ p.toNNReal ↔ r ≤ p
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x : Completion α<GOAL>dist x x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x : Completion α<GOAL>IsClosed {a | dist a a = 0}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>x : Completion α<GOAL>∀ (a : α), dist (↑α a) (↑α a) = 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>el : { x // x ∈ filter (fun p => p.card = s.card / P.parts.card + 1) P.parts } ≃ Fin (filter (fun p => p.card = s.card / P.parts.card + 1) P.parts).card := (filter (fun p => p.card = s.card / P.parts.card + 1) P.parts).equivFin<VAR>es : { x // x ∈ filter (fun p => p.card = s.card / P.parts.card) P.parts } ≃ Fin (filter (fun p => p.card = s.card / P.parts.card) P.parts).card := (filter (fun p => p.card = s.card / P.parts.card) P.parts).equivFin<GOAL>∃ f, ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>es : { x // x ∈ filter (fun p => p.card = s.card / P.parts.card) P.parts } ≃ Fin (filter (fun p => p.card = s.card / P.parts.card) P.parts).card := (filter (fun p => p.card = s.card / P.parts.card) P.parts).equivFin<VAR>el : { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card + 1 } ≃ Fin (s.card % P.parts.card)<GOAL>∃ f, ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>el : { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card + 1 } ≃ Fin (s.card % P.parts.card)<VAR>es : { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card } ≃ Fin (P.parts.card - s.card % P.parts.card)<GOAL>∃ f, ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>el : { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card + 1 } ≃ Fin (s.card % P.parts.card)<VAR>es : { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card } ≃ Fin (P.parts.card - s.card % P.parts.card)<VAR>sneg : { x // x ∈ P.parts ∧ ¬x.card = s.card / P.parts.card + 1 } ≃ { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card } := (Equiv.refl (Finset α)).subtypeEquiv ⋯<GOAL>∃ f, ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>sneg : { x // x ∈ P.parts ∧ ¬x.card = s.card / P.parts.card + 1 } ≃ { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card } := (Equiv.refl (Finset α)).subtypeEquiv ⋯<VAR>el : { x // (↑x).card = s.card / P.parts.card + 1 } ≃ Fin (s.card % P.parts.card)<VAR>es : { x // ¬(↑x).card = s.card / P.parts.card + 1 } ≃ Fin (P.parts.card - s.card % P.parts.card)<VAR>f : { x // x ∈ P.parts } ≃ Fin (s.card % P.parts.card + (P.parts.card - s.card % P.parts.card)) := (Equiv.sumCompl fun a => (↑a).card = s.card / P.parts.card + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)<GOAL>∃ f, ∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>sneg : { x // x ∈ P.parts ∧ ¬x.card = s.card / P.parts.card + 1 } ≃ { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card } := (Equiv.refl (Finset α)).subtypeEquiv ⋯<VAR>el : { x // (↑x).card = s.card / P.parts.card + 1 } ≃ Fin (s.card % P.parts.card)<VAR>es : { x // ¬(↑x).card = s.card / P.parts.card + 1 } ≃ Fin (P.parts.card - s.card % P.parts.card)<VAR>f : { x // x ∈ P.parts } ≃ Fin (s.card % P.parts.card + (P.parts.card - s.card % P.parts.card)) := (Equiv.sumCompl fun a => (↑a).card = s.card / P.parts.card + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)<GOAL>∀ (t : { x // x ∈ P.parts }), (↑t).card = s.card / P.parts.card + 1 ↔ ↑((f.trans (finCongr ⋯)) t) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>sneg : { x // x ∈ P.parts ∧ ¬x.card = s.card / P.parts.card + 1 } ≃ { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card } := (Equiv.refl (Finset α)).subtypeEquiv ⋯<VAR>el : { x // (↑x).card = s.card / P.parts.card + 1 } ≃ Fin (s.card % P.parts.card)<VAR>es : { x // ¬(↑x).card = s.card / P.parts.card + 1 } ≃ Fin (P.parts.card - s.card % P.parts.card)<VAR>f : { x // x ∈ P.parts } ≃ Fin (s.card % P.parts.card + (P.parts.card - s.card % P.parts.card)) := (Equiv.sumCompl fun a => (↑a).card = s.card / P.parts.card + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)<VAR>p : Finset α<VAR>property✝ : p ∈ P.parts<GOAL>(↑⟨p, property✝⟩).card = s.card / P.parts.card + 1 ↔ ↑((f.trans (finCongr ⋯)) ⟨p, property✝⟩) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>sneg : { x // x ∈ P.parts ∧ ¬x.card = s.card / P.parts.card + 1 } ≃ { x // x ∈ P.parts ∧ x.card = s.card / P.parts.card } := (Equiv.refl (Finset α)).subtypeEquiv ⋯<VAR>el : { x // (↑x).card = s.card / P.parts.card + 1 } ≃ Fin (s.card % P.parts.card)<VAR>es : { x // ¬(↑x).card = s.card / P.parts.card + 1 } ≃ Fin (P.parts.card - s.card % P.parts.card)<VAR>f : { x // x ∈ P.parts } ≃ Fin (s.card % P.parts.card + (P.parts.card - s.card % P.parts.card)) := (Equiv.sumCompl fun a => (↑a).card = s.card / P.parts.card + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)<VAR>p : Finset α<VAR>property✝ : p ∈ P.parts<GOAL>p.card = s.card / P.parts.card + 1 ↔ ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a => (↑a).card = s.card / P.parts.card + 1).symm ⟨p, property✝⟩))) < s.card % P.parts.card
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<VAR>Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid<VAR>compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B<GOAL>∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<VAR>Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid<VAR>compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B<VAR>H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}<GOAL>∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<VAR>Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid<VAR>compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B<VAR>H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}<VAR>x : X<VAR>hx : x ∈ ⋂ Q, Q.proj ⁻¹' {Qs Q}<GOAL>∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>h : Group.IsNilpotent (G ⧸ center G)<GOAL>Group.IsNilpotent G
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>h : Group.IsNilpotent (G ⧸ center G)<VAR>n : ℕ<VAR>hn : upperCentralSeries (G ⧸ center G) n = ⊤<GOAL>Group.IsNilpotent G
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>h : Group.IsNilpotent (G ⧸ center G)<VAR>n : ℕ<VAR>hn : upperCentralSeries (G ⧸ center G) n = ⊤<GOAL>upperCentralSeries G n.succ = ⊤
<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>f : R → R<VAR>n : ℕ<VAR>a : A<VAR>hf : autoParam (ContinuousOn f ((fun x => x ^ n) '' spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f (x ^ n)) a = cfc f (a ^ n)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>p q : ℚ<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedField K<GOAL>0 < ↑q ↔ 0 < q
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<GOAL>eLpNorm f p μ = (∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal)
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>α : Type u_2<VAR>f : M × ↥S → α<VAR>wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p'<VAR>m : M<VAR>s : ↥S<GOAL>(mk m s).liftOn f wd = f (m, s)
<VAR>f : ℝ → ℝ<VAR>p : ℤ<VAR>hf : GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<GOAL>GrowsPolynomially fun x => f x ^ p
<VAR>f : ℝ → ℝ<VAR>p : ℤ<VAR>hf : GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<GOAL>GrowsPolynomially fun x => f x ^ ↑p
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ r p q : R[X]<GOAL>(p * q).coeff 0 = p.coeff 0 * q.coeff 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I J✝ J : FractionalIdeal R₁⁰ K<VAR>h : J ≠ 0<GOAL>↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J
<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✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : AddCommGroup N<VAR>f : M → N<VAR>x y : M<GOAL>polar f x y = polar f y x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ s t : Multiset α<VAR>i : α<GOAL>(toDFinsupp (s ∩ t)) i = (toDFinsupp s ⊓ toDFinsupp t) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R✝ : Type u_3<VAR>s✝ t : Finset α<VAR>a b : α<VAR>inst✝¹ : DecidableEq α<VAR>R : Type u_4<VAR>inst✝ : AddGroupWithOne R<VAR>s : Finset α<VAR>hs : a ∈ s<GOAL>↑(s.erase a).card = ↑s.card - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R✝ : Type u_3<VAR>s✝ t : Finset α<VAR>a b : α<VAR>inst✝¹ : DecidableEq α<VAR>R : Type u_4<VAR>inst✝ : AddGroupWithOne R<VAR>s : Finset α<VAR>hs : a ∈ s<GOAL>1 ≤ s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R✝ : Type u_3<VAR>s✝ t : Finset α<VAR>a b : α<VAR>inst✝¹ : DecidableEq α<VAR>R : Type u_4<VAR>inst✝ : AddGroupWithOne R<VAR>s : Finset α<VAR>hs : a ∈ s<GOAL>s.Nonempty
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>L R : ListBlank Γ<GOAL>move Dir.left (mk' L R) = mk' L.tail (ListBlank.cons L.head R)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>x ∈ closure (Set.range Int.cast)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>IsClosed {b | b ∈ closure (Set.range Int.cast)}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝² : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : MetrizableSpace γ<VAR>hm : m ≤ m0<VAR>f g : β → γ<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<GOAL>f =ᶠ[ae (μ.trim hm)] g
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝² : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : MetrizableSpace γ<VAR>hm : m ≤ m0<VAR>f g : β → γ<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<GOAL>MeasurableSet {a | ¬f a = g a}
<VAR>m n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : c ≡ d [ZMOD n]<GOAL>a - c ≡ b - d [ZMOD n]
<VAR>m n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : c ≡ d [ZMOD n]<GOAL>a + -c ≡ b + -d [ZMOD n]
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ'.haarScalarFactor μ • μ s ≤ μ' s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>r : ℝ≥0∞<VAR>hr : r < μ'.haarScalarFactor μ • μ s<GOAL>r < μ' s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>r : ℝ≥0∞<VAR>hr : r < μ'.haarScalarFactor μ • μ s<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<GOAL>r < μ' s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>r : ℝ≥0∞<VAR>hr : r < μ'.haarScalarFactor μ • μ s<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>this : ν s ≠ ⊤<GOAL>r < μ' s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>r : ℝ≥0∞<VAR>hr : r < μ'.haarScalarFactor μ • μ s<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>this : ν s ≠ ⊤<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>f_comp : HasCompactSupport f<VAR>hf : f ⁻¹' {1} ⊆ s<VAR>νf : r < ν (f ⁻¹' {1})<GOAL>r < μ' s
<VAR>α : Type u_1<VAR>a : PosNum<GOAL>sub' 1 (a + a) = (neg a).bit1
<VAR>α : Type u_1<VAR>a : PosNum<GOAL>a.bit0.pred'.toZNumNeg = (neg a).bit1
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (x + ↑n) ↔ LiouvilleWith p x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>m : Multiset α<VAR>r : α → α → Prop<GOAL>(∀ x ∈ m, r x x) → Rel r m m
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>m : Multiset α<VAR>r : α → α → Prop<GOAL>(∀ x ∈ 0, r x x) → Rel r 0 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>m : Multiset α<VAR>r : α → α → Prop<GOAL>∀ (a : α) (s : Multiset α), ((∀ x ∈ s, r x x) → Rel r s s) → (∀ x ∈ a ::ₘ s, r x x) → Rel r (a ::ₘ s) (a ::ₘ s)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x : T<GOAL>∃ y, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1