-- Module: Mathlib.RingTheory.Algebraic.MvPolynomial
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Transcendental R f
rw rw₁ rw₂ :
  ∀ (hf : Function.Injective (α := R[X]) (β := R[X]) (⇑(Polynomial.aeval f) : (a : R[X]) → R[X])),
    Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
      (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
            (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
        (a : (↥(supported R s))[X]) → MvPolynomial σ R)
rw₃ :
  ∀ (hf : Function.Injective (α := R[X]) (β := R[X]) (⇑(Polynomial.aeval f) : (a : R[X]) → R[X])),
    Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
      (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
            (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
        (a : (↥(supported R s))[X]) → MvPolynomial σ R)
rw₄ rw₅ rw₆ :
  let g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
    mapAlgHom (Polynomial.aeval f);
  ∀
    (hf :
      Function.Injective (α := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X]) (β :=
        MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
        (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])),
    Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
      (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
            (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
        (a : (↥(supported R s))[X]) → MvPolynomial σ R)
rw₇ :
  let g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
    mapAlgHom (Polynomial.aeval f);
  let u :=
    (AlgHom.comp
          (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
            (↑(AlgEquiv.trans
                  (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                    (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                  (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
              MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
          g).comp
      (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
        (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X]);
  ∀
    (hf :
      Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
        (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R)),
    Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
      (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
            (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
        (a : (↥(supported R s))[X]) → MvPolynomial σ R)
rw₈ :
  let g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
    mapAlgHom (Polynomial.aeval f);
  let u :=
    (AlgHom.comp
          (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
            (↑(AlgEquiv.trans
                  (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                    (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                  (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
              MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
          g).comp
      (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
        (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X]);
  ∀
    (hf :
      Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
        (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R))
    (h1 :
      Eq (α := R[X] →ₐ[R] MvPolynomial σ R) (Polynomial.aeval (X i))
        (AlgHom.comp
          (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
            (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
              MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
          (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯))))),
    Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
      (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
            (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
        (a : (↥(supported R s))[X]) → MvPolynomial σ R)
rw₉ :
  let g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
    mapAlgHom (Polynomial.aeval f);
  let u :=
    (AlgHom.comp
          (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
            (↑(AlgEquiv.trans
                  (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                    (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                  (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
              MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
          g).comp
      (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
        (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X]);
  let v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
    AlgHom.comp
      (AlgHom.restrictScalars R (S := ↥(supported R s))
        (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
      (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
        (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X]);
  ∀
    (hf :
      Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := MvPolynomial σ R)
        (⇑u : (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial σ R))
    (h1 :
      Eq (α := R[X] →ₐ[R] MvPolynomial σ R) (Polynomial.aeval (X i))
        (AlgHom.comp
          (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
            (↑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
              MvPolynomial (↑(insert i s) : Type u_1) R →ₐ[R] ↥(supported R (insert i s))))
          (Polynomial.aeval (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert i s) i ⋯)))))
    (h2 : u = v),
    Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
      (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
            (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
        (a : (↥(supported R s))[X]) → MvPolynomial σ R)
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)

Tactic:
classical
  rw [transcendental_iff_injective] at hf ⊢
  let g := MvPolynomial.mapAlgHom (R := R) (σ := s) (Polynomial.aeval (R := R) f)
  replace hf : Function.Injective g := MvPolynomial.map_injective _ hf
  let u := (Subalgebra.val _).comp
    ((optionEquivRight R s).symm |>.trans
      (renameEquiv R (Set.subtypeInsertEquivOption h).symm) |>.trans
      (supportedEquivMvPolynomial _).symm).toAlgHom |>.comp
    g |>.comp
    ((optionEquivLeft R s).symm.trans (optionEquivRight R s)).toAlgHom
  let v := ((Polynomial.aeval (R := supported R s)
    (Polynomial.aeval (X i : MvPolynomial σ R) f)).restrictScalars R).comp
      (Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm).toAlgHom
  replace hf : Function.Injective u := by
    simp only [AlgHom.coe_comp, Subalgebra.coe_val,
      AlgEquiv.coe_algHom, AlgEquiv.coe_trans, Function.comp_assoc, u]
    apply Subtype.val_injective.comp
    simp only [EquivLike.comp_injective]
    apply hf.comp
    simp only [EquivLike.comp_injective, EquivLike.injective]
  have h1 : Polynomial.aeval (X i : MvPolynomial σ R) = ((Subalgebra.val _).comp
      (supportedEquivMvPolynomial _).symm.toAlgHom |>.comp
      (Polynomial.aeval (X ⟨i, s.mem_insert i⟩ : MvPolynomial ↑(insert i s) R))) := by
    ext1; simp
  have h2 : u = v := by
    simp only [u, v, g]
    ext1
    · ext1
      simp [Set.subtypeInsertEquivOption, Subalgebra.algebraMap_eq, optionEquivLeft_symm_apply]
    · simp [Set.subtypeInsertEquivOption, h1, optionEquivLeft_symm_apply]
  simpa only [h2, v, AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.injective_comp, AlgHom.coe_restrictScalars'] using hf

Premises used: transcendental_iff_injective, EquivLike.injective_comp, AlgHom.coe_comp, AlgHom.coe_restrictScalars', AlgEquiv.coe_algHom