-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.restrictScalars {K : Type*} [CommRing K] [Algebra R K] [Algebra K A]
    [IsScalarTower R K A] (hinj : Function.Injective (algebraMap R K))
    (ai : AlgebraicIndependent K x) : AlgebraicIndependent R x

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_7
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom
⊢ Injective ⇑(aeval x).toRingHom

Tactic:
rw [← this, RingHom.coe_comp]

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_7
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom
⊢ Injective (⇑(aeval x).toRingHom ∘ ⇑(MvPolynomial.map (algebraMap R K)))

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_7
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom
⊢ Injective (⇑(aeval x).toRingHom ∘ ⇑(MvPolynomial.map (algebraMap R K)))

Tactic:
exact Injective.comp ai (MvPolynomial.map_injective _ hinj)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_7
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom
⊢ AlgebraicIndependent R x

Tactic:
show Injective (aeval x).toRingHom

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_7
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom
⊢ Injective ⇑(aeval x).toRingHom

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_7
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
⊢ (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom

Tactic:
ext <;> simp [algebraMap_eq_smul_one]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_7
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
⊢ AlgebraicIndependent R x

Tactic:
have : (aeval x : MvPolynomial ι K →ₐ[K] A).toRingHom.comp (MvPolynomial.map (algebraMap R K)) =
    (aeval x : MvPolynomial ι R →ₐ[R] A).toRingHom := by
  ext <;> simp [algebraMap_eq_smul_one]

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_7
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom
⊢ AlgebraicIndependent R x