-- Mathlib/RingTheory/Algebraic/MvPolynomial.lean
theorem transcendental_polynomial_aeval_X (i : σ) {f : R[X]} (hf : Transcendental R f) :
    Transcendental R (Polynomial.aeval (X i : MvPolynomial σ R) f)

Proof state:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
x✝ : R
⊢ ((algebraMap (↥(supported R ∅)) (MvPolynomial σ R)).comp ↑g) x✝ =
    ((↑(RingHom.id (MvPolynomial σ R))).comp (algebraMap R (MvPolynomial σ R))) x✝

Tactic:
rfl

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
rwa [Transcendental, ← isAlgebraic_ringHom_iff_of_comp_eq g (RingHom.id (MvPolynomial σ R))
  Function.injective_id (by ext1; rfl), RingHom.id_apply, ← Transcendental]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
let g := (Algebra.botEquivOfInjective (MvPolynomial.C_injective σ R)).symm.trans
  (Subalgebra.equivOfEq _ _ supported_empty).symm

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
have := transcendental_supported_polynomial_aeval_X R (Set.not_mem_empty i) hf

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ (algebraMap (↥(supported R ∅)) (MvPolynomial σ R)).comp ↑g =
    (↑(RingHom.id (MvPolynomial σ R))).comp (algebraMap R (MvPolynomial σ R))

Tactic:
ext1

Result:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
x✝ : R
⊢ ((algebraMap (↥(supported R ∅)) (MvPolynomial σ R)).comp ↑g) x✝ =
    ((↑(RingHom.id (MvPolynomial σ R))).comp (algebraMap R (MvPolynomial σ R))) x✝