ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.84186, u_1} C<VAR>inst✝³ : Category.{?u.84190, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hi : IsLimit (KernelFork.ofι S.f ⋯)<GOAL>S.LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.84186, u_1} C<VAR>inst✝³ : Category.{?u.84190, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hi : IsLimit (KernelFork.ofι S.f ⋯)<VAR>f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)<GOAL>S.LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.84186, u_1} C<VAR>inst✝³ : Category.{?u.84190, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hi : IsLimit (KernelFork.ofι S.f ⋯)<VAR>f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)<VAR>hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt<GOAL>S.LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.84186, u_1} C<VAR>inst✝³ : Category.{?u.84190, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hi : IsLimit (KernelFork.ofι S.f ⋯)<VAR>f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)<VAR>hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt<VAR>wπ : f' ≫ 0 = 0<GOAL>S.LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.84186, u_1} C<VAR>inst✝³ : Category.{?u.84190, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hi : IsLimit (KernelFork.ofι S.f ⋯)<VAR>f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)<VAR>hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt<VAR>wπ : f' ≫ 0 = 0<VAR>hπ : IsColimit (CokernelCofork.ofπ 0 wπ)<GOAL>S.LeftHomologyData
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<GOAL>(∀ (U_1 : ↑(↑(f ⁻¹ᵁ U)).affineOpens), P (Hom.appLE (f ∣_ U) ⊤ ↑U_1 ⋯)) ↔ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (Hom.appLE f U (↑V) e)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<GOAL>(∀ (U_1 : ↑(↑(f ⁻¹ᵁ U)).affineOpens), P (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑U_1) ⋯)) ↔ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (Hom.appLE f U (↑V) e)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<GOAL>(∀ (a : ↑X.affineOpens) (b : ↑a ≤ f ⁻¹ᵁ U), P (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨a, b⟩)) ⋯)) ↔ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (Hom.appLE f U (↑V) e)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<VAR>V : ↑X.affineOpens<VAR>h : ↑V ≤ f ⁻¹ᵁ U<GOAL>P (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩)) ⋯) ↔ P (Hom.appLE f U (↑V) h)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<VAR>V : ↑X.affineOpens<VAR>h : ↑V ≤ f ⁻¹ᵁ U<VAR>this : (affineOpensRestrict (f ⁻¹ᵁ U)) ((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩) = ⟨V, h⟩<GOAL>P (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨V, h⟩)) ⋯) ↔ P (Hom.appLE f U (↑V) h)
<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>n : ℕ<VAR>H : p.degree ≤ ↑n<VAR>H1 : p.degree < ↑(n + 1)<GOAL>(X ^ (n + 1) + p).coeff (n + 1) = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : M<GOAL>m ∈ span R (range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : M<VAR>h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)<GOAL>m ∈ span R (range ⇑b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : M<VAR>h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)<GOAL>((b.repr m).sum fun i a => a • b i) ∈ span R (range ⇑b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : M<VAR>h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)<VAR>i : ι<VAR>x✝ : i ∈ (b.repr m).support<GOAL>(fun i a => a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : M<VAR>h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)<VAR>i : ι<VAR>x✝ : i ∈ (b.repr m).support<VAR>w✝ : R<VAR>h : (algebraMap R S) w✝ = (b.repr m) i<GOAL>(fun i a => a • b i) i ((b.repr m) i) ∈ span R (range ⇑b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : M<VAR>h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)<VAR>i : ι<VAR>x✝ : i ∈ (b.repr m).support<VAR>w✝ : R<VAR>h : (algebraMap R S) w✝ = (b.repr m) i<GOAL>w✝ • b i ∈ span R (range ⇑b)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Coalgebra R A<VAR>a : A<GOAL>(TensorProduct.assoc R A A A).symm ((LinearMap.lTensor A comul) (comul a)) = (LinearMap.rTensor A comul) (comul a)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hp : 0 < p.degree<GOAL>(p - C a).degree = p.degree
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>this : Nonempty α<GOAL>edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>this : Nonempty α<VAR>cs : Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b) ∈ s<VAR>hc : variationOnFromTo f s a (Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b)) = variationOnFromTo f s a b<GOAL>edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>this : Nonempty α<VAR>cs : Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b) ∈ s<VAR>hc : variationOnFromTo f s (Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b)) b = 0<GOAL>edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>inst✝⁴ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₂₃<VAR>inst✝ : RingHomIsometric σ₁₃<VAR>f : E →SL[σ₁₃] F →SL[σ₂₃] G<GOAL>‖f.flip‖ ≤ ‖f‖
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarModule R A<VAR>inst✝⁶ : TopologicalSemiring A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : T2Space B<VAR>S : StarSubalgebra R A<VAR>φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarModule R A<VAR>inst✝⁶ : TopologicalSemiring A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : T2Space B<VAR>S : StarSubalgebra R A<VAR>φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)<GOAL>⇑φ = ⇑ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarModule R A<VAR>inst✝⁶ : TopologicalSemiring A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : T2Space B<VAR>S : StarSubalgebra R A<VAR>φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)<VAR>this : Dense (range ⇑(inclusion ⋯))<GOAL>⇑φ = ⇑ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarModule R A<VAR>inst✝⁶ : TopologicalSemiring A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : T2Space B<VAR>S : StarSubalgebra R A<VAR>φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)<VAR>this : Dense (range ⇑(inclusion ⋯))<GOAL>EqOn (⇑φ) (⇑ψ) (range ⇑(inclusion ⋯))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarModule R A<VAR>inst✝⁶ : TopologicalSemiring A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : T2Space B<VAR>S : StarSubalgebra R A<VAR>φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)<VAR>this : Dense (range ⇑(inclusion ⋯))<VAR>x : ↥S<GOAL>φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>x : E × F<GOAL>Tendsto (fun x_1 => f x_1 - f x) (𝓝 x) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>x : E × F<GOAL>Tendsto (fun y => f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0))
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>x : E × F<GOAL>Tendsto (fun x_1 => f (x_1.1 - x.1, x_1.2)) (𝓝 x) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>x : E × F<GOAL>Tendsto (fun x_1 => f (x.1, x_1.2 - x.2)) (𝓝 x) (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²⁰ : RCLike 𝕜<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>inst✝ : SigmaFinite (μ.trim hm)<GOAL>∫⁻ (a : α), ↑‖↑↑(condexpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²⁰ : RCLike 𝕜<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (x_1 : α) in t, ↑‖↑↑(condexpIndSMul hm hs hμs x) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²⁰ : RCLike 𝕜<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>μ (s ∩ t) * ↑‖x‖₊ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²⁰ : RCLike 𝕜<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>s ∩ t ⊆ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>h : ∞ ∈ s<VAR>this : ∞ ∉ sᶜ<GOAL>IsClosed s ↔ IsClosed (some ⁻¹' s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>h : a * b = 1<GOAL>IsSMulRegular M 1
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hg : GrowsPolynomially g<GOAL>GrowsPolynomially fun x => f x / g x
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hg : GrowsPolynomially g<VAR>this : (fun x => f x / g x) = fun x => f x * (g x)⁻¹<GOAL>GrowsPolynomially fun x => f x / g x
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hg : GrowsPolynomially g<VAR>this : (fun x => f x / g x) = fun x => f x * (g x)⁻¹<GOAL>GrowsPolynomially fun x => f x * (g x)⁻¹
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>support✝ : Finset ℕ<VAR>toFun✝ : ℕ → R<VAR>mem_support_toFun✝ : ∀ (a : ℕ), a ∈ support✝ ↔ toFun✝ a ≠ 0<GOAL>{ toFinsupp := Finsupp.erase n { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } } = erase n { toFinsupp := { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } }
<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>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x y : R<GOAL>(algebraMap R T) x = (algebraMap R T) y → ∃ c, ↑c * x = ↑c * y
<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>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x y : R<GOAL>(∃ c, ↑c * (algebraMap R S) x = ↑c * (algebraMap R S) y) → ∃ c, ↑c * x = ↑c * y
<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>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x y : R<VAR>z : ↥N<VAR>eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y<GOAL>∃ c, ↑c * x = ↑c * y
<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>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x y : R<VAR>z : ↥N<VAR>eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y<VAR>z' : R<VAR>s : ↥M<VAR>eq₂ : ↑z * (algebraMap R S) ↑(z', s).2 = (algebraMap R S) (z', s).1<GOAL>∃ c, ↑c * x = ↑c * y
<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>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x y : R<VAR>z : ↥N<VAR>eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y<VAR>z' : R<VAR>s : ↥M<VAR>eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'<GOAL>(algebraMap R S) (x * z') = (algebraMap R S) (y * z')