Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk.intro.intro.intro.intro.intro.intro
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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
huu' :
  (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (PolynomialMap.φ R s).range ≤ B
hA'B : (PolynomialMap.φ R s').range ≤ B
h :
  (LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u =
    (LinearMap.rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (PolynomialMap.φ R t).range
hAB' : (PolynomialMap.φ R s).range ≤ (PolynomialMap.φ R t).range
hA'B' : (PolynomialMap.φ R s').range ≤ (PolynomialMap.φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q =
    (LinearMap.rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (LinearMap.rTensor M ((Subalgebra.inclusion hA'B').comp (PolynomialMap.φ R s').rangeRestrict).toLinearMap) p' =
    (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q
Tactic:
simp only [hq, comp_toLinearMap, rTensor_comp, LinearMap.comp_apply]
Proof state after:
case mk.mk.intro.intro.intro.intro.intro.intro
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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
huu' :
  (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (PolynomialMap.φ R s).range ≤ B
hA'B : (PolynomialMap.φ R s').range ≤ B
h :
  (LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u =
    (LinearMap.rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (PolynomialMap.φ R t).range
hAB' : (PolynomialMap.φ R s).range ≤ (PolynomialMap.φ R t).range
hA'B' : (PolynomialMap.φ R s').range ≤ (PolynomialMap.φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q =
    (LinearMap.rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (LinearMap.rTensor M (Subalgebra.inclusion hA'B').toLinearMap)
      ((LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p') =
    (LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap)
      ((LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u)