ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X : Type w'<VAR>inst✝² : TopologicalSpace X<VAR>Z B : C<VAR>π : Z ⟶ B<VAR>inst✝¹ : HasPullback π π<VAR>inst✝ : PreservesLimit (cospan π π) G<VAR>a : C(↑(G.obj Z), X)<VAR>ha : ⇑a ∘ ⇑(G.map (pullback.fst π π)) = ⇑a ∘ ⇑(G.map (pullback.snd π π))<VAR>x y : ↑(G.obj Z)<VAR>hxy : (G.map π) x = (G.map π) y<VAR>xy : ↑(G.obj (pullback π π)) := (PreservesPullback.iso G π π).inv ((TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv ⟨(x, y), hxy⟩)<VAR>ha' : a (↑⟨(x, y), hxy⟩).1 = a (↑⟨(x, y), hxy⟩).2<VAR>h₁ : ∀ (y : ↑(pullback (G.map π) (G.map π))), (G.map (pullback.fst π π)) ((PreservesPullback.iso G π π).inv y) = (pullback.fst (G.map π) (G.map π)) y<VAR>h₂ : ∀ (y : ↑(pullback (G.map π) (G.map π))), (G.map (pullback.snd π π)) ((PreservesPullback.iso G π π).inv y) = (pullback.snd (G.map π) (G.map π)) y<GOAL>a x = a y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>x : (P F).W α<GOAL>recF g x = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' x))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>x : (P F).W α<GOAL>∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α), recF g ((P F).wMk a f' f) = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk a f' f)))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>x : (P F).W α<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<GOAL>recF g ((P F).wMk a f' f) = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk a f' f)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<GOAL>(fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) =ᶠ[ae (ν a)] fun b => f (a, b) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a✝ : α<VAR>q : ℚ<VAR>a : β<VAR>ha : IsRatStieltjesPoint f (a✝, a)<GOAL>↑(stieltjesOfMeasurableRat f ⋯ (a✝, a)) ↑q = f (a✝, a) q
<VAR>n : ℕ<GOAL>n.smoothNumbers = factoredNumbers n.primesBelow
<VAR>n : ℕ<GOAL>factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow
<VAR>n m : ℕ<VAR>hm : m ∈ factoredNumbers (Finset.range n)<GOAL>m ∈ factoredNumbers n.primesBelow
<VAR>n m : ℕ<VAR>hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n<GOAL>∀ (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>x : A<GOAL>x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure ∅) ↔ x = 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g σ : Perm α<GOAL>σ.support = ∅ ↔ σ = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<GOAL>Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ last n<GOAL>b < (a.castPred ha).succ ↔ b ≤ a
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⟶ R₂<VAR>c : C<GOAL>adj₁.unit.app c ≫ α.app (L₁.obj c) = adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⟶ R₂<VAR>c : C<GOAL>adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) = adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)
<VAR>n : ℕ<GOAL>(n + 1 + 1).choose (n + 1) = n + 1 + 1
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<GOAL>nndist z ((starRingEnd ℂ) z) = 2 * Real.nnabs z.im
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>s : Multiset α<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>p_one : p 1<VAR>p_s : ∀ a ∈ s, p a<GOAL>p s.prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>s : Multiset α<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>p_one : p 1<VAR>p_s : ∀ a ∈ s, p a<GOAL>p (foldr (fun x x_1 => x * x_1) ⋯ 1 s)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : Preadditive C<VAR>J : Type<VAR>inst✝³ : Fintype J<VAR>f✝ : J → C<VAR>inst✝² : HasBiproduct f✝<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>P : C<VAR>x : (j : J) → P ⟶ f j<VAR>m : (j : J) → (k : K) → f j ⟶ g k<VAR>j✝ : K<GOAL>(lift x ≫ matrix m) ≫ π g j✝ = (lift fun k => ∑ j : J, x j ≫ m j k) ≫ π g j✝
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>P : Ideal R<VAR>hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P<VAR>n : ℕ<VAR>hf0 : ¬f = 0<GOAL>(map (mk P) f).coeff n = (C ((mk P) f.leadingCoeff) * X ^ f.natDegree).coeff n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>P : Ideal R<VAR>hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P<VAR>n : ℕ<VAR>hf0 : ¬f = 0<VAR>h : ↑n < f.degree<GOAL>(map (mk P) f).coeff n = (C ((mk P) f.leadingCoeff) * X ^ f.natDegree).coeff n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>P : Ideal R<VAR>hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P<VAR>n : ℕ<VAR>hf0 : ¬f = 0<VAR>h : ↑n = f.degree<GOAL>(map (mk P) f).coeff n = (C ((mk P) f.leadingCoeff) * X ^ f.natDegree).coeff n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>P : Ideal R<VAR>hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P<VAR>n : ℕ<VAR>hf0 : ¬f = 0<VAR>h : f.degree < ↑n<GOAL>(map (mk P) f).coeff n = (C ((mk P) f.leadingCoeff) * X ^ f.natDegree).coeff n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>b : β<VAR>s : Multiset α<VAR>t : Multiset β<VAR>l₁ : List α<VAR>l₂ : List β<VAR>d₁ : Nodup ⟦l₁⟧<VAR>d₂ : Nodup ⟦l₂⟧<GOAL>(⟦l₁⟧ ×ˢ ⟦l₂⟧).Nodup
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M'<VAR>ι✝ : Type u_4<VAR>inst✝² : DecidableEq ι✝<VAR>inst✝¹ : Fintype ι✝<VAR>e✝ : Basis ι✝ R M<VAR>ι : Type u_5<VAR>inst✝ : Finite ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<VAR>h : f ⇑e = 0<GOAL>f = 0
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M'<VAR>ι✝ : Type u_4<VAR>inst✝² : DecidableEq ι✝<VAR>inst✝¹ : Fintype ι✝<VAR>e✝ : Basis ι✝ R M<VAR>ι : Type u_5<VAR>inst✝ : Finite ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<VAR>h : f ⇑e = 0<VAR>val✝ : Fintype ι<GOAL>f = 0
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M'<VAR>ι✝ : Type u_4<VAR>inst✝² : DecidableEq ι✝<VAR>inst✝¹ : Fintype ι✝<VAR>e✝ : Basis ι✝ R M<VAR>ι : Type u_5<VAR>inst✝ : Finite ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<VAR>h : f ⇑e = 0<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>f = 0
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>P : Subgroup G<VAR>hP : IsPGroup p ↥P<VAR>c : Set (Subgroup G)<VAR>hc1 : c ⊆ {Q | IsPGroup p ↥Q}<VAR>hc2 : IsChain (fun x x_1 => x ≤ x_1) c<VAR>Q : Subgroup G<VAR>hQ : Q ∈ c<VAR>x✝ : ↥{ carrier := ⋃ R, ↑↑R, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }<VAR>g : G<VAR>S : ↑c<VAR>hg : g ∈ (fun R => ↑↑R) S<GOAL>∃ k, ⟨g, ⋯⟩ ^ p ^ k = 1
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>P : Subgroup G<VAR>hP : IsPGroup p ↥P<VAR>c : Set (Subgroup G)<VAR>hc1 : c ⊆ {Q | IsPGroup p ↥Q}<VAR>hc2 : IsChain (fun x x_1 => x ≤ x_1) c<VAR>Q : Subgroup G<VAR>hQ : Q ∈ c<VAR>x✝ : ↥{ carrier := ⋃ R, ↑↑R, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }<VAR>g : G<VAR>S : ↑c<VAR>hg : g ∈ (fun R => ↑↑R) S<VAR>k : ℕ<VAR>hk : ⟨g, hg⟩ ^ p ^ k = 1<GOAL>⟨g, ⋯⟩ ^ p ^ k = 1
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)<VAR>i : ι<VAR>x : A<VAR>hx : x ∈ ⨅ i, f i<GOAL>↑(((decompose 𝒜) x) i) ∈ ⨅ i, f i
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)<VAR>i : ι<VAR>x : A<VAR>hx : ∀ (i : κ), x ∈ f i<GOAL>∀ (i_1 : κ), ↑(((decompose 𝒜) x) i) ∈ f i_1
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Function.Surjective ⇑g<VAR>z : P ⊗[R] Q<GOAL>∃ a, (rTensor Q g) a = z
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>h₀ : t ∈ 𝓝 0<VAR>hc : Convex ℝ t<VAR>x : E<VAR>hx : x ∈ interior s<GOAL>gaugeRescale s t x ∈ interior t
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>h₀ : t ∈ 𝓝 0<VAR>hc : Convex ℝ t<VAR>x : E<VAR>hx : x ∈ interior s<GOAL>gauge t (gaugeRescale s t x) < 1
<VAR>x y : ℂ<GOAL>cexp x = cexp y ↔ ∃ n, x = y + ↑n * (2 * ↑π * I)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X : C<VAR>inst✝ : Simple X<GOAL>¬IsZero X
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<GOAL>eLpNorm' f q μ ≤ eLpNormEssSup f μ * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<VAR>h_le : ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ<GOAL>eLpNorm' f q μ ≤ eLpNormEssSup f μ * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<VAR>h_le : ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ<GOAL>(∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) ≤ eLpNormEssSup f μ ^ 1 * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<VAR>h_le : ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ<GOAL>(∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) ≤ eLpNormEssSup f μ ^ (q * q⁻¹) * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<VAR>h_le : ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ<GOAL>(∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ q⁻¹ ≤ (eLpNormEssSup f μ ^ q * μ Set.univ) ^ q⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<VAR>h_le : ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ ≤ eLpNormEssSup f μ ^ q * μ Set.univ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<GOAL>σ 𝕜 ((cfcₙAux ⋯ a ha) f) = Set.range ⇑f
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<GOAL>σ 𝕜 (↑(cfcHom ⋯) (((↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))).comp ContinuousMapZero.toContinuousMapHom) f)) = Set.range ⇑f
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<GOAL>σ 𝕜 ((cfcHom ⋯) ((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f))) = Set.range ⇑f
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<GOAL>Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f)) = Set.range ⇑f
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I J : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>I' J' : Ideal R<VAR>hI : ↑I = ↑I'<VAR>hJ : ↑J = ↑J'<GOAL>mk I = mk J ↔ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I J : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>I' J' : Ideal R<VAR>hI : ↑I = ↑I'<VAR>hJ : ↑J = ↑J'<GOAL>(∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J) ↔ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Finite ι<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : ContinuousSMul R M<VAR>f : (ι → R) →ₗ[R] M<GOAL>Continuous ⇑f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Finite ι<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : ContinuousSMul R M<VAR>f : (ι → R) →ₗ[R] M<VAR>val✝ : Fintype ι<GOAL>Continuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Topology.IsLowerSet α<VAR>s : Set α<GOAL>IsClosed s ↔ IsUpperSet s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot
<VAR>d : ℤ<VAR>a : Solution₁ d<GOAL>d * a.y ^ 2 = a.x ^ 2 - 1
<VAR>d : ℤ<VAR>a : Solution₁ d<GOAL>d * a.y ^ 2 = a.x ^ 2 - (a.x ^ 2 - d * a.y ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>ho : ∀ a < o, succ a < o<GOAL>∀ a < type LT.lt, succ a < type LT.lt
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<VAR>f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s<GOAL>map m (ofComapInfPrincipal h) = g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<VAR>f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s<VAR>this : f.NeBot<GOAL>map m (ofComapInfPrincipal h) = g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<VAR>f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s<VAR>this : f.NeBot<GOAL>↑(map m (ofComapInfPrincipal h)) ≤ ↑g
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x : 𝕎 R<GOAL>x.verschiebungFun.coeff 0 = 0
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w✝ : InfinitePlace K<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>w w' : InfinitePlace K<VAR>h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)<GOAL>∃ σ, σ • w = w'
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w✝ : InfinitePlace K<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>w w' : InfinitePlace K<VAR>h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K) ∨ ComplexEmbedding.conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)<GOAL>∃ σ, σ • w = w'
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset E<VAR>x : E<GOAL>x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset E<VAR>x : E<GOAL>(∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>s : Finset E<VAR>x : E<VAR>w : E → R<VAR>hw : ∑ y ∈ s, w y = 1<GOAL>s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ φ, (∀ (x : α), ↑(↑φ x) ≤ f x) ∧ ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ φ, (∀ (x : α), ↑(↑φ x) ≤ f x) ∧ ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ < (⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ) + ε<GOAL>∃ φ, (∀ (x : α), ↑(↑φ x) ≤ f x) ∧ ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ < ⨆ i ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ f x, (SimpleFunc.map ofNNReal i).lintegral μ + ε<GOAL>∃ φ, (∀ (x : α), ↑(↑φ x) ≤ f x) ∧ ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this : ∃ i, ∃ (_ : i ∈ fun φ => ∀ (x : α), ↑(↑φ x) ≤ f x), ∃ b < (SimpleFunc.map ofNNReal i).lintegral μ + ε, ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b<GOAL>∃ φ, (∀ (x : α), ↑(↑φ x) ≤ f x) ∧ ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε