ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>ℵ₀ ≤ cof 0 ↔ IsLimit 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>ℵ₀ ≤ (succ o).cof ↔ (succ o).IsLimit
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<VAR>l : o.IsLimit<GOAL>ℵ₀ ≤ o.cof ↔ o.IsLimit
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p q : α<VAR>hcontra : p = q<VAR>hp : p ≠ 0<VAR>x : α<VAR>hx' : ¬IsUnit x<VAR>hx'' : q = p * x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p q : α<VAR>hcontra : p = q<VAR>hp : p ≠ 0<VAR>x : α<VAR>hx' : ¬IsUnit x<VAR>hx'' : p * 1 = p * x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p q : α<VAR>hcontra : p = q<VAR>hp : p ≠ 0<VAR>x : α<VAR>hx' : ¬IsUnit 1<VAR>hx'' : p * 1 = p * x<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g' : Z ⟶ W<VAR>inst✝² : HasPushout f g<VAR>inst✝¹ : HasPushout (pushout.inr f g) g'<VAR>inst✝ : HasPushout f (g ≫ g')<GOAL>pushout.inr f (g ≫ g') ≫ (pushoutLeftPushoutInrIso f g g').inv = pushout.inr (pushout.inr f g) g'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>s.card / P.parts.card ≤ t.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>(∑ i ∈ P.parts, i.card) / P.parts.card ≤ t.card
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>A : Type u_3<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>f : ℕ → A<VAR>n : ℕ<GOAL>(aeval f) (W_ R n) = ∑ i ∈ range (n + 1), ↑p ^ i * f i ^ p ^ (n - i)
<VAR>a b c d m✝ n : ℤ<VAR>m : ℕ<GOAL>m < n.toNat ↔ ↑m < n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v w : Fin 3 → R<GOAL>w ⬝ᵥ (crossProduct v) w = 0
<VAR>I : Type u<VAR>inst✝⁵ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.157279, u_1} C<VAR>inst✝³ : MonoidalCategory C<VAR>X₁ X₂ X₃ X₄ : GradedObject I C<VAR>inst✝² : X₃.HasTensor X₄<VAR>inst✝¹ : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>i₁ i₂ i₃ i₄ j : I<VAR>h : i₁ + i₂ + i₃ + i₄ = j<VAR>i₂₃₄ : I<VAR>hi : i₂ + i₃ + i₄ = i₂₃₄<GOAL>i₁ + i₂₃₄ = j
<VAR>a b : ℝ<VAR>f : C(↑(Set.Icc a b), ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<GOAL>∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
<VAR>a b : ℝ<VAR>f : C(↑(Set.Icc a b), ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>w : ∃ᶠ (x : C(↑(Set.Icc a b), ℝ)) in nhds f, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring<GOAL>∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
<VAR>a b : ℝ<VAR>f : C(↑(Set.Icc a b), ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring<GOAL>∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
<VAR>a b : ℝ<VAR>f : C(↑(Set.Icc a b), ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring<VAR>m : ℝ[X]<VAR>H : ↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m ∈ Metric.ball f ε<GOAL>∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
<VAR>a b : ℝ<VAR>f : C(↑(Set.Icc a b), ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring<VAR>m : ℝ[X]<VAR>H : ‖↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m - f‖ < ε<GOAL>∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<GOAL>IsUnit f ↔ IsUnit (map φ f)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h : IsUnit (map φ f)<GOAL>IsUnit f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h : IsUnit (map φ f)<VAR>u : Sˣ<VAR>hu : C ↑u = map φ f<GOAL>IsUnit f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h : IsUnit (map φ f)<VAR>u : Sˣ<VAR>hu : C ↑u = map φ f<VAR>hdeg : (C ↑u).degree = 0<GOAL>IsUnit f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h : IsUnit (map φ f)<VAR>u : Sˣ<VAR>hu : C ↑u = map φ f<VAR>hdeg : f.degree = 0<GOAL>IsUnit f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : (C (f.coeff 0)).IsPrimitive<VAR>h : IsUnit (map φ f)<VAR>u : Sˣ<VAR>hu : C ↑u = map φ f<VAR>hdeg : f.degree = 0<GOAL>IsUnit (C (f.coeff 0))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ f g : ι →₀ α<VAR>s✝ : Finset ι<VAR>hf : f.support ⊆ s✝<VAR>h : ∀ i ∈ s✝, f i ≤ g i<VAR>s : ι<GOAL>f s ≤ g s
<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>s : Finset α<VAR>n : ℤ<VAR>f : α → ℤ<GOAL>(Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n
<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>s : Finset α<VAR>n : ℤ<VAR>f : α → ℤ<GOAL>(Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).prod % n = (Multiset.map (fun i => f i % n) s.val).prod % n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>borel ℝ = generateFrom (⋃ a, {Ioi ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>generateFrom (range Ioi) = generateFrom (⋃ a, {Ioi ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>∀ t ∈ range Ioi, MeasurableSet t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>a : ℝ<GOAL>MeasurableSet (Ioi a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>a : ℝ<VAR>this : IsGLB (range Rat.cast ∩ Ioi a) a<GOAL>MeasurableSet (Ioi a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>a : ℝ<VAR>this : IsGLB (range Rat.cast ∩ Ioi a) a<GOAL>MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi ↑y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<GOAL>Primrec₂ fun p => encode
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<GOAL>Primrec₂ fun p a => p.1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>mixedEmbedding.norm x = 0 ↔ ∃ w, (normAtPlace w) x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>x✝ y✝ : E<VAR>inst✝ : Invertible 2<VAR>x y : E<GOAL>x ∈ [x + y-[𝕜]x - y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>x✝ y✝ : E<VAR>inst✝ : Invertible 2<VAR>x y : E<GOAL>x = midpoint 𝕜 (x + y) (x - y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>∀ (x y : A), (fun a => a • baseChangeHom R A M N) (x + y) = (fun a => a • baseChangeHom R A M N) x + (fun a => a • baseChangeHom R A M N) y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>∀ (m x : A), { toFun := fun a => a • baseChangeHom R A M N, map_add' := ⋯ }.toFun (m • x) = (RingHom.id A) m • { toFun := fun a => a • baseChangeHom R A M N, map_add' := ⋯ }.toFun x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<GOAL>iteratedDeriv n f x = deriv^[n] f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<GOAL>iteratedDerivWithin n f univ x = deriv^[n] f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝¹ x : 𝕜<VAR>x✝ : 𝕜 → F<GOAL>deriv x✝ = derivWithin x✝ univ
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(node s l x r).toList = l.toList ++ x :: r.toList
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList
<VAR>a : Prop<VAR>l : List Prop<GOAL>(a :: a :: l).TFAE ↔ (a :: l).TFAE
<VAR>θ ψ : ℝ<GOAL>↑(toIocMod two_pi_pos ψ θ) = ↑θ
<VAR>θ ψ : ℝ<GOAL>∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k
<VAR>θ ψ : ℝ<GOAL>toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>closure E ⊆ cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>cthickening (min δ 0) E ⊆ cthickening δ E
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>y ∈ closedBall x ε ↔ dist x y ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs ys : List α<VAR>h : xs ~ ys<GOAL>xs.sym2 ~ ys.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f g : α → β<VAR>hp : 1 ≤ p<VAR>hp_ne_top : p ≠ ⊤<VAR>hg : Memℒp g p μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f g : α → β<VAR>hp : 1 ≤ p<VAR>hp_ne_top : p ≠ ⊤<VAR>hg : Memℒp g p μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ<VAR>hδ_pos : 0 < δ<VAR>hgδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T T' : Set α → E →L[ℝ] F<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ f.range, (T (↑f ⁻¹' {x})) x = ∑ x ∈ f.range, (T' (↑f ⁻¹' {x})) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T T' : Set α → E →L[ℝ] F<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>x✝ : x ∈ f.range<GOAL>(T (↑f ⁻¹' {x})) x = (T' (↑f ⁻¹' {x})) x
<VAR>s : ℂ<GOAL>((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral
<VAR>s : ℂ<GOAL>∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) = ∫ (x : ℝ) in Ioi 0, (starRingEnd ℂ) (↑(rexp (-x)) * ↑x ^ (s - 1))
<VAR>s : ℂ<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) = (starRingEnd ℂ) (↑(rexp (-x)) * ↑x ^ (s - 1))
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<GOAL>↑n ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>mu : N → N → N<VAR>inst✝ : IsSymmOp N N mu<GOAL>Covariant N N (flip mu) r ↔ Covariant N N mu r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>k : α<VAR>h : m.buckets.WF<GOAL>((m.buckets.update (mkIdx ⋯ (hash k).toUSize).val AssocList.nil ⋯).update (mkIdx ⋯ (hash k).toUSize).val (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>k : α<VAR>h : m.buckets.WF<GOAL>(m.buckets.update (mkIdx ⋯ (hash k).toUSize).val (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>inst✝³ : BEq α<VAR>inst✝² : Hashable α<VAR>m : Imp α β<VAR>k : α<VAR>h : m.buckets.WF<VAR>inst✝¹ : PartialEquivBEq α<VAR>inst✝ : LawfulHashable α<VAR>H : List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val].toList<GOAL>List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none) m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat].toList)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>k : α<VAR>h✝ : m.buckets.WF<VAR>H : AssocList.All (fun k_1 x => ((hash k_1).toUSize % m.buckets.val.size).toNat = (mkIdx ⋯ (hash k).toUSize).val.toNat) m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val]<VAR>a : α × β<VAR>h : a ∈ List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none) m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat].toList<GOAL>((hash a.fst).toUSize % m.buckets.val.size).toNat = (mkIdx ⋯ (hash k).toUSize).val.toNat
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : SeminormedRing α<VAR>inst✝ : NormOneClass α<VAR>a : α<VAR>n : ℕ<GOAL>‖a ^ Nat.zero‖ ≤ ‖a‖ ^ Nat.zero
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>(∃ S ⊆ {t | IsOpen t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔ ∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a b : Associates α<VAR>x✝¹ x✝ : α<GOAL>(⟦x✝¹⟧ * ⟦x✝⟧).out = Associates.out ⟦x✝¹⟧ * Associates.out ⟦x✝⟧
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<GOAL>c < (succ c).ord.cof
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : ⟦α⟧ = succ c<GOAL>c < (succ c).ord.cof
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<GOAL>c < (succ c).ord.cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<GOAL>c < (succ c).ord.cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (succ c).ord.IsLimit<GOAL>c < (succ c).ord.cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<GOAL>c < (type r).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<GOAL>c < (type r).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<GOAL>c < #↑S
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<GOAL>c * c < #↑S * c
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<GOAL>#α ≤ sum fun x => c
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<GOAL>#α ≤ sum fun x => (typein r ↑x).card
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h : ℵ₀ ≤ c<VAR>α : Type u<VAR>αe : #α = succ c<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<VAR>i : ↑S<GOAL>(fun x => (typein r ↑x).card) i ≤ c
<VAR>x y : EReal<GOAL>min (-x) (-y) = -max x y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P : C<VAR>hP : PreservesFiniteColimits (preadditiveCoyonedaObj (op P))<GOAL>Projective P
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P : C<VAR>hP : PreservesFiniteColimits (preadditiveCoyonedaObj (op P))<GOAL>(preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>‖integral μ f‖ ≤ integral μ (map norm f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : μ s < ⊤<GOAL>‖weightedSMul μ s‖ ≤ 1 * (μ s).toReal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>σₙ R (((↑(cfcHom ha)).comp ((↑(compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom)) f) = range ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>spectrum R (((↑(cfcHom ha)).comp ((↑(compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom)) f) ∪ {0} = range ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>spectrum R ((cfcHom ha) ((compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f))) ∪ {0} = range ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : CompleteSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>range ⇑((compStarAlgHom' R R { toFun := inclusion ⋯, continuous_toFun := ⋯ }) (toContinuousMapHom f)) ∪ {0} = range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<GOAL>a * b + b * a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<VAR>this : a + b = a + b + (a * b + b * a)<GOAL>a * b + b * a = 0
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Z : C<GOAL>f ▷ (Y ⊗ Z) = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Z : C<GOAL>f ⊗ 𝟙 (Y ⊗ Z) = (α_ X Y Z).inv ≫ ((f ⊗ 𝟙 Y) ⊗ 𝟙 Z) ≫ (α_ X' Y Z).hom
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Z : C<GOAL>f ⊗ 𝟙 (Y ⊗ Z) = (α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ (f ⊗ 𝟙 Y ⊗ 𝟙 Z)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>f : ι → α<GOAL>Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)