Theorem: PolynomialMap.toFunLifted_factorsThrough_π (DividedPowers/PolynomialMap/Basic.lean)

State before:
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
⊢ Function.FactorsThrough (PolynomialMap.toFunLifted f) (PolynomialMap.π R M S)
Tactic:
rintro ⟨s, p⟩ ⟨s', p'⟩ h
State after:
case mk.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
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'⟩
⊢ PolynomialMap.toFunLifted f ⟨s, p⟩ = PolynomialMap.toFunLifted f ⟨s', p'⟩

State before:
case mk.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
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'⟩
⊢ PolynomialMap.toFunLifted f ⟨s, p⟩ = PolynomialMap.toFunLifted f ⟨s', p'⟩
Tactic:
simp only [toFunLifted]
State after:
case mk.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
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'⟩
⊢ (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')

State before:
case mk.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
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'⟩
⊢ (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:
set u := rTensor M (φ R s).rangeRestrict.toLinearMap p with hu
State after:
case mk.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
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
⊢ (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')

State before:
case mk.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
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
⊢ (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 uFG : Subalgebra.FG (R := R) (φ R s).range := by
  rw [← Algebra.map_top]
  exact Subalgebra.FG.map _ (Algebra.FiniteType.mvPolynomial R (Fin s.card)).out
State after:
case mk.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
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
⊢ (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')

State before:
case mk.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
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
⊢ (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:
set u' := rTensor M (φ R s').rangeRestrict.toLinearMap p' with hu'
State after:
case mk.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
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'
⊢ (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')

State before:
case mk.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
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'
⊢ (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 u'FG : Subalgebra.FG (R := R) (φ R s').range := by
  rw [← Algebra.map_top]
  exact Subalgebra.FG.map _ (Algebra.FiniteType.mvPolynomial R (Fin s'.card)).out
State after:
case mk.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
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
⊢ (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')

State before:
case mk.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
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
⊢ (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 huu' : rTensor M (Subalgebra.val _).toLinearMap u =
  rTensor M (Subalgebra.val _).toLinearMap u' := by
  simp only [π] at h
  simp only [hu, hu', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap,
    comp_rangeRestrict, h]
State after:
case mk.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
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'
⊢ (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')

State before:
case mk.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
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'
⊢ (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:
obtain ⟨B, hAB, hA'B, hB, h⟩ :=
  TensorProduct.Algebra.eq_of_fg_of_subtype_eq' (R := R) uFG u u'FG u' huu'
State after:
case mk.mk.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
hB : B.FG
h :
  (LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u =
    (LinearMap.rTensor M (Subalgebra.inclusion hA'B).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')

State before:
case mk.mk.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
hB : B.FG
h :
  (LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u =
    (LinearMap.rTensor M (Subalgebra.inclusion hA'B).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')
Tactic:
obtain ⟨t, hB⟩ := hB
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 : Algebra.adjoin R ↑t = B
⊢ (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')

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 : Algebra.adjoin R ↑t = B
⊢ (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:
rw [← φ_range R t, eq_comm] at hB
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
⊢ (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')

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
⊢ (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 hAB' : (φ R s).range ≤ (φ R t).range := le_trans hAB (le_of_eq hB)
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
⊢ (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')

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
⊢ (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 hA'B' : (φ R s').range ≤ (φ R t).range := le_trans hA'B (le_of_eq hB)
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
⊢ (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')

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 _) _
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')

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
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')
Tactic:
obtain ⟨q, hq⟩ := this
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 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')

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 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:
rw [toFun'_eq_of_inclusion f p q hAB', toFun'_eq_of_inclusion f p' q hA'B']
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').comp (PolynomialMap.φ R s').rangeRestrict).toLinearMap) p' =
    (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q

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 hAB').comp (PolynomialMap.φ R s).rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q

State before:
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
⊢ (PolynomialMap.φ R s).range.FG
Tactic:
rw [← Algebra.map_top]
State after:
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
⊢ (Subalgebra.map (PolynomialMap.φ R s) ⊤).FG

State before:
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
⊢ (Subalgebra.map (PolynomialMap.φ R s) ⊤).FG
Tactic:
exact Subalgebra.FG.map _ (Algebra.FiniteType.mvPolynomial R (Fin s.card)).out
State after:
no goals

State before:
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'
⊢ (PolynomialMap.φ R s').range.FG
Tactic:
rw [← Algebra.map_top]
State after:
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'
⊢ (Subalgebra.map (PolynomialMap.φ R s') ⊤).FG

State before:
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'
⊢ (Subalgebra.map (PolynomialMap.φ R s') ⊤).FG
Tactic:
exact Subalgebra.FG.map _ (Algebra.FiniteType.mvPolynomial R (Fin s'.card)).out
State after:
no goals

State before:
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
⊢ (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
Tactic:
simp only [π] at h
State after:
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 :
  (LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p =
    (LinearMap.rTensor M (PolynomialMap.φ R s').toLinearMap) 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
⊢ (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'

State before:
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 :
  (LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p =
    (LinearMap.rTensor M (PolynomialMap.φ R s').toLinearMap) 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
⊢ (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
Tactic:
simp only [hu, hu', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap,
  comp_rangeRestrict, h]
State after:
no goals

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]
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)

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').toLinearMap)
      ((LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p') =
    (LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap)
      ((LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u)
Tactic:
rw [← hu', h]
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) u' =
    (LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap)
      ((LinearMap.rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u')

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').toLinearMap) u' =
    (LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap)
      ((LinearMap.rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u')
Tactic:
simp only [← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
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) u' =
    (LinearMap.rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hA'B)).toLinearMap) u'

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').toLinearMap) u' =
    (LinearMap.rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hA'B)).toLinearMap) u'
Tactic:
congr
State after:
no goals

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 hAB').comp (PolynomialMap.φ R s).rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q
Tactic:
simp only [hq, hu, ← LinearMap.comp_apply, comp_toLinearMap, rTensor_comp]
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 hAB').toLinearMap ∘ₗ
        LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap)
      p =
    ((LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ
          LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) ∘ₗ
        LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap)
      p

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 hAB').toLinearMap ∘ₗ
        LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap)
      p =
    ((LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ
          LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) ∘ₗ
        LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap)
      p
Tactic:
congr
State after:
case mk.mk.intro.intro.intro.intro.intro.intro.e_a.e_f
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 hAB').toLinearMap =
    LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ
      LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap

State before:
case mk.mk.intro.intro.intro.intro.intro.intro.e_a.e_f
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 hAB').toLinearMap =
    LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ
      LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap
Tactic:
ext
State after:
case mk.mk.intro.intro.intro.intro.intro.intro.e_a.e_f.a.h.h
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
x✝¹ : ↥(PolynomialMap.φ R s).range
x✝ : M
⊢ ((TensorProduct.AlgebraTensorModule.curry (LinearMap.rTensor M (Subalgebra.inclusion hAB').toLinearMap)) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
          (LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ
            LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap))
        x✝¹)
      x✝

State before:
case mk.mk.intro.intro.intro.intro.intro.intro.e_a.e_f.a.h.h
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
x✝¹ : ↥(PolynomialMap.φ R s).range
x✝ : M
⊢ ((TensorProduct.AlgebraTensorModule.curry (LinearMap.rTensor M (Subalgebra.inclusion hAB').toLinearMap)) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
          (LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ
            LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap))
        x✝¹)
      x✝
Tactic:
rfl
State after:
no goals