-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h_1 :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
huu' :
  Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s)))) : (a : ↥(φ R s).range ⊗[R] M) → S ⊗[R] M) u :
      S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s')))) : (a : ↥(φ R s').range ⊗[R] M) → S ⊗[R] M) u' :
      S ⊗[R] M)
B : Subalgebra R S
hAB : AlgHom.range (φ R s) ≤ B
hA'B : AlgHom.range (φ R s') ≤ B
h :
  Eq (α := TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥(φ R s).range ⊗[R] M) → ↥B ⊗[R] M) u :
      TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥(φ R s').range ⊗[R] M) → ↥B ⊗[R] M) u' :
      TensorProduct.{u, v, u_1} R (↥B) M)
t : Finset S
hB : B = AlgHom.range (φ R t)
hAB' : LE.le (α := Subalgebra R S) (AlgHom.range (φ R s)) (AlgHom.range (φ R t))
hA'B' : LE.le (α := Subalgebra R S) (AlgHom.range (φ R s')) (AlgHom.range (φ R t))
this :
  ∃ (q : MvPolynomial (Fin t.card) R ⊗[R] M),
    Eq (α := TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)
      ((rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R t))) :
            (a : MvPolynomial (Fin t.card) R ⊗[R] M) → ↥(φ R t).range ⊗[R] M)
          q :
        TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)
      ((rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap :
            (a : ↥(φ R s).range ⊗[R] M) → ↥(φ R t).range ⊗[R] M)
          u :
        TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)
obtain :
  ∀ (q : MvPolynomial (Fin t.card) R ⊗[R] M)
    (hq :
      Eq (α := TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)
        ((rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R t))) :
              (a : MvPolynomial (Fin t.card) R ⊗[R] M) → ↥(φ R t).range ⊗[R] M)
            q :
          TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)
        ((rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap :
              (a : ↥(φ R s).range ⊗[R] M) → ↥(φ R t).range ⊗[R] M)
            u :
          TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)),
    Eq (α := S ⊗[R] N)
      ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
          (f.toFun' (MvPolynomial (Fin s.card) R) p) :
        S ⊗[R] N)
      ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → S ⊗[R] N)
          (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
        S ⊗[R] N)
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      S ⊗[R] N)

Tactic:
obtain ⟨q, hq⟩ := this