-- 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
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst_9 : CommSemiring T
inst_10 : Algebra R T
B : Type u
inst_11 : CommSemiring B
inst_12 : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : AlgHom.{u, v, w} R ↥φ.range ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  Eq (α := TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M (h'.comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
θ : RingCon.Quotient (RingCon.ker (↑φ : A →+* S)) →ₐ[R] RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) :=
  (↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
    (h'.comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range))
ht :
  (h.comp φ.range.val).comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range) =
    ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).comp θ)
h₁ :
  Eq (α := TensorProduct.{u, w, u_2} R (↥ψ.range) N)
    ((rTensor N (↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).toLinearMap :
          (a : (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] N) → ↥ψ.range ⊗[R] N)
        (f.toFun' (RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)))
          ((rTensor M θ.toLinearMap :
              (a : (RingCon.ker (↑φ : A →+* S)).Quotient ⊗[R] M) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] M)
            ((rTensor M (toLinearMap (mkₐ R (RingCon.ker (↑φ : A →+* S)))) :
                (a : A ⊗[R] M) → (RingCon.ker (↑φ : A →+* S)).Quotient ⊗[R] M)
              p))) :
      TensorProduct.{u, w, u_2} R (↥ψ.range) N)
    ((rTensor N (↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).toLinearMap :
          (a : (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] N) → ↥ψ.range ⊗[R] N)
        (f.toFun' (RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)))
          ((rTensor M (toLinearMap (mkₐ R (RingCon.ker (↑ψ : B →+* T)))) :
              (a : B ⊗[R] M) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] M)
            q)) :
      TensorProduct.{u, w, u_2} R (↥ψ.range) N)
⊢ Eq (α := TensorProduct.{u, w, u_2} R (↥ψ.range) N)
    ((rTensor N (↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).toLinearMap :
          (a : (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] N) → ↥ψ.range ⊗[R] N)
        ((rTensor N θ.toLinearMap :
            (a : (RingCon.ker (↑φ : A →+* S)).Quotient ⊗[R] N) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] N)
          ((rTensor N (toLinearMap (mkₐ R (RingCon.ker (↑φ : A →+* S)))) :
              (a : A ⊗[R] N) → (RingCon.ker (↑φ : A →+* S)).Quotient ⊗[R] N)
            (f.toFun' A p))) :
      TensorProduct.{u, w, u_2} R (↥ψ.range) N)
    ((rTensor N (↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).toLinearMap :
          (a : (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] N) → ↥ψ.range ⊗[R] N)
        ((rTensor N (toLinearMap (mkₐ R (RingCon.ker (↑ψ : B →+* T)))) :
            (a : B ⊗[R] N) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] N)
          (f.toFun' B q)) :
      TensorProduct.{u, w, u_2} R (↥ψ.range) N)

Tactic:
rw [← rTensor_comp_apply, ← AlgHom.comp_toLinearMap, isCompat_apply',
    isCompat_apply', AlgHom.comp_toLinearMap, rTensor_comp_apply,
    isCompat_apply']

Premises used: AlgHom.comp_toLinearMap, LinearMap.rTensor_comp_apply, PolynomialLaw.isCompat_apply'