-- Mathlib/RingTheory/Localization/Algebra.lean
/-- If `A` is the localization of `R` at a submonoid `S`, then `A[X]` is the localization of
`R[X]` at `S.map Polynomial.C`.

See also `MvPolynomial.isLocalization` for the multivariate case. -/
lemma isLocalization {R} [CommRing R] (S : Submonoid R) (A) [CommRing A] [Algebra R A]
    [IsLocalization S A] : letI := (mapRingHom (algebraMap R A)).toAlgebra
    IsLocalization (S.map C) A[X]

Proof state:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
this✝ : Algebra R[X] A[X] := (mapRingHom (algebraMap R A)).toAlgebra
this : IsScalarTower R R[X] A[X]
x✝ : R[X]
⊢ (polyEquivTensor' R A).symm.toLinearEquiv (1 ⊗ₜ[R] x✝) = eval₂ (C.comp (algebraMap R A)) X x✝

Tactic:
simp [eval₂, ← C_mul_X_pow_eq_monomial]

Result:
no goals

Proof state:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
⊢ IsLocalization (Submonoid.map C S) A[X]

Tactic:
letI := (mapRingHom (algebraMap R A)).toAlgebra

Result:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
this : Algebra R[X] A[X] := (mapRingHom (algebraMap R A)).toAlgebra
⊢ IsLocalization (Submonoid.map C S) A[X]

Proof state:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
this✝ : Algebra R[X] A[X] := (mapRingHom (algebraMap R A)).toAlgebra
this : IsScalarTower R R[X] A[X]
⊢ IsLocalization (Submonoid.map C S) A[X]

Tactic:
apply isLocalizedModule_iff_isLocalization.mp <| (isLocalizedModule_iff_isBaseChange S A _).mpr <|
  .of_equiv (polyEquivTensor' R A).symm.toLinearEquiv fun _ ↦ ?_

Result:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
this✝ : Algebra R[X] A[X] := (mapRingHom (algebraMap R A)).toAlgebra
this : IsScalarTower R R[X] A[X]
x✝ : R[X]
⊢ (polyEquivTensor' R A).symm.toLinearEquiv (1 ⊗ₜ[R] x✝) = (IsScalarTower.toAlgHom R R[X] A[X]).toLinearMap x✝

Proof state:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
this✝ : Algebra R[X] A[X] := (mapRingHom (algebraMap R A)).toAlgebra
this : IsScalarTower R R[X] A[X]
x✝ : R[X]
⊢ (polyEquivTensor' R A).symm.toLinearEquiv (1 ⊗ₜ[R] x✝) = (IsScalarTower.toAlgHom R R[X] A[X]).toLinearMap x✝

Tactic:
show _ = eval₂ ..

Result:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
this✝ : Algebra R[X] A[X] := (mapRingHom (algebraMap R A)).toAlgebra
this : IsScalarTower R R[X] A[X]
x✝ : R[X]
⊢ (polyEquivTensor' R A).symm.toLinearEquiv (1 ⊗ₜ[R] x✝) = eval₂ (C.comp (algebraMap R A)) X x✝

Proof state:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
this : Algebra R[X] A[X] := (mapRingHom (algebraMap R A)).toAlgebra
⊢ IsLocalization (Submonoid.map C S) A[X]

Tactic:
have : IsScalarTower R R[X] A[X] := .of_algebraMap_eq fun _ ↦ (map_C _).symm

Result:
R : Type u_5
inst✝³ : CommRing R
S : Submonoid R
A : Type u_6
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
this✝ : Algebra R[X] A[X] := (mapRingHom (algebraMap R A)).toAlgebra
this : IsScalarTower R R[X] A[X]
⊢ IsLocalization (Submonoid.map C S) A[X]