-- Mathlib/RingTheory/Algebraic/MvPolynomial.lean
theorem transcendental_supported_polynomial_aeval_X {i : σ} {s : Set σ} (h : i ∉ s)
    {f : R[X]} (hf : Transcendental R f) :
    Transcendental (supported R s) (Polynomial.aeval (X i : MvPolynomial σ R) f)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ (((supported R (insert i s)).val.comp
              ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                  (supportedEquivMvPolynomial (insert i s)).symm)).comp
          (mapAlgHom (Polynomial.aeval f))).comp
      ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s)) =
    (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
      ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)

Tactic:
ext1

Result:
case hC
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ ((((supported R (insert i s)).val.comp
                  ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                      (supportedEquivMvPolynomial (insert i s)).symm)).comp
              (mapAlgHom (Polynomial.aeval f))).comp
          ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))).comp
      CAlgHom =
    ((AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
          ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)).comp
      CAlgHom

case hX
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ ((((supported R (insert i s)).val.comp
                ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                    (supportedEquivMvPolynomial (insert i s)).symm)).comp
            (mapAlgHom (Polynomial.aeval f))).comp
        ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s)))
      Polynomial.X =
    ((AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
        ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm))
      Polynomial.X

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Function.Injective ⇑(Polynomial.aeval f)
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))

Tactic:
replace hf : Function.Injective g := MvPolynomial.map_injective _ hf

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
hf : Function.Injective ⇑g
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
hf : Function.Injective ⇑u
⊢ Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))

Tactic:
ext1

Result:
case hX
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
hf : Function.Injective ⇑u
⊢ (Polynomial.aeval (X i)) Polynomial.X =
    (((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
        (Polynomial.aeval (X ⟨i, ⋯⟩)))
      Polynomial.X