ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)<VAR>h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x<VAR>x : ℝ<VAR>hx : x ∈ Set.Iio 0<GOAL>x ∈ {0}ᶜ
<VAR>h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)<VAR>h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x<VAR>x : ℝ<VAR>hx : x < 0<GOAL>x ∈ {0}ᶜ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<GOAL>P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<GOAL>P.symm.Λ s + (1 / s) • P.symm.f₀ + (P.symm.ε / (↑P.symm.k - s)) • P.symm.g₀ = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : AddTorsor G P<VAR>v₁ v₂ : G<VAR>p₁ p₂ : P<GOAL>v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MetricSpace α<VAR>s : Set α<VAR>inst✝ : Finite ↑s<GOAL>0 < s.infsep ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MetricSpace α<VAR>s : Set α<VAR>inst✝ : Finite ↑s<GOAL>s.Nontrivial → 0 < s.einfsep
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>f : Aut F<VAR>A : C<VAR>inst✝ : IsGalois A<VAR>a : ↑(F.obj A)<GOAL>F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) ((endEquivAutGalois F) ↑((Aut.unitsEndEquivAut F).symm f))).hom a = f.hom.app A a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>f : Aut F<VAR>A : C<VAR>inst✝ : IsGalois A<VAR>a : ↑(F.obj A)<GOAL>(↑((Aut.unitsEndEquivAut F).symm f)).app { obj := A, pt := a, isGalois := ⋯ }.obj { obj := A, pt := a, isGalois := ⋯ }.pt = f.hom.app A a
<VAR>s : ℂ<VAR>hs : s ≠ 0<GOAL>(s + 1).Gammaℂ = s.Gammaℂ * s / 2 / ↑π
<VAR>s : ℂ<VAR>hs : s ≠ 0<GOAL>2 * ((2 * ↑π) ^ (-s) * (2 * ↑π)⁻¹) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s / 2 / ↑π
<VAR>s : ℂ<VAR>hs : s ≠ 0<GOAL>2 * (2 * ↑π) ^ (-s) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹⁵ : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹⁴ : NormedAddCommGroup EB<VAR>inst✝¹³ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹² : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝¹¹ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup EM<VAR>inst✝⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : ChartedSpace HB B<VAR>inst✝³ : FiberBundle F E<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝ : VectorBundle 𝕜 F E<VAR>x : B<GOAL>ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) ⊤ (fun x => { proj := x, snd := 0 }) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹⁵ : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹⁴ : NormedAddCommGroup EB<VAR>inst✝¹³ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹² : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝¹¹ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup EM<VAR>inst✝⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : ChartedSpace HB B<VAR>inst✝³ : FiberBundle F E<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝ : VectorBundle 𝕜 F E<VAR>x : B<GOAL>ContMDiffAt IB 𝓘(𝕜, F) ⊤ (fun x_1 => (↑(trivializationAt F E x) { proj := x_1, snd := 0 }).2) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹⁵ : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹⁴ : NormedAddCommGroup EB<VAR>inst✝¹³ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹² : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝¹¹ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup EM<VAR>inst✝⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : ChartedSpace HB B<VAR>inst✝³ : FiberBundle F E<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝ : VectorBundle 𝕜 F E<VAR>x : B<GOAL>(fun x_1 => (↑(trivializationAt F E x) { proj := x_1, snd := 0 }).2) =ᶠ[𝓝 x] fun x => 0
<VAR>α : Type u_1<VAR>a b : ℂ<VAR>ha : a ≠ 0<GOAL>ContinuousAt (fun x => a ^ x) b
<VAR>α : Type u_1<VAR>a b : ℂ<VAR>ha : a ≠ 0<VAR>cpow_eq : (fun x => a ^ x) = fun x => cexp (Complex.log a * x)<GOAL>ContinuousAt (fun x => a ^ x) b
<VAR>α : Type u_1<VAR>a b : ℂ<VAR>ha : a ≠ 0<VAR>cpow_eq : (fun x => a ^ x) = fun x => cexp (Complex.log a * x)<GOAL>ContinuousAt (fun x => cexp (Complex.log a * x)) b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>inst✝¹ : HasProduct I.left<VAR>inst✝ : HasProduct I.right<VAR>K : Multifork I<GOAL>∀ (j : WalkingMulticospan I.fstTo I.sndTo), ((𝟭 (Multifork I)).obj K).π.app j = (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫ ((I.toPiForkFunctor ⋙ I.ofPiForkFunctor).obj K).π.app j
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<GOAL>MeasurePreserving (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<GOAL>(fun z => (z.2 * z.1, z.1⁻¹)) = (fun z => (z.2, z.2⁻¹ * z.1)) ∘ fun z => (z.2, z.2 * z.1)
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>x y : G<GOAL>((x, y).2 * (x, y).1, (x, y).1⁻¹) = ((fun z => (z.2, z.2⁻¹ * z.1)) ∘ fun z => (z.2, z.2 * z.1)) (x, y)
<VAR>N : ℕ<VAR>inst✝² : NeZero N<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>inst✝ : IsDomain R<VAR>χ : DirichletCharacter R N<VAR>hχ : χ.IsPrimitive<VAR>he : ¬e.IsPrimitive<GOAL>gaussSum χ e = 0
<VAR>N : ℕ<VAR>inst✝² : NeZero N<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>inst✝ : IsDomain R<VAR>χ : DirichletCharacter R N<VAR>he : ¬e.IsPrimitive<VAR>hχ : gaussSum χ e ≠ 0<GOAL>¬χ.IsPrimitive
<VAR>N : ℕ<VAR>inst✝² : NeZero N<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>inst✝ : IsDomain R<VAR>χ : DirichletCharacter R N<VAR>he : ¬e.IsPrimitive<VAR>hχ : gaussSum χ e ≠ 0<VAR>d : ℕ<VAR>hd₁ : d ∣ N<VAR>hd₂ : d < N<VAR>hed : e.mulShift ↑d = 1<GOAL>¬χ.IsPrimitive
<VAR>N : ℕ<VAR>inst✝² : NeZero N<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>inst✝ : IsDomain R<VAR>χ : DirichletCharacter R N<VAR>he : ¬e.IsPrimitive<VAR>hχ : gaussSum χ e ≠ 0<VAR>d : ℕ<VAR>hd₁ : d ∣ N<VAR>hd₂ : d < N<VAR>hed : e.mulShift ↑d = 1<VAR>this : χ.conductor ≤ d<GOAL>¬χ.IsPrimitive
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<GOAL>∀ (x : V), ((-o).rotation θ) x = (o.rotation (-θ)) x
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>ι : Type u_2<VAR>f : ι → Subgroup α<VAR>H : Subgroup α<GOAL>∀ (a₁ a₂ : ↥H), (fun q i => quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁) = (fun q i => quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂) → Quotient.mk'' a₁ = Quotient.mk'' a₂
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>0 = 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆)
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<GOAL>(IsLocalization.map S' f ⋯).FiniteType
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<GOAL>(IsLocalization.map S' f ⋯).FiniteType
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝¹ : Algebra R S := f.toAlgebra<VAR>this✝ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this : Algebra R' S' := f'.toAlgebra<GOAL>(IsLocalization.map S' f ⋯).FiniteType
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<GOAL>(IsLocalization.map S' f ⋯).FiniteType
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<GOAL>(IsLocalization.map S' f ⋯).FiniteType
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<GOAL>(IsLocalization.map S' f ⋯).FiniteType
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<GOAL>Algebra.adjoin R' ↑(Finset.image (⇑(algebraMap S S')) T) = ⊤
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<GOAL>⊤ ≤ Algebra.adjoin R' ↑(Finset.image (⇑(algebraMap S S')) T)
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>x : S'<GOAL>x ∈ Algebra.adjoin R' ↑(Finset.image (⇑(algebraMap S S')) T)
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<GOAL>IsLocalization.mk' S' y ⟨f r, ⋯⟩ ∈ Algebra.adjoin R' ↑(Finset.image (⇑(algebraMap S S')) T)
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<GOAL>IsLocalization.mk' S' 1 ⟨f r, ⋯⟩ * (algebraMap S S') y ∈ Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T)
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<VAR>hy : y ∈ Algebra.adjoin R ↑T<GOAL>IsLocalization.mk' S' 1 ⟨f r, ⋯⟩ * (algebraMap S S') y ∈ Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T)
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<VAR>hy : (algebraMap S S') y ∈ Subalgebra.map fₐ (Algebra.adjoin R ↑T)<GOAL>IsLocalization.mk' S' 1 ⟨f r, ⋯⟩ * (algebraMap S S') y ∈ Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T)
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<VAR>hy : (algebraMap S S') y ∈ Algebra.adjoin R (⇑fₐ '' ↑T)<GOAL>IsLocalization.mk' S' 1 ⟨f r, ⋯⟩ * (algebraMap S S') y ∈ Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T)
<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>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<VAR>hy : (algebraMap S S') y ∈ Algebra.adjoin R (⇑fₐ '' ↑T)<VAR>H : Algebra.adjoin R (⇑(algebraMap S S') '' ↑T) ≤ Subalgebra.restrictScalars R (Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T))<GOAL>IsLocalization.mk' S' 1 ⟨f r, ⋯⟩ * (algebraMap S S') y ∈ Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T)