-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
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)
⊢ 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)
have 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')) sorry;
  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) sorry) ∘
        (⇑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)
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]