Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk.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
⊢ (LinearMap.rTensor N (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:
have : ∃ q : MvPolynomial (Fin t.card) R ⊗[R] M, rTensor M (toLinearMap (φ R t).rangeRestrict) q =
    rTensor M ((Subalgebra.inclusion (le_of_eq hB)).comp
      (Subalgebra.inclusion hAB)).toLinearMap u :=
  rTensor_surjective _ (rangeRestrict_surjective _) _
Proof state after:
case mk.mk.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
this :
  ∃ q,
    (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q =
      (LinearMap.rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (LinearMap.rTensor N (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')