-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
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])
⊢ 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)
have 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)))))))
Tactic: simp only [AlgHom.coe_comp, Subalgebra.coe_val,
      AlgEquiv.coe_algHom, AlgEquiv.coe_trans, Function.comp_assoc, u]