-- 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_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)).comp ↑e)

Tactic:
rw [this, AlgHom.coe_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 (⇑(aeval x) ∘ ⇑(rename (Sum.elim Subtype.val Subtype.val)))

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))
⊢ AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i

Tactic:
have _ := @MvPolynomial.isScalarTower

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.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

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 (⇑(AlgHom.restrictScalars R (aeval fun i => x ↑i)) ∘ ⇑e.toEquiv)

Tactic:
show Injective ((AlgHom.restrictScalars R <| aeval _).comp e.toAlgHom)

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)).comp ↑e)

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
⊢ AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i

Tactic:
let e := (sumAlgEquiv R t s).trans (mapAlgEquiv t (hx.comp _ Subtype.val_injective).aevalEquiv)

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)
⊢ AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => 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)
⊢ AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i

Tactic:
have : ((aeval fun i : t ↦ x i).restrictScalars R).comp e.toAlgHom =
    (aeval x).comp (rename <| Sum.elim Subtype.val Subtype.val) := by
  ext (_|_) <;> simp [e, algebraMap_aevalEquiv]

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))
⊢ AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i