ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>S : Subalgebra R A<VAR>a : A<VAR>ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))<GOAL>star a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>S : Subalgebra R A<VAR>a : A<VAR>ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))<GOAL>a ∈ Algebra.adjoin R (star (↑(star S) ⊔ ↑S))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<GOAL>(inverse_of_rightInverse Q hfg hgh) ((rTensor Q g) y) = Submodule.Quotient.mk y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<GOAL>(inverse_of_rightInverse Q hfg✝ hgh ∘ₗ rTensor Q g) y = (range (rTensor Q f)).mkQ y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<GOAL>inverse_of_rightInverse Q hfg✝ hgh ∘ₗ rTensor Q g = (range (rTensor Q f)).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<GOAL>∀ (x : N) (y : Q), (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ rTensor Q g) (x ⊗ₜ[R] y) = (range (rTensor Q f)).mkQ (x ⊗ₜ[R] y)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<VAR>n : N<VAR>q : Q<GOAL>(inverse_of_rightInverse Q hfg✝ hgh ∘ₗ rTensor Q g) (n ⊗ₜ[R] q) = (range (rTensor Q f)).mkQ (n ⊗ₜ[R] q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<VAR>n : N<VAR>q : Q<GOAL>Submodule.Quotient.mk (h (g n) ⊗ₜ[R] q) = Submodule.Quotient.mk (n ⊗ₜ[R] q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<VAR>n : N<VAR>q : Q<GOAL>(h (g n) - n) ⊗ₜ[R] q ∈ range (rTensor Q f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<VAR>n : N<VAR>q : Q<GOAL>h (g n) - n ∈ range f
<VAR>r p : ℝ≥0<VAR>h : r ≠ 0<GOAL>r⁻¹ ≤ p ↔ 1 ≤ r * p
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>n : ℕ<VAR>hx : orderOf x ≠ 0<VAR>hn : n ∣ orderOf x<GOAL>orderOf (x ^ (orderOf x / n)) = n
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>n : ℕ<VAR>hx : orderOf x ≠ 0<VAR>hn : n ∣ orderOf x<GOAL>orderOf x / n ≠ 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>n : ℕ<VAR>hx : orderOf x / n * n ≠ 0<VAR>hn : n ∣ orderOf x<GOAL>orderOf x / n ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>B : Set α<VAR>hB : M.Base B<VAR>f : α → β<VAR>hf : InjOn f M.E<GOAL>(M.map f hf).Base (f '' B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>B : Set α<VAR>hB : M.Base B<VAR>f : α → β<VAR>hf : InjOn f M.E<GOAL>∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
<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>w : InfinitePlace K<GOAL>w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding
<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>w : InfinitePlace K<GOAL>w.IsComplex → ¬ComplexEmbedding.IsReal w.embedding
<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>φ : K →+* ℂ<VAR>hφ : ¬ComplexEmbedding.IsReal φ<GOAL>¬ComplexEmbedding.IsReal (mk φ).embedding
<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>φ : K →+* ℂ<VAR>hφ : ComplexEmbedding.IsReal (mk φ).embedding<GOAL>ComplexEmbedding.IsReal φ
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h0 : ¬0 = 1<GOAL>(p * q).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>this✝ : DecidableEq R := Classical.decEq R<VAR>h0 : ¬0 = 1<VAR>this : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>(p * q).Monic
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>(eval P) W.polynomial / P z ^ 6 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomial
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j k : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<GOAL>ShortComplex.cyclesMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) = ShortComplex.cyclesMap ((shortComplexFunctor C c i).map φ) ≫ ShortComplex.cyclesMap ((shortComplexFunctor C c i).map ψ)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>x : (i : ι) → α i<GOAL>(x ∈ s.pi fun i => t i ∩ t₁ i) ↔ x ∈ s.pi t ∩ s.pi t₁
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<GOAL>s - s ∩ t + s ∩ t = s - t + s ∩ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>p q : α → Prop<VAR>h : ∀ᶠ (x : α) in f, p x ↔ q x<VAR>hq : ∀ᶠ (x : α) in f, q x<GOAL>∀ᶠ (x : α) in f, q x ↔ p x
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>B : Type u<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra R B<VAR>I : Ideal B<GOAL>FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>B : Type u<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra R B<VAR>I : Ideal B<GOAL>(∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp) ↔ (∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp) ∧ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T T' : L.Theory<VAR>h : M ⊨ T<VAR>h' : M ⊨ T'<GOAL>M ⊨ T ∪ T'
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T T' : L.Theory<VAR>h : ∀ φ ∈ T, M ⊨ φ<VAR>h' : ∀ φ ∈ T', M ⊨ φ<GOAL>∀ (φ : L.Sentence), φ ∈ T ∨ φ ∈ T' → M ⊨ φ
<VAR>x : ℝ<GOAL>x.smoothTransition = 0 ↔ x ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : SigmaFinite μ<VAR>hs : MeasurableSet s<GOAL>(μ.restrict (⋃ i, spanningSets μ i)) s = μ s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>hf : Injective2 f<GOAL>image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>hk : 0 < k<GOAL>(hasseDeriv k) 1 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0<GOAL>IntegrableOn f univ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0<GOAL>∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t✝ t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure<GOAL>t = s.singularPart μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t✝ t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure<GOAL>t = s.singularPart μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t✝ t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : Integrable f μ<VAR>htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure<GOAL>t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure = (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure - (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G✝ : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>G : SimpleGraph W<VAR>e : V ≃ W<GOAL>SimpleGraph.map e.symm.toEmbedding G = SimpleGraph.comap (⇑e.toEmbedding) G
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<GOAL>∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<VAR>A : ⋃ n, closure (⇑f '' ball 0 ↑n) = Set.univ<GOAL>∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<VAR>A : ⋃ n, closure (⇑f '' ball 0 ↑n) = Set.univ<VAR>this : ∃ n x, x ∈ interior (closure (⇑f '' ball 0 ↑n))<GOAL>∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<VAR>A : ⋃ n, closure (⇑f '' ball 0 ↑n) = Set.univ<VAR>this : ∃ n x, ∃ ε > 0, ball x ε ⊆ closure (⇑f '' ball 0 ↑n)<GOAL>∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<VAR>A : ⋃ n, closure (⇑f '' ball 0 ↑n) = Set.univ<VAR>n : ℕ<VAR>a : F<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>H : ball a ε ⊆ closure (⇑f '' ball 0 ↑n)<GOAL>∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<VAR>A : ⋃ n, closure (⇑f '' ball 0 ↑n) = Set.univ<VAR>n : ℕ<VAR>a : F<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>H : ball a ε ⊆ closure (⇑f '' ball 0 ↑n)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<VAR>A : ⋃ n, closure (⇑f '' ball 0 ↑n) = Set.univ<VAR>n : ℕ<VAR>a : F<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>H : ball a ε ⊆ closure (⇑f '' ball 0 ↑n)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>y : F<GOAL>∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<VAR>A : ⋃ n, closure (⇑f '' ball 0 ↑n) = Set.univ<VAR>n : ℕ<VAR>a : F<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>H : ball a ε ⊆ closure (⇑f '' ball 0 ↑n)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>∃ x, dist (f x) 0 ≤ 1 / 2 * ‖0‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖0‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁸ : RingHomInvPair σ σ'<VAR>inst✝⁷ : RingHomInvPair σ' σ<VAR>inst✝⁶ : RingHomIsometric σ<VAR>inst✝⁵ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝ : CompleteSpace F<VAR>surj : Surjective ⇑f<VAR>A : ⋃ n, closure (⇑f '' ball 0 ↑n) = Set.univ<VAR>n : ℕ<VAR>a : F<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>H : ball a ε ⊆ closure (⇑f '' ball 0 ↑n)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>y : F<VAR>hy : y ≠ 0<GOAL>∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddCommMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>m : Multiset R[A]<GOAL>m.prod.support.sup degb ≤ (Multiset.map (fun f => f.support.sup degb) m).sum
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddCommMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>a✝ : List R[A]<GOAL>(Multiset.prod (Quot.mk Setoid.r a✝)).support.sup degb ≤ (Multiset.map (fun f => f.support.sup degb) (Quot.mk Setoid.r a✝)).sum
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddCommMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>a✝ : List R[A]<GOAL>a✝.prod.support.sup degb ≤ (List.map (fun f => f.support.sup degb) a✝).sum
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type v₁<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : FinCategory J<VAR>K✝ : J ⥤ C<VAR>F : C ⥤ D<VAR>inst✝ : RepresentablyFlat F<VAR>c✝ : Cone K✝<VAR>hc✝ : IsLimit c✝<VAR>s✝ : Cone (K✝ ⋙ F)<VAR>K : J ⥤ C<VAR>c : Cone K<VAR>hc : IsLimit c<VAR>s : Cone (K ⋙ F)<VAR>f₁ f₂ : s.pt ⟶ F.obj c.pt<VAR>h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }<VAR>α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }<VAR>c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)<VAR>c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)<VAR>c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)<VAR>g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left<VAR>g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right<GOAL>f₁ = f₂