Theorem: PolynomialMap.isCompat_apply
Proof state before:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(PolynomialMap.φ R s).range →ₐ[R] ↥(PolynomialMap.φ R s').range :=
  (h.comp (PolynomialMap.φ R s).range.val).codRestrict (PolynomialMap.φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (PolynomialMap.φ R s').comp (rename j) = h.comp (PolynomialMap.φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := (LinearMap.rTensor M (rename j).toLinearMap) p
ha' : PolynomialMap.π R M T ⟨s', p'⟩ = (LinearMap.rTensor M h.toLinearMap) t
⊢ (LinearMap.rTensor N (h.comp (PolynomialMap.φ R s)).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Tactic:
apply toFun'_eq_of_diagram f p p' h h'
Proof state after:
case intro.mk.hh'
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(PolynomialMap.φ R s).range →ₐ[R] ↥(PolynomialMap.φ R s').range :=
  (h.comp (PolynomialMap.φ R s).range.val).codRestrict (PolynomialMap.φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (PolynomialMap.φ R s').comp (rename j) = h.comp (PolynomialMap.φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := (LinearMap.rTensor M (rename j).toLinearMap) p
ha' : PolynomialMap.π R M T ⟨s', p'⟩ = (LinearMap.rTensor M h.toLinearMap) t
⊢ (PolynomialMap.φ R s').range.val.comp h' = h.comp (PolynomialMap.φ R s).range.val

case intro.mk.hpq
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(PolynomialMap.φ R s).range →ₐ[R] ↥(PolynomialMap.φ R s').range :=
  (h.comp (PolynomialMap.φ R s).range.val).codRestrict (PolynomialMap.φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (PolynomialMap.φ R s').comp (rename j) = h.comp (PolynomialMap.φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := (LinearMap.rTensor M (rename j).toLinearMap) p
ha' : PolynomialMap.π R M T ⟨s', p'⟩ = (LinearMap.rTensor M h.toLinearMap) t
⊢ (LinearMap.rTensor M (h'.comp (PolynomialMap.φ R s).rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'