-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
obtain :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
      (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
obtain₁ obtain₂ obtain₃ :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
      (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
obtain₄ obtain₅ :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    let s' : Finset T := Finset.image (⇑h : (a : S) → T) s;
    let h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
      AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯;
    let j : Fin s.card → Fin s'.card :=
      Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
        ((fun (x : ↥s) ↦
            match (motive := ↥s → ↥s') x with
            | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
          (⇑s.equivFin.symm : (a : Fin s.card) → ↥s));
    ∀ (eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)),
      Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
        (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
obtain₆ :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    let s' : Finset T := Finset.image (⇑h : (a : S) → T) s;
    let h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
      AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯;
    let j : Fin s.card → Fin s'.card :=
      Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
        ((fun (x : ↥s) ↦
            match (motive := ↥s → ↥s') x with
            | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
          (⇑s.equivFin.symm : (a : Fin s.card) → ↥s));
    ∀ (eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)),
      let p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
        (rTensor M (toLinearMap (rename j)) :
            (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
          p;
      ∀
        (ha' :
          Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
            ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)),
        Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
          (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
obtain₇ :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    let s' : Finset T := Finset.image (⇑h : (a : S) → T) s;
    let h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
      AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯;
    let j : Fin s.card → Fin s'.card :=
      Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
        ((fun (x : ↥s) ↦
            match (motive := ↥s → ↥s') x with
            | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
          (⇑s.equivFin.symm : (a : Fin s.card) → ↥s));
    ∀ (eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)),
      let p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
        (rTensor M (toLinearMap (rename j)) :
            (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
          p;
      ∀
        (ha' :
          Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
            ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)),
        Eq (α := T ⊗[R] N)
          ((rTensor N (h.comp (φ R s)).toLinearMap : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → T ⊗[R] N)
              (f.toFun' (MvPolynomial (Fin s.card) R) p) :
            T ⊗[R] N)
          ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → T ⊗[R] N)
              (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
            T ⊗[R] N)
hh' :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    let s' : Finset T := Finset.image (⇑h : (a : S) → T) s;
    let h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
      AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯;
    let j : Fin s.card → Fin s'.card :=
      Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
        ((fun (x : ↥s) ↦
            match (motive := ↥s → ↥s') x with
            | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
          (⇑s.equivFin.symm : (a : Fin s.card) → ↥s));
    ∀ (eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)),
      let p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
        (rTensor M (toLinearMap (rename j)) :
            (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
          p;
      ∀
        (ha' :
          Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
            ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)),
        AlgHom.comp (Subalgebra.val (AlgHom.range (φ R s'))) h' = h.comp (Subalgebra.val (AlgHom.range (φ R s)))
hpq hpq₁ :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    let s' : Finset T := Finset.image (⇑h : (a : S) → T) s;
    let h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
      AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯;
    let j : Fin s.card → Fin s'.card :=
      Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
        ((fun (x : ↥s) ↦
            match (motive := ↥s → ↥s') x with
            | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
          (⇑s.equivFin.symm : (a : Fin s.card) → ↥s));
    ∀ (eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)),
      let p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
        (rTensor M (toLinearMap (rename j)) :
            (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
          p;
      ∀
        (ha' :
          Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
            ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)),
        Eq (α := TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
          ((rTensor M (h'.comp (AlgHom.rangeRestrict (φ R s))).toLinearMap :
                (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
              p :
            TensorProduct.{u, w, 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' :
            TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
⊢ Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)

Tactic:
classical
  obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
  let s' := s.image h
  let h' : (φ R s).range →ₐ[R] (φ R s').range :=
    (h.comp (Subalgebra.val _)).codRestrict (φ R s').range (by
    rintro ⟨x, hx⟩
    simp only [range_φ] at hx ⊢
    simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
      Algebra.adjoin_image, s']
    exact ⟨x, hx, rfl⟩)
  let j : Fin s.card → Fin s'.card :=
    (s'.equivFin) ∘ (fun ⟨x, hx⟩ ↦ ⟨h x, Finset.mem_image_of_mem h hx⟩) ∘ (s.equivFin).symm
  have eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s) := by
    ext p
    simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]
    congr
    ext n
    simp only [Function.comp_apply, Equiv.symm_apply_apply, j]
  let p' := rTensor M (rename j).toLinearMap p
  have ha' : π R M T (⟨s', p'⟩ : lifts R M T) = rTensor M h.toLinearMap t := by
    simp only [← ha, π, p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, eq_h_comp]
  rw [toFun_eq_rTensor_φ_toFun' f ha, toFun_eq_rTensor_φ_toFun' f ha', ← LinearMap.comp_apply,
    ← rTensor_comp, ← comp_toLinearMap]
  apply toFun'_eq_of_diagram f p p' h h'
  · simp only [val_comp_codRestrict, h']
  · simp only [p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    congr
    ext n
    simp only [AlgHom.coe_comp, Function.comp_apply, coe_codRestrict,
      Subalgebra.coe_val, rename_X, h', j]
    simp only [φ, aeval_X, Equiv.symm_apply_apply]

Premises used: AlgHom.val_comp_codRestrict, AlgHom.comp_toLinearMap, MvPolynomial.aeval_X, Equiv.symm_apply_apply, LinearMap.comp_apply, PolynomialLaw.π_surjective, Subalgebra.coe_val, AlgHom.coe_comp, PolynomialLaw.φ, LinearMap.rTensor_comp, MvPolynomial.rename_X, Function.comp_apply, AlgHom.coe_codRestrict