ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : V → E<VAR>w : V<GOAL>𝓕⁻ f w = ∫ (v : V), Complex.exp (↑(2 * π * ⟪v, w⟫_ℝ) * Complex.I) • f v
<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>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₁ → R<VAR>hg : g 0 = 0<VAR>φ : MvPolynomial σ S₁<GOAL>(map f) (mapRange g hg φ) = φ ↔ ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ
<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>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₁ → R<VAR>hg : g 0 = 0<VAR>φ : MvPolynomial σ S₁<GOAL>(∀ (m : σ →₀ ℕ), coeff m ((map f) (mapRange g hg φ)) = coeff m φ) ↔ ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ
<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>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₁ → R<VAR>hg : g 0 = 0<VAR>φ : MvPolynomial σ S₁<GOAL>∀ (a : σ →₀ ℕ), coeff a ((map f) (mapRange g hg φ)) = coeff a φ ↔ f (g (coeff a φ)) = coeff a φ
<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>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₁ → R<VAR>hg : g 0 = 0<VAR>φ : MvPolynomial σ S₁<VAR>m : σ →₀ ℕ<GOAL>coeff m ((map f) (mapRange g hg φ)) = coeff m φ ↔ f (g (coeff m φ)) = coeff m φ
<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>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₁ → R<VAR>hg : g 0 = 0<VAR>φ : MvPolynomial σ S₁<VAR>m : σ →₀ ℕ<GOAL>f (coeff m (mapRange g hg φ)) = coeff m φ ↔ f (g (coeff m φ)) = coeff m φ
<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>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₁ → R<VAR>hg : g 0 = 0<VAR>φ : MvPolynomial σ S₁<VAR>m : σ →₀ ℕ<GOAL>f (coeff m (mapRange g hg φ)) = f (g (coeff m φ))
<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✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype m<VAR>A B : Matrix m n α<VAR>x : m → α<VAR>x✝ : n<GOAL>(x ᵥ* (A + B)) x✝ = (x ᵥ* A + x ᵥ* B) 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>hm : m ≤ m0<VAR>T : E' →L[ℝ] E''<VAR>f : ↥(Lp E' 2 μ)<GOAL>↑↑↑((condexpL2 E'' 𝕜' hm) (T.compLp f)) =ᶠ[ae μ] ↑↑(T.compLp ↑((condexpL2 E' 𝕜 hm) f))
<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>hm : m ≤ m0<VAR>T : E' →L[ℝ] E''<VAR>f : ↥(Lp E' 2 μ)<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑((condexpL2 E'' 𝕜' hm) (T.compLp f)) x ∂μ = ∫ (x : α) in s, ↑↑(T.compLp ↑((condexpL2 E' 𝕜 hm) f)) 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>hm : m ≤ m0<VAR>T : E' →L[ℝ] E''<VAR>f : ↥(Lp E' 2 μ)<GOAL>AEStronglyMeasurable' m (↑↑↑((condexpL2 E'' 𝕜' hm) (T.compLp f))) μ
<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>hm : m ≤ m0<VAR>T : E' →L[ℝ] E''<VAR>f : ↥(Lp E' 2 μ)<GOAL>AEStronglyMeasurable' m (↑↑(T.compLp ↑((condexpL2 E' 𝕜 hm) f))) μ
<VAR>α : Sort u<VAR>β : Sort v<VAR>inst✝ : Nonempty α<GOAL>Uncountable α ↔ ∀ (f : ℕ → α), ¬Surjective f
<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 ∈ Submodule.span R ↑s<GOAL>∃ m, m • x ∈ Submodule.span 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 ∈ Submodule.span R ↑s<VAR>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<GOAL>∃ m, m • x ∈ Submodule.span 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 ∈ Submodule.span R ↑s<VAR>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<GOAL>∃ m, m • x ∈ Submodule.span 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 ∈ Submodule.span R ↑s<VAR>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)<GOAL>∃ m, m • x ∈ Submodule.span 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 ∈ Submodule.span R ↑s<VAR>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<GOAL>∃ m, m • x ∈ Submodule.span 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 ∈ Submodule.span R ↑s<VAR>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<GOAL>∃ m, m • x ∈ Submodule.span 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 ∈ Submodule.span R ↑s<VAR>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : Submodule.span R (y' • ↑s) = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<GOAL>∃ m, m • x ∈ Submodule.span 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 ∈ Submodule.span R ↑s<VAR>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<GOAL>∃ m, m • x ∈ Submodule.span 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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx : y' • (algebraMap S S') x ∈ y' • Submodule.span R ↑s<GOAL>∃ m, m • x ∈ Submodule.span 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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx : y' • (algebraMap S S') x ∈ Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<GOAL>∃ m, m • x ∈ Submodule.span 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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx : g (y' • x) ∈ Submodule.map (↑g).toLinearMap (Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<GOAL>∃ m, m • x ∈ Submodule.span 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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>x' : S<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx'' : (algebraMap S S') x' = g (y' • x)<GOAL>∃ m, m • x ∈ Submodule.span 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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>x' : S<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx'' : (algebraMap S S') x' = g (y' • x)<VAR>a : R<VAR>ha₁ : a ∈ ↑M<VAR>ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x<GOAL>∃ m, m • x ∈ Submodule.span 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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>x' : S<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx'' : (algebraMap S S') x' = g (y' • x)<VAR>a : R<VAR>ha₁ : a ∈ ↑M<VAR>ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x<GOAL>(⟨a, ha₁⟩ * ⟨y', hy'⟩) • x ∈ Submodule.span 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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>x' : S<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx'' : (algebraMap S S') x' = g (y' • x)<VAR>a : R<VAR>ha₁ : a ∈ ↑M<VAR>ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x<GOAL>(⟨a, ha₁⟩ * ⟨y', hy'⟩) • x = a • x'
<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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>x' : S<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx'' : (algebraMap S S') x' = g (y' • x)<VAR>a : R<VAR>ha₁ : a ∈ ↑M<VAR>ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x<GOAL>(⟨a, ha₁⟩ * ⟨y', hy'⟩) • x = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
<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>g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s<VAR>y' : R<VAR>hy' : y' ∈ ↑M<VAR>e : (algebraMap R S) y' = ↑y<VAR>this : (algebraMap R S) y' • ↑s = y' • ↑s<VAR>hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>x' : S<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))<VAR>hx'' : (algebraMap S S') x' = g (y' • x)<VAR>a : R<VAR>ha₁ : a ∈ ↑M<VAR>ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x<GOAL>a • x' = ↑⟨(algebraMap R S) a, ⋯⟩ * x'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : 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>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>f : α × β →₀ M<VAR>g : α → β → M → N<VAR>hg₀ : ∀ (a : α) (b : β), g a b 0 = 0<VAR>hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁<GOAL>(fun a b => (single a.1 (single a.2 b)).sum fun a f => f.sum (g a)) = fun p c => g p.1 p.2 c