ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R' →+* R<VAR>j : S →+* S'<VAR>hi : Injective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'<GOAL>lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')
<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>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R' →+* R<VAR>j : S →+* S'<VAR>hi : Injective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'<VAR>r : R'<VAR>x✝ : S<GOAL>↑j (i r • x✝) = r • ↑j x✝
<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>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R' →+* R<VAR>j : S →+* S'<VAR>hi : Injective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'<VAR>r : R'<VAR>x✝ : S<VAR>this : ((j.comp (algebraMap R S)).comp i) r = (algebraMap R' S') r<GOAL>↑j (i r • x✝) = r • ↑j x✝
<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>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R' →+* R<VAR>j : S →+* S'<VAR>hi : Injective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'<VAR>r : R'<VAR>x✝ : S<VAR>this : j ((algebraMap R S) (i r)) = (algebraMap R' S') r<GOAL>↑j (i r • x✝) = r • ↑j x✝
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<GOAL>(trinomial k m n u v w).trailingCoeff = u
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<GOAL>∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>this : p.IsPrime<GOAL>∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>this : p.IsPrime<VAR>f' : R →+* S ⧸ I := (Quotient.mk I).comp f<GOAL>∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>this : p.IsPrime<VAR>f' : R →+* S ⧸ I := (Quotient.mk I).comp f<VAR>e : RingHom.ker f' = comap f I<GOAL>∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>this✝ : p.IsPrime<VAR>f' : R →+* S ⧸ I := (Quotient.mk I).comp f<VAR>e : RingHom.ker f' = comap f I<VAR>this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p<GOAL>∃ p', p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>this✝ : p.IsPrime<VAR>f' : R →+* S ⧸ I := (Quotient.mk I).comp f<VAR>e : RingHom.ker f' = comap f I<VAR>this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p<GOAL>map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>this✝ : p.IsPrime<VAR>f' : R →+* S ⧸ I := (Quotient.mk I).comp f<VAR>e : RingHom.ker f' = comap f I<VAR>this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p<GOAL>(map (Quotient.mk (RingHom.ker f')) p).IsPrime
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>H : p ∈ (comap f I).minimalPrimes<VAR>this✝ : p.IsPrime<VAR>f' : R →+* S ⧸ I := (Quotient.mk I).comp f<VAR>e : RingHom.ker f' = comap f I<VAR>this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p<GOAL>∀ ⦃b : Ideal (R ⧸ RingHom.ker f')⦄, b ∈ {p | p.IsPrime ∧ ⊥ ≤ p} → (fun x x_1 => x ≤ x_1) b (map (Quotient.mk (RingHom.ker f')) p) → (fun x x_1 => x ≤ x_1) (map (Quotient.mk (RingHom.ker f')) p) b
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x : β<GOAL>p.c x ∈ p.iUnionUpTo p.lastStep
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x : β<VAR>A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep<GOAL>p.c x ∈ p.iUnionUpTo p.lastStep
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x : β<VAR>A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep<VAR>h : ¬p.c x ∈ p.iUnionUpTo p.lastStep<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x : β<VAR>A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep<VAR>h : ¬p.c x ∈ p.iUnionUpTo p.lastStep<VAR>H : p.τ * p.r x < p.R p.lastStep<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x : β<VAR>A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep<VAR>h : ¬p.c x ∈ p.iUnionUpTo p.lastStep<VAR>H : p.τ * p.r x < p.R p.lastStep<VAR>Rpos : 0 < p.R p.lastStep<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x : β<VAR>A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep<VAR>h : ¬p.c x ∈ p.iUnionUpTo p.lastStep<VAR>H : p.τ * p.r x < p.R p.lastStep<VAR>Rpos : 0 < p.R p.lastStep<VAR>B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>x : α<VAR>n k : ℕ<VAR>hk' : n + k < l.length<GOAL>n + k + 1 < (insertNth n x l).length
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : DivisionSemiring α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>inst✝ : T2Space α<VAR>hf : ¬Summable f<VAR>ha : ¬a = 0<GOAL>∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : Integrable f μ<GOAL>0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>D : ι → ℝ<VAR>h : (Matrix.diagonal D).det ≠ 0<GOAL>ofReal |(Matrix.diagonal D).det| • Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>D : ι → ℝ<VAR>h : (Matrix.diagonal D).det ≠ 0<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>(ofReal |(Matrix.diagonal D).det| • Measure.map (⇑(toLin' (Matrix.diagonal D))) volume) (univ.pi s) = ∏ i : ι, volume (s i)
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>D : ι → ℝ<VAR>h : (Matrix.diagonal D).det ≠ 0<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>ofReal |∏ i : ι, D i| * (Measure.map (⇑(toLin' (Matrix.diagonal D))) volume) (univ.pi s) = ∏ x : ι, volume (s x)
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>D : ι → ℝ<VAR>h : (Matrix.diagonal D).det ≠ 0<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>ofReal |∏ i : ι, D i| * volume (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi s) = ∏ x : ι, volume (s x)
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>D : ι → ℝ<VAR>h : (Matrix.diagonal D).det ≠ 0<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>Measurable ⇑(toLin' (Matrix.diagonal D))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>D : ι → ℝ<VAR>h : (Matrix.diagonal D).det ≠ 0<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i => s i) = univ.pi fun i => (fun x => D i * x) ⁻¹' s i<VAR>B : ∀ (i : ι), ofReal |D i| * volume ((fun x => D i * x) ⁻¹' s i) = volume (s i)<GOAL>ofReal |∏ i : ι, D i| * volume (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi s) = ∏ x : ι, volume (s x)
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>D : ι → ℝ<VAR>h : (Matrix.diagonal D).det ≠ 0<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i => s i) = univ.pi fun i => (fun x => D i * x) ⁻¹' s i<VAR>B : ∀ (i : ι), ofReal |D i| * volume ((fun x => D i * x) ⁻¹' s i) = volume (s i)<GOAL>∏ x : ι, ofReal |D x| * volume ((fun x_1 => D x * x_1) ⁻¹' s x) = ∏ x : ι, volume (s x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : α → ℝ≥0<VAR>hf : Continuous f<VAR>x : α<GOAL>(μ.withDensity fun x => ↑(f x)).FiniteAtFilter (nhds x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : α → ℝ≥0<VAR>hf : Continuous f<VAR>x : α<VAR>U : Set α<VAR>hμU : μ U < ⊤<VAR>hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}<VAR>hUx : U ∈ nhds x<VAR>hUo : IsOpen U<GOAL>(μ.withDensity fun x => ↑(f x)).FiniteAtFilter (nhds x)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : α → ℝ≥0<VAR>hf : Continuous f<VAR>x : α<VAR>U : Set α<VAR>hμU : μ U < ⊤<VAR>hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}<VAR>hUx : U ∈ nhds x<VAR>hUo : IsOpen U<GOAL>(μ.withDensity fun x => ↑(f x)) U < ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : α → ℝ≥0<VAR>hf : Continuous f<VAR>x : α<VAR>U : Set α<VAR>hμU : μ U < ⊤<VAR>hUf : U ⊆ {x_1 | (fun a => f a ≤ f x + 1) x_1}<VAR>hUx : U ∈ nhds x<VAR>hUo : IsOpen U<GOAL>∫⁻ (a : α) in U, ↑(f a) ∂μ < ⊤
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : Finmap β<VAR>a₁ a₂ : AList β<GOAL>insert a b (⟦a₁⟧ ∪ ⟦a₂⟧) = insert a b ⟦a₁⟧ ∪ ⟦a₂⟧
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>s₁ s₂ : Set Ω<VAR>h : s₁ ⊆ s₂<GOAL>(↑μ s₁).toNNReal ≤ (↑μ s₂).toNNReal
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>s₁ s₂ : Set Ω<VAR>h : s₁ ⊆ s₂<VAR>key : ↑μ s₁ ≤ ↑μ s₂<GOAL>(↑μ s₁).toNNReal ≤ (↑μ s₂).toNNReal
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid A<VAR>s✝ t u : Set M<VAR>s : Submonoid M<VAR>x : M<GOAL>x ∈ ↑s * ↑s ↔ x ∈ ↑s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid A<VAR>s✝ t u : Set M<VAR>s : Submonoid M<VAR>x : M<GOAL>x ∈ ↑s * ↑s → x ∈ ↑s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid A<VAR>s✝ t u : Set M<VAR>s : Submonoid M<VAR>a : M<VAR>ha : a ∈ ↑s<VAR>b : M<VAR>hb : b ∈ ↑s<GOAL>(fun x x_1 => x * x_1) a b ∈ ↑s
<VAR>G : Type w<VAR>inst✝³ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝² : R1Space G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Set G<VAR>h1U : IsOpen U<VAR>h2U : U.Nonempty<GOAL>0 < μ.outerMeasure U
<VAR>G : Type w<VAR>inst✝³ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝² : R1Space G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Set G<VAR>h1U : IsOpen U<VAR>h2U : U.Nonempty<GOAL>μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := h1U }
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>y : ↥M<VAR>z₁ z₂ : S<GOAL>mk' S x y + z₁ = z₂ ↔ (algebraMap R S) x + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>f : ℕ → Set α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<GOAL>↑v (A ∪ B) = ↑v A + ↑v B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>f : ℕ → Set α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<GOAL>∀ (i : Bool), MeasurableSet (bif i then A else B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>f : ℕ → Set α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<GOAL>Pairwise (Disjoint on fun b => bif b then A else B)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>f : α → E<VAR>a : α<GOAL>∫ (a : α) in {a}, f a ∂μ = (μ {a}).toReal • f a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Zero M<VAR>inst✝ : CommMonoid N<VAR>v : α →₀ M<VAR>f : α ↪ β<VAR>g : β → M → N<GOAL>(embDomain f v).prod g = v.prod fun a b => g (f a) b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Zero M<VAR>inst✝ : CommMonoid N<VAR>v : α →₀ M<VAR>f : α ↪ β<VAR>g : β → M → N<GOAL>∏ x ∈ v.support, g (f x) ((embDomain f v) (f x)) = ∏ a ∈ v.support, g (f a) (v a)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(twoCocycles A)<VAR>g : G<GOAL>↑f (g, 1) = (A.ρ g) (↑f (1, 1))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(twoCocycles A)<VAR>g : G<VAR>this : ↑f (g * 1, 1) + ↑f (g, 1) = (A.ρ g) (↑f (1, 1)) + ↑f (g, 1 * 1)<GOAL>↑f (g, 1) = (A.ρ g) (↑f (1, 1))
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z✝ z : ℤ<GOAL>a - (z • p + a) = -z • p
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonAssocSemiring α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq m<VAR>x : α<VAR>v : m → α<VAR>x✝ : m<GOAL>((diagonal fun x_1 => x) *ᵥ v) x✝ = (x • v) x✝
<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>hs : IsOpen s<GOAL>frontier s = closure s \ s
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<VAR>x : A<VAR>hx : x ∈ adjoin R s<VAR>p : (x : A) → x ∈ adjoin R s → Prop<VAR>mem : ∀ (x : A) (h : x ∈ s), p x ⋯<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯<GOAL>p x hx
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<VAR>x : A<VAR>hx : x ∈ adjoin R s<VAR>p : (x : A) → x ∈ adjoin R s → Prop<VAR>mem : ∀ (x : A) (h : x ∈ s), p x ⋯<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯<GOAL>∀ (x y : ↥(adjoin R s)), (fun x => p ↑x ⋯) x → (fun x => p ↑x ⋯) y → (fun x => p ↑x ⋯) (x + y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<VAR>x : A<VAR>hx : x ∈ adjoin R s<VAR>p : (x : A) → x ∈ adjoin R s → Prop<VAR>mem : ∀ (x : A) (h : x ∈ s), p x ⋯<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯<GOAL>∀ (x y : ↥(adjoin R s)), (fun x => p ↑x ⋯) x → (fun x => p ↑x ⋯) y → (fun x => p ↑x ⋯) (x * y)
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>b c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<GOAL>b - c + c = b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hi : Irreducible p<VAR>x : R<VAR>hx : p.IsRoot x<VAR>g : R[X]<VAR>hg : p = (X - C x) * g<VAR>this : IsUnit (X - C x) ∨ IsUnit g<VAR>h : IsUnit (X - C x)<GOAL>p.degree = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hi : Irreducible p<VAR>x : R<VAR>hx : p.IsRoot x<VAR>g : R[X]<VAR>hg : p = (X - C x) * g<VAR>this : IsUnit (X - C x) ∨ IsUnit g<VAR>h : IsUnit (X - C x)<VAR>h₁ : (X - C x).degree = 1<GOAL>p.degree = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hi : Irreducible p<VAR>x : R<VAR>hx : p.IsRoot x<VAR>g : R[X]<VAR>hg : p = (X - C x) * g<VAR>this : IsUnit (X - C x) ∨ IsUnit g<VAR>h : IsUnit (X - C x)<VAR>h₁ : (X - C x).degree = 1<VAR>h₂ : (X - C x).degree = 0<GOAL>p.degree = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hi : Irreducible p<VAR>x : R<VAR>hx : p.IsRoot x<VAR>g : R[X]<VAR>hg : p = (X - C x) * g<VAR>this : IsUnit (X - C x) ∨ IsUnit g<VAR>hgu : IsUnit g<GOAL>p.degree = 1
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι✝ → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>ι : Type u_9<VAR>s : Set ι<VAR>f : ι → A<VAR>hs : AlgebraicIndependent R fun x => f ↑x<GOAL>AlgebraicIndependent R fun x => ↑x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n✝ : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>n : σ →₀ ℕ<GOAL>(coeff R n) (φ * 0) = (coeff R n) 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<GOAL>UniqueMul (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } A)) (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } B)) (op (op a0)) (op (op b0))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<GOAL>UniqueMul (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) A) (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) B) (op (op a0)) (op (op b0))