-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem algebraicIndependent_unique_type_iff [Unique ι] :
    AlgebraicIndependent R x ↔ Transcendental R (x default)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
⊢ AlgebraicIndependent R x ↔ Transcendental R (x default)

Tactic:
rw [transcendental_iff_injective, algebraicIndependent_iff_injective_aeval]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := (renameEquiv R (Equiv.equivPUnit ι)).trans (pUnitAlgEquiv R)
key : aeval x = (Polynomial.aeval (x default)).comp ↑i
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Tactic:
simp [key]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := (renameEquiv R (Equiv.equivPUnit ι)).trans (pUnitAlgEquiv R)
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Tactic:
have key : aeval (R := R) x = (Polynomial.aeval (R := R) (x default)).comp i := by
  ext y
  simp [i, Subsingleton.elim y default]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := (renameEquiv R (Equiv.equivPUnit ι)).trans (pUnitAlgEquiv R)
key : aeval x = (Polynomial.aeval (x default)).comp ↑i
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Tactic:
let i := (renameEquiv R (Equiv.equivPUnit.{_, 1} ι)).trans (pUnitAlgEquiv R)

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := (renameEquiv R (Equiv.equivPUnit ι)).trans (pUnitAlgEquiv R)
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := (renameEquiv R (Equiv.equivPUnit ι)).trans (pUnitAlgEquiv R)
⊢ aeval x = (Polynomial.aeval (x default)).comp ↑i

Tactic:
ext y

Result:
case hf
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := (renameEquiv R (Equiv.equivPUnit ι)).trans (pUnitAlgEquiv R)
y : ι
⊢ (aeval x) (X y) = ((Polynomial.aeval (x default)).comp ↑i) (X y)

Proof state:
case hf
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := (renameEquiv R (Equiv.equivPUnit ι)).trans (pUnitAlgEquiv R)
y : ι
⊢ (aeval x) (X y) = ((Polynomial.aeval (x default)).comp ↑i) (X y)

Tactic:
simp [i, Subsingleton.elim y default]

Result:
no goals