-- 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 σ R)
    (Function.comp (β := ↥(supported R (insert i s)))
      (Subtype.val (p := fun (x : MvPolynomial σ R) ↦
        Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R (insert i s)) x))
      (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)))))))
⊢ 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)

Tactic:
simp only [AlgHom.coe_comp, Subalgebra.coe_val,
      AlgEquiv.coe_algHom, AlgEquiv.coe_trans, Function.comp_assoc, u]

Premises used: Subalgebra.coe_val, AlgHom.coe_comp, AlgEquiv.coe_algHom, AlgEquiv.coe_trans, Function.comp_assoc