-- 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)
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])
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])
simp :
  Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (Function.comp (β := 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.comp (β := MvPolynomial.{u_1, u_2} (Option (↑s : Type u_1)) R)
        (⇑(optionEquivRight R (↑s : Type u_1)) :
          (a : MvPolynomial (Option (↑s : Type u_1)) R) → MvPolynomial (↑s : Type u_1) R[X])
        (⇑(AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) :
          (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial (Option (↑s : Type u_1)) R)))
⊢ Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β := ↥(supported R (insert i s)))
    (Function.comp (β := MvPolynomial.{u_1, u_2} { i_1 : σ // i_1 ∈ insert i s } R)
      (⇑(AlgEquiv.symm (supportedEquivMvPolynomial (insert i s))) :
        (a : MvPolynomial { i_1 : σ // i_1 ∈ insert i s } R) → ↥(supported R (insert i s)))
      (Function.comp (β := MvPolynomial.{u_1, u_2} (Option (↑s : Type u_1)) R)
        (⇑(renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm) :
          (a : MvPolynomial (Option (↑s : Type u_1)) R) → MvPolynomial { i_1 : σ // i_1 ∈ insert i s } R)
        (Function.comp (β := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
          (⇑(AlgEquiv.symm (optionEquivRight R (↑s : Type u_1))) :
            (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (Option (↑s : Type u_1)) R)
          (Function.comp (β := 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.comp (β := MvPolynomial.{u_1, u_2} (Option (↑s : Type u_1)) R)
              (⇑(optionEquivRight R (↑s : Type u_1)) :
                (a : MvPolynomial (Option (↑s : Type u_1)) R) → MvPolynomial (↑s : Type u_1) R[X])
              (⇑(AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) :
                (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial (Option (↑s : Type u_1)) R))))))

Tactic:
simp only [EquivLike.comp_injective]

Premises used: EquivLike.comp_injective