ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹¹ : CommSemiring R✝<VAR>inst✝¹⁰ : NonUnitalRing A✝<VAR>inst✝⁹ : Module R✝ A✝<VAR>inst✝⁸ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁷ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : Semifield R<VAR>inst✝⁵ : Semifield S<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h : SpectrumRestricts a f<VAR>s : S<VAR>hs : s ∈ spectrum S a<GOAL>f s ∈ spectrum R a ∧ (algebraMap R S) (f s) = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a x✝ : α<GOAL>a < x✝ ↔ ¬x✝ ≤ a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Group M<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>c : Con M<VAR>w x y z : M<VAR>h1 : c w x<VAR>h2 : c y z<GOAL>c (w / y) (x / z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set (Set α)<GOAL>⋃₀ s = ⋃ i, ↑i
<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>p : ℝ<VAR>hp : 0 ≤ p<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>eLpNorm' f p (c • μ) = c ^ (1 / p) * eLpNorm' f p μ
<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>p : ℝ<VAR>hp : 0 ≤ p<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>0 ≤ 1 / p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝³ : One M<VAR>inst✝² : One N<VAR>inst✝¹ : One P<VAR>inst✝ : DecidableEq α<VAR>f : α → M<VAR>x : α<VAR>y : M<VAR>hy : y ≠ 1<VAR>a : α<GOAL>a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)
<VAR>α : Type u_1<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : (↑t).Nonempty<GOAL>∃ u, Nat.card ↑u * Nat.card ↑↑t ≤ Nat.card ↑(↑s * ↑t) ∧ ↑s ⊆ u * ↑t / ↑t ∧ u.Finite
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : CommGroup α<VAR>v : Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : CommGroup α<VAR>v : Vector α n<VAR>i : Fin n<VAR>a : α<GOAL>(v.toList.prod * if hn : ↑i < v.toList.length then (v.toList.get ⟨↑i, hn⟩)⁻¹ * a else 1) = v.toList.prod * (v.get i)⁻¹ * a
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F : C × D ⥤ E<VAR>fst✝² : C<VAR>snd✝² : D<VAR>fst✝¹ : C<VAR>snd✝¹ : D<VAR>fst✝ : (fst✝², snd✝²).1 ⟶ (fst✝¹, snd✝¹).1<VAR>snd✝ : (fst✝², snd✝²).2 ⟶ (fst✝¹, snd✝¹).2<GOAL>(F.map (fst✝, 𝟙 snd✝²) ≫ F.map (𝟙 fst✝¹, snd✝)) ≫ 𝟙 (F.obj (fst✝¹, snd✝¹)) = 𝟙 (F.obj (fst✝², snd✝²)) ≫ F.map (fst✝, snd✝)
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F : C × D ⥤ E<VAR>fst✝² : C<VAR>snd✝² : D<VAR>fst✝¹ : C<VAR>snd✝¹ : D<VAR>fst✝ : (fst✝², snd✝²).1 ⟶ (fst✝¹, snd✝¹).1<VAR>snd✝ : (fst✝², snd✝²).2 ⟶ (fst✝¹, snd✝¹).2<GOAL>F.map ((fst✝, 𝟙 snd✝²) ≫ (𝟙 fst✝¹, snd✝)) ≫ 𝟙 (F.obj (fst✝¹, snd✝¹)) = 𝟙 (F.obj (fst✝², snd✝²)) ≫ F.map (fst✝, snd✝)
<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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>h : ↑f =ᶠ[ae μ] ↑g<GOAL>setToSimpleFunc T f = setToSimpleFunc T g
<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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>h : ↑f =ᶠ[ae μ] ↑g<GOAL>Pairwise fun x y => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>h : ↑f =ᶠ[ae μ] ↑g<VAR>x y : E<VAR>hxy : x ≠ y<GOAL>μ (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>h : μ {a | ¬↑f a = ↑g a} = 0<VAR>x y : E<VAR>hxy : x ≠ y<GOAL>μ (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>h : μ {a | ¬↑f a = ↑g a} = 0<VAR>x y : E<VAR>hxy : x ≠ y<VAR>z : α<GOAL>z ∈ ↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y} → z ∈ {a | ¬↑f a = ↑g a}
<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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>h : μ {a | ¬↑f a = ↑g a} = 0<VAR>x y : E<VAR>hxy : x ≠ y<VAR>z : α<GOAL>↑f z = x ∧ ↑g z = y → ¬↑f z = ↑g z
<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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>h✝ : μ {a | ¬↑f a = ↑g a} = 0<VAR>x y : E<VAR>hxy : x ≠ y<VAR>z : α<VAR>h : ↑f z = x ∧ ↑g z = y<GOAL>¬↑f z = ↑g z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>a : α<GOAL>p a ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>a b : α<GOAL>(if b = a then p a else 0) ≤ p b
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'<VAR>x : S<VAR>s : Finset S'<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<GOAL>∃ m, m • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'<VAR>x : S<VAR>s : Finset S'<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>a : R<VAR>ha : a ∈ ↑M<VAR>e : ⟨(algebraMap R S) a, ⋯⟩ • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)<GOAL>∃ m, m • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'<VAR>x : S<VAR>s : Finset S'<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>a : R<VAR>ha : a ∈ ↑M<VAR>e : ⟨(algebraMap R S) a, ⋯⟩ • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)<GOAL>⟨a, ha⟩ • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
<VAR>α : Type u<VAR>i✝ : Nat<VAR>a b : Array α<VAR>i j : Nat<VAR>h : a.size ≤ i<GOAL>(a ++ b).extract i j = b.extract (i - a.size) (j - a.size)
<VAR>α : Type u<VAR>i✝ : Nat<VAR>a b : Array α<VAR>i j : Nat<VAR>h : a.size ≤ i<GOAL>((a ++ b).extract i j).size = (b.extract (i - a.size) (j - a.size)).size
<VAR>α : Type u<VAR>i✝ : Nat<VAR>a b : Array α<VAR>i j : Nat<VAR>h : a.size ≤ i<GOAL>∀ (i_1 : Nat) (hi₁ : i_1 < ((a ++ b).extract i j).size) (hi₂ : i_1 < (b.extract (i - a.size) (j - a.size)).size), ((a ++ b).extract i j)[i_1] = (b.extract (i - a.size) (j - a.size))[i_1]
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<GOAL>(-a).val = (-a).val % n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<GOAL>(-a).val + a.val ≡ n - a.val + a.val [MOD n]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<GOAL>(p.scaleRoots s).natDegree = p.natDegree
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>f : (i : ι) → G i →* K<VAR>k : H →* K<VAR>hf : ∀ (i : ι), (f i).comp (φ i) = k<VAR>i : ι<VAR>g : G i<GOAL>((con φ).lift (Coprod.lift (CoprodI.lift f) k) ⋯) (((con φ).mk'.comp (inl.comp CoprodI.of)) g) = (f i) g
<VAR>k : Type u<VAR>inst✝ : Field k<GOAL>spanEval k ≠ ⊤
<VAR>k : Type u<VAR>inst✝ : Field k<GOAL>¬∃ l ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ, (Finsupp.total (MonicIrreducible k) (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) (evalXSelf k)) l = 1
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k<VAR>left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ<VAR>hv : (toSplittingField k v.support) ((Finsupp.total (MonicIrreducible k) (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) (evalXSelf k)) v) = (toSplittingField k v.support) 1<GOAL>False
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k<VAR>left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ<VAR>hv : 0 = 1<GOAL>False
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k<VAR>left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ<VAR>hv : ∑ x ∈ v.support, (toSplittingField k v.support) (v x • evalXSelf k x) = 1<GOAL>∀ x ∈ v.support, (toSplittingField k v.support) (v x • evalXSelf k x) = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k<VAR>left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ<VAR>hv : ∑ x ∈ v.support, (toSplittingField k v.support) (v x • evalXSelf k x) = 1<VAR>j : MonicIrreducible k<VAR>hj : j ∈ v.support<GOAL>(toSplittingField k v.support) (v j • evalXSelf k j) = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>x : S₁<GOAL>(optionEquivLeft R S₁) (X (Option.some x)) = Polynomial.C (X x)
<VAR>p a b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>dvd : p ∣ b<GOAL>padicValNat p (b / p) = padicValNat p b - 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : TaggedPrepartition I<VAR>πi : (J : Box ι) → Prepartition J<VAR>hπi : ∀ J ∈ π, (πi J).IsPartition<GOAL>integralSum f vol (π.biUnionPrepartition πi) = integralSum f vol π
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>I J✝ : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : TaggedPrepartition I<VAR>πi : (J : Box ι) → Prepartition J<VAR>hπi : ∀ J ∈ π, (πi J).IsPartition<VAR>J : Box ι<VAR>hJ : J ∈ π.boxes<GOAL>∑ J' ∈ (πi J).boxes, (vol J') (f ((π.biUnionPrepartition πi).tag J')) = (vol J) (f (π.tag J))
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>inst✝ : HasKernels V<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>inst✝ : HasKernels V<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>kernelSubobject (C.d i j ≫ (C.xNextIso r).inv) = kernelSubobject (C.d i j)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<GOAL>(isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>x : (Opens ↑↑Y)ᵒᵖ<GOAL>(((isoRestrict f).hom ≫ Y.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app x = f.c.app x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>x : (Opens ↑↑Y)ᵒᵖ<GOAL>(((isoRestrict f).hom ≫ Y.ofRestrict ⋯).c ≫ 𝟙 ((Opens.map ((isoRestrict f).hom ≫ Y.ofRestrict ⋯).base).op ⋙ X.presheaf)).app x = f.c.app x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>x : (Opens ↑↑Y)ᵒᵖ<GOAL>f.c.app x ≫ X.presheaf.map ((Opens.map f.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ (eqToIso ⋯).hom) = f.c.app x
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>L : F<VAR>r ε δ : ℝ<VAR>h : ε ≤ δ<VAR>x r' : ℝ<VAR>r'r : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<GOAL>x ∈ A f L r δ
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>L : F<VAR>r ε δ : ℝ<VAR>h : ε ≤ δ<VAR>x r' : ℝ<VAR>r'r : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<VAR>y : ℝ<VAR>hy : y ∈ Icc x (x + r')<VAR>z : ℝ<VAR>hz : z ∈ Icc x (x + r')<GOAL>0 ≤ r
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>hd : Disjoint s1 s2<GOAL>Disjoint ↑(affineSpan k (p '' s1)) ↑(affineSpan k (p '' s2))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>hd : Disjoint s1 s2<VAR>p0 : P<VAR>hp0s1 : p0 ∈ ↑(affineSpan k (p '' s1))<VAR>hp0s2 : p0 ∈ ↑(affineSpan k (p '' s2))<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>hd : Disjoint s1 s2<VAR>p0 : P<VAR>hp0s1 : p0 ∈ ↑(affineSpan k (p '' s1))<VAR>hp0s2 : p0 ∈ ↑(affineSpan k (p '' s2))<VAR>i : ι<VAR>hi : i ∈ s1 ∩ s2<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<GOAL>hA.sqrt * hA.sqrt = A
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<GOAL>lift.{v, v'} (Module.rank R ↥(LinearMap.range f)) ≤ lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<GOAL>lift.{v, v'} (⨆ ι, #↑↑ι) ≤ lift.{v', v} (⨆ ι, #↑↑ι)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<GOAL>⨆ i, lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<GOAL>∀ (i : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }), lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<VAR>s : Set ↥(LinearMap.range f)<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} (⨆ ι, #↑↑ι)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<VAR>s : Set ↥(LinearMap.range f)<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>lift.{v, v'} #↑↑⟨s, li⟩ ≤ ?h.mk.b
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<VAR>s : Set ↥(LinearMap.range f)<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>?h.mk.b ≤ lift.{v', v} (⨆ ι, #↑↑ι)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<VAR>s : Set ↥(LinearMap.range f)<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>Cardinal.{max v' v}
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>W.Equation P ↔ P 1 ^ 2 * P 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 2 = P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 + W.a₄ * P 0 * P 2 ^ 2 + W.a₆ * P 2 ^ 3
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a ≤ c / b ↔ a * b ≤ c