-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem adjoin_of_disjoint {s t : Set ι} (h : Disjoint s t) :
    AlgebraicIndependent (adjoin R (x '' s)) fun i : t ↦ x i

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
hx : AlgebraicIndependent R x
s t : Set ι
h : Disjoint s t
e : MvPolynomial (↑t ⊕ ↑s) R ≃ₐ[R] MvPolynomial ↑t ↥(adjoin R (range (x ∘ Subtype.val))) :=
  (sumAlgEquiv R ↑t ↑s).trans (mapAlgEquiv ↑t ⋯.aevalEquiv)
this :
  (AlgHom.restrictScalars R (aeval fun i => x ↑i)).comp ↑e = (aeval x).comp (rename (Sum.elim Subtype.val Subtype.val))
x✝ :
  ∀ {R : Type ?u.44434} {S₁ : Type ?u.44433} {S₂ : Type ?u.44432} {σ : Type ?u.44431} [inst : CommSemiring S₂]
    [inst_1 : SMul R S₁] [inst_2 : SMulZeroClass R S₂] [inst_3 : SMulZeroClass S₁ S₂] [inst_4 : IsScalarTower R S₁ S₂],
    IsScalarTower R S₁ (MvPolynomial σ S₂)
⊢ AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i

Tactic:
rw [Set.image_eq_range, AlgebraicIndependent, ← AlgHom.coe_restrictScalars' R, ← e.injective_comp]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
s t : Set ι
h : Disjoint s t
e : MvPolynomial (↑t ⊕ ↑s) R ≃ₐ[R] MvPolynomial ↑t ↥(adjoin R (range (x ∘ Subtype.val))) :=
  (sumAlgEquiv R ↑t ↑s).trans (mapAlgEquiv ↑t ⋯.aevalEquiv)
this :
  (AlgHom.restrictScalars R (aeval fun i => x ↑i)).comp ↑e = (aeval x).comp (rename (Sum.elim Subtype.val Subtype.val))
x✝ :
  ∀ {R : Type u_2} {S₁ S₂ : Type u_3} {σ : Type u_1} [inst : CommSemiring S₂] [inst_1 : SMul R S₁]
    [inst_2 : SMulZeroClass R S₂] [inst_3 : SMulZeroClass S₁ S₂] [inst_4 : IsScalarTower R S₁ S₂],
    IsScalarTower R S₁ (MvPolynomial σ S₂)
⊢ Injective (⇑(AlgHom.restrictScalars R (aeval fun i => x ↑i)) ∘ ⇑e.toEquiv)

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
hx : AlgebraicIndependent R x
s t : Set ι
h : Disjoint s t
e : MvPolynomial (↑t ⊕ ↑s) R ≃ₐ[R] MvPolynomial ↑t ↥(adjoin R (range (x ∘ Subtype.val))) :=
  (sumAlgEquiv R ↑t ↑s).trans (mapAlgEquiv ↑t ⋯.aevalEquiv)
⊢ (AlgHom.restrictScalars R (aeval fun i => x ↑i)).comp ↑e = (aeval x).comp (rename (Sum.elim Subtype.val Subtype.val))

Tactic:
ext (_|_) <;> simp [e, algebraMap_aevalEquiv]

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
hx : AlgebraicIndependent R x
s t : Set ι
h : Disjoint s t
e : MvPolynomial (↑t ⊕ ↑s) R ≃ₐ[R] MvPolynomial ↑t ↥(adjoin R (range (x ∘ Subtype.val))) :=
  (sumAlgEquiv R ↑t ↑s).trans (mapAlgEquiv ↑t ⋯.aevalEquiv)
this :
  (AlgHom.restrictScalars R (aeval fun i => x ↑i)).comp ↑e = (aeval x).comp (rename (Sum.elim Subtype.val Subtype.val))
x✝ :
  ∀ {R : Type u_2} {S₁ S₂ : Type u_3} {σ : Type u_1} [inst : CommSemiring S₂] [inst_1 : SMul R S₁]
    [inst_2 : SMulZeroClass R S₂] [inst_3 : SMulZeroClass S₁ S₂] [inst_4 : IsScalarTower R S₁ S₂],
    IsScalarTower R S₁ (MvPolynomial σ S₂)
⊢ Injective (⇑(aeval x) ∘ ⇑(rename (Sum.elim Subtype.val Subtype.val)))

Tactic:
exact .comp hx (rename_injective _ <| Subtype.val_injective.sumElim
  Subtype.val_injective fun i j eq ↦ h.ne_of_mem j.2 i.2 eq.symm)

Result:
no goals