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

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
⊢ (Polynomial.aeval (X i)) f ∈ supported R s

Tactic:
exact Algebra.adjoin_mono (Set.singleton_subset_iff.2 (Set.mem_image_of_mem _ h))
  (Polynomial.aeval_mem_adjoin_singleton _ _)

Result:
no goals

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s

Tactic:
rw [Transcendental] at h

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : ¬IsAlgebraic (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
⊢ IsAlgebraic (↥(supported R s)) ((Polynomial.aeval (X i)) f)

Tactic:
refine isAlgebraic_algebraMap (⟨Polynomial.aeval (X i) f, ?_⟩ : supported R s)

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
⊢ (Polynomial.aeval (X i)) f ∈ supported R s

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R f

Tactic:
rw [← transcendental_polynomial_aeval_X_iff R i]

Result:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
refine h.restrictScalars fun _ _ heq ↦ MvPolynomial.C_injective σ R ?_

Result:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ C x✝¹ = C x✝

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ C x✝¹ = C x✝

Tactic:
simp_rw [← MvPolynomial.algebraMap_eq]

Result:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ (algebraMap R (MvPolynomial σ R)) x✝¹ = (algebraMap R (MvPolynomial σ R)) x✝

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
⊢ Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f) ↔ i ∉ s ∧ Transcendental R f

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, hf⟩ ↦ transcendental_supported_polynomial_aeval_X R h hf⟩

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s

case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R f

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : ¬IsAlgebraic (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s

Tactic:
contrapose! h

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
⊢ IsAlgebraic (↥(supported R s)) ((Polynomial.aeval (X i)) f)

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ (algebraMap R (MvPolynomial σ R)) x✝¹ = (algebraMap R (MvPolynomial σ R)) x✝

Tactic:
exact congr($(heq).1)

Result:
no goals