ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>Set.range ⇑U.ι.val.base = ↑U
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>Function.Surjective (⇑(↑U).isoSpec.inv.val.base ∘ ⇑(Spec.map (X.presheaf.map (eqToHom ⋯).op)).val.base)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>Epi ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).val.base ≫ (↑U).isoSpec.inv.val.base)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<GOAL>(expand R (p ^ Nat.zero)) f = (⇑(expand R p))^[Nat.zero] f
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<VAR>n : ℕ<VAR>ih : (expand R (p ^ n)) f = (⇑(expand R p))^[n] f<GOAL>(expand R (p ^ n.succ)) f = (⇑(expand R p))^[n.succ] f
<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>s : Set G<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<GOAL>μ' s = μ'.haarScalarFactor μ • μ 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>s : Set G<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<GOAL>μ' s ≤ μ'.haarScalarFactor μ • μ 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>s : Set G<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<GOAL>μ'.haarScalarFactor μ • μ s ≤ μ' s
<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<GOAL>(weightSpace M 0).normalizer = weightSpace M 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<GOAL>(weightSpace M 0).normalizer ≤ weightSpace M 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>m : M<VAR>hm : m ∈ (weightSpace M 0).normalizer<GOAL>m ∈ weightSpace M 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>m : M<VAR>hm : ∀ (x : L), ⁅x, m⁆ ∈ weightSpace M 0<GOAL>m ∈ weightSpace M 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>m : M<VAR>hm : ∀ (x x_1 : L), ∃ k, ((toEnd R L M) x_1 ^ k) ⁅x, m⁆ = 0<GOAL>∀ (x : L), ∃ k, ((toEnd R L M) x ^ k) m = 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>m : M<VAR>hm : ∀ (x x_1 : L), ∃ k, ((toEnd R L M) x_1 ^ k) ⁅x, m⁆ = 0<VAR>y : L<VAR>k : ℕ<VAR>hk : ((toEnd R L M) y ^ k) ⁅y, m⁆ = 0<GOAL>∃ k, ((toEnd R L M) y ^ k) m = 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>m : M<VAR>hm : ∀ (x x_1 : L), ∃ k, ((toEnd R L M) x_1 ^ k) ⁅x, m⁆ = 0<VAR>y : L<VAR>k : ℕ<VAR>hk : ((toEnd R L M) y ^ k) ⁅y, m⁆ = 0<GOAL>((toEnd R L M) y ^ (k + 1)) m = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>a✝ b✝ c✝ d a b c : α<VAR>hc : c ≠ 0<GOAL>b + a / c = (b * c + a) / c
<VAR>a b : ℕ<GOAL>φ (a.gcd b) * φ (a * b) = φ a * φ b * a.gcd b
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>φ (a.gcd b) * φ (a * b) = φ a * φ b * a.gcd b
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>((a.gcd b / ∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ((a * b / ∏ p ∈ (a * b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, (p - 1)) = ((a / ∏ p ∈ a.primeFactors, p) * ∏ p ∈ a.primeFactors, (p - 1)) * ((b / ∏ p ∈ b.primeFactors, p) * ∏ p ∈ b.primeFactors, (p - 1)) * a.gcd b
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>∏ p ∈ a.primeFactors, p ∣ a
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>∏ p ∈ b.primeFactors, p ∣ b
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>∏ p ∈ (a * b).primeFactors, p ∣ a * b
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) * ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) = a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) * ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) * a.gcd b
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) * ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) = a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) * ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) * a.gcd b
<VAR>a b : ℕ<VAR>shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)<GOAL>(∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p ∣ a * b
<VAR>p✝ p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>h : multiplicity.Finite p n<GOAL>p.maxPowDiv n = (multiplicity p n).get h
<VAR>p✝ p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>h : multiplicity.Finite p n<GOAL>multiplicity p n = ↑(p.maxPowDiv n)
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<VAR>α : 𝓞 K<VAR>i : K →+* ℂ<GOAL>((basisMatrix K)ᵀ⁻¹ *ᵥ fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i = ↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x : M'<VAR>m : M<VAR>s : ↥S<VAR>eq1 : (m, s).2 • x = f (m, s).1<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk m s) = x
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>m : α → EReal<VAR>f : Filter α<GOAL>(∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Iio ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>l : List (Perm α)<VAR>h : f ∈ l<VAR>hl : List.Pairwise Disjoint l<VAR>x : α<VAR>hx : x ∈ f.support<GOAL>x ∈ l.prod.support
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝² : MulZeroClass α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : MulPosMono α<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a * b ≤ 0
<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 : Set α → E →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ f.range, ‖T (↑f ⁻¹' {x})‖ * ‖x‖ ≤ ∑ x ∈ f.range, C * (μ (↑f ⁻¹' {x})).toReal * ‖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 : Set α → E →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>b : E<VAR>hb : b ∈ f.range<GOAL>‖T (↑f ⁻¹' {b})‖ * ‖b‖ ≤ C * (μ (↑f ⁻¹' {b})).toReal * ‖b‖
<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 : Set α → E →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hb : 0 ∈ f.range<GOAL>‖T (↑f ⁻¹' {0})‖ * ‖0‖ ≤ C * (μ (↑f ⁻¹' {0})).toReal * ‖0‖
<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 : Set α → E →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>b : E<VAR>hb✝ : b ∈ f.range<VAR>hb : b ≠ 0<GOAL>‖T (↑f ⁻¹' {b})‖ * ‖b‖ ≤ C * (μ (↑f ⁻¹' {b})).toReal * ‖b‖
<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 : Set α → E →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>b : E<VAR>hb✝ : b ∈ f.range<VAR>hb : b ≠ 0<GOAL>‖T (↑f ⁻¹' {b})‖ ≤ C * (μ (↑f ⁻¹' {b})).toReal
<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 : Set α → E →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ f.range, C * (μ (↑f ⁻¹' {x})).toReal * ‖x‖ ≤ C * ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal * ‖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 : Set α → E →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ f.range, C * (μ (↑f ⁻¹' {x})).toReal * ‖x‖ ≤ ∑ x ∈ f.range, C * (μ (↑f ⁻¹' {x})).toReal * ‖x‖
<VAR>n : ℕ<VAR>F✝ : TypeVec.{u} (n + 1) → Type u<VAR>q✝ : MvQPF F✝<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : Cofix F α<VAR>R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x<GOAL>Quot.mk Mcongr x.repr = x
<VAR>n : ℕ<VAR>F✝ : TypeVec.{u} (n + 1) → Type u<VAR>q✝ : MvQPF F✝<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : Cofix F α<VAR>R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x<GOAL>∀ (x y : Cofix F α), R x y → LiftR' (α.RelLast' R) x.dest y.dest
<VAR>n : ℕ<VAR>F✝ : TypeVec.{u} (n + 1) → Type u<VAR>q✝ : MvQPF F✝<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x<VAR>a✝ : (P F).M α<GOAL>LiftR' (α.RelLast' R) ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (repr (Quot.mk Mcongr a✝)))) (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝))
<VAR>n : ℕ<VAR>F✝ : TypeVec.{u} (n + 1) → Type u<VAR>q✝ : MvQPF F✝<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x<VAR>a✝ : (P F).M α<GOAL>LiftR' (α.RelLast' R) ((TypeVec.id ::: Quot.mk Mcongr) <$$> (TypeVec.id ::: M.corec (P F) fun x => MvQPF.repr x.dest) <$$> dest (Quot.mk Mcongr a✝)) ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
<VAR>n : ℕ<VAR>F✝ : TypeVec.{u} (n + 1) → Type u<VAR>q✝ : MvQPF F✝<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x<VAR>a✝ : (P F).M α<GOAL>LiftR' (α.RelLast' R) ((TypeVec.id ::: Quot.mk Mcongr) <$$> (TypeVec.id ::: M.corec (P F) fun x => MvQPF.repr (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ x)) <$$> Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (Quot.mk Mcongr a✝)) ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
<VAR>n : ℕ<VAR>F✝ : TypeVec.{u} (n + 1) → Type u<VAR>q✝ : MvQPF F✝<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x<VAR>a✝ : (P F).M α<GOAL>LiftR' (α.RelLast' R) ((TypeVec.id ::: (Quot.mk Mcongr ∘ M.corec (P F) fun x => MvQPF.repr (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ x)) ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝)) ((TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a✝))
<VAR>n : ℕ<VAR>F✝ : TypeVec.{u} (n + 1) → Type u<VAR>q✝ : MvQPF F✝<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x<VAR>a✝ : (P F).M α<GOAL>∀ (x : (P F).M α), R (((Quot.mk Mcongr ∘ M.corec (P F) fun x => MvQPF.repr (Quot.lift (fun x => (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ x)) ∘ Quot.mk Mcongr) x) (Quot.mk Mcongr x)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MulAction G X<VAR>inst✝⁸ : MulAction G Y<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : TopologicalSpace Z<VAR>H : Type u_5<VAR>inst✝³ : Group H<VAR>inst✝² : MulAction H X<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : ProperSMul G X<VAR>f : H →* G<VAR>f_clemb : ClosedEmbedding ⇑f<VAR>f_compat : ∀ (h : H) (x : X), f h • x = h • x<GOAL>IsProperMap fun gx => (gx.1 • gx.2, gx.2)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MulAction G X<VAR>inst✝⁸ : MulAction G Y<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : TopologicalSpace Z<VAR>H : Type u_5<VAR>inst✝³ : Group H<VAR>inst✝² : MulAction H X<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : ProperSMul G X<VAR>f : H →* G<VAR>f_clemb : ClosedEmbedding ⇑f<VAR>f_compat : ∀ (h : H) (x : X), f h • x = h • x<VAR>this : IsProperMap ⇑f<GOAL>IsProperMap fun gx => (gx.1 • gx.2, gx.2)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MulAction G X<VAR>inst✝⁸ : MulAction G Y<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : TopologicalSpace Z<VAR>H : Type u_5<VAR>inst✝³ : Group H<VAR>inst✝² : MulAction H X<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : ProperSMul G X<VAR>f : H →* G<VAR>f_clemb : ClosedEmbedding ⇑f<VAR>f_compat : ∀ (h : H) (x : X), f h • x = h • x<VAR>this : IsProperMap ⇑f<VAR>h : IsProperMap (Prod.map ⇑f fun x => x)<GOAL>IsProperMap fun gx => (gx.1 • gx.2, gx.2)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MulAction G X<VAR>inst✝⁸ : MulAction G Y<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : TopologicalSpace Z<VAR>H : Type u_5<VAR>inst✝³ : Group H<VAR>inst✝² : MulAction H X<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : ProperSMul G X<VAR>f : H →* G<VAR>f_clemb : ClosedEmbedding ⇑f<VAR>f_compat : ∀ (h : H) (x : X), f h • x = h • x<VAR>this✝ : IsProperMap ⇑f<VAR>h : IsProperMap (Prod.map ⇑f fun x => x)<VAR>this : (fun hx => (hx.1 • hx.2, hx.2)) = fun hx => (f hx.1 • hx.2, hx.2)<GOAL>IsProperMap fun hx => (f hx.1 • hx.2, hx.2)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CommMonoidWithZero α<VAR>s : Multiset α<VAR>h : 0 ∈ s<GOAL>s.prod = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CommMonoidWithZero α<VAR>s : Multiset α<VAR>h : 0 ∈ s<VAR>s' : Multiset α<VAR>hs' : s = 0 ::ₘ s'<GOAL>s.prod = 0
<VAR>n : Type u_1<VAR>inst✝⁹ : Fintype n<VAR>R : Type u_2<VAR>M✝ : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M✝<VAR>inst✝⁶ : Module R M✝<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Nontrivial A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>M : Matrix n n A<GOAL>(∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0
<VAR>n : Type u_1<VAR>inst✝⁹ : Fintype n<VAR>R : Type u_2<VAR>M✝ : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M✝<VAR>inst✝⁶ : Module R M✝<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Nontrivial A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>M : Matrix n n A<VAR>this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ ((algebraMap A K).mapMatrix M).det = 0<GOAL>(∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0
<VAR>n : Type u_1<VAR>inst✝⁹ : Fintype n<VAR>R : Type u_2<VAR>M✝ : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M✝<VAR>inst✝⁶ : Module R M✝<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Nontrivial A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>M : Matrix n n A<VAR>this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0<GOAL>(∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0
<VAR>n : Type u_1<VAR>inst✝⁹ : Fintype n<VAR>R : Type u_2<VAR>M✝ : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M✝<VAR>inst✝⁶ : Module R M✝<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Nontrivial A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>M : Matrix n n A<VAR>this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0<GOAL>(∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>b : α<GOAL>toIcoMod hp 0 b = Int.fract (b / p) * p
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)<VAR>x : Presieve.FamilyOfElements (presheafHom F G) S.arrows<VAR>hx : x.Compatible<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)<VAR>x : Presieve.FamilyOfElements (presheafHom F G) S.arrows<VAR>hx : x.Compatible<GOAL>∃ x_1, x.IsAmalgamation x_1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)<VAR>x : Presieve.FamilyOfElements (presheafHom F G) S.arrows<VAR>hx : x.Compatible<GOAL>∀ (y₁ y₂ : (presheafHom F G).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s : Set X<GOAL>Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s : Set X<VAR>h : RegularSpace X ↔ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s<GOAL>Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>l[indexOf a l]? = some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : α →₀ ℕ<GOAL>Multiset.card (toMultiset f) = f.sum fun x => id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α<VAR>s t : Finset α<VAR>f : α → β<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidablePred fun y => y ∈ Set.range f<VAR>inst✝ : DecidableEq β<VAR>this : DecidablePred fun y => ∃ x, f x = y := inst✝¹<GOAL>filter (fun y => y ∈ Set.range f) univ = image f univ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>p q : R[X]<GOAL>eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>p.comp 0 = C (eval 0 p)