-- 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]
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)
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (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])
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 ⋯))))
hC :
  ∀ (i_1 : (↑s : Type u_1)),
    Eq (α := MvPolynomial σ R)
      ((((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))))
                      (mapAlgHom (Polynomial.aeval f))).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])).comp
              CAlgHom :
            (a : MvPolynomial (↑s : Type u_1) R) → MvPolynomial σ R)
          (X i_1) :
        MvPolynomial σ R)
      (((AlgHom.comp
                (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]))
                CAlgHom :
              MvPolynomial.{u_1, u_2} (↑s : Type u_1) R →ₐ[R] MvPolynomial σ R) :
            (a : MvPolynomial (↑s : Type u_1) R) → MvPolynomial σ R)
          (X i_1) :
        MvPolynomial σ R)
⊢ ((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))))
              (mapAlgHom (Polynomial.aeval f))).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])).comp
      CAlgHom =
    AlgHom.comp
      (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]))
      CAlgHom

Tactic:
ext1