Theorem: PolynomialMap.isCompat_apply (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
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
State after:
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
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)

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
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
let s' := s.image h
State after:
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
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)

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
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
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⟩)
State after:
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 ⋯
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)

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 ⋯
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
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
State after:
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
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)

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
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
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]
State after:
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)
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)

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)
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
let p' := rTensor M (rename j).toLinearMap  p
State after:
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
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)

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
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
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]
State after:
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.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)

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.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
rw [toFun_eq_toFunLifted_apply f ha, toFun_eq_toFunLifted_apply f ha', ← LinearMap.comp_apply,
  ← rTensor_comp, ← comp_toLinearMap]
State after:
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')

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

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
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
⊢ ∀ (x : ↥(PolynomialMap.φ R s).range), (h.comp (PolynomialMap.φ R s).range.val) x ∈ (PolynomialMap.φ R s').range
Tactic:
rintro ⟨x, hx⟩
State after:
case 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
x : S
hx : x ∈ (PolynomialMap.φ R s).range
⊢ (h.comp (PolynomialMap.φ R s).range.val) ⟨x, hx⟩ ∈ (PolynomialMap.φ R s').range

State before:
case 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
x : S
hx : x ∈ (PolynomialMap.φ R s).range
⊢ (h.comp (PolynomialMap.φ R s).range.val) ⟨x, hx⟩ ∈ (PolynomialMap.φ R s').range
Tactic:
simp only [φ_range] at hx ⊢
State after:
case 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
x : S
hx✝ : x ∈ (PolynomialMap.φ R s).range
hx : x ∈ Algebra.adjoin R ↑s
⊢ (h.comp (PolynomialMap.φ R s).range.val) ⟨x, hx✝⟩ ∈ Algebra.adjoin R ↑s'

State before:
case 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
x : S
hx✝ : x ∈ (PolynomialMap.φ R s).range
hx : x ∈ Algebra.adjoin R ↑s
⊢ (h.comp (PolynomialMap.φ R s).range.val) ⟨x, hx✝⟩ ∈ Algebra.adjoin R ↑s'
Tactic:
simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
  Algebra.adjoin_image, s']
State after:
case 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
x : S
hx✝ : x ∈ (PolynomialMap.φ R s).range
hx : x ∈ Algebra.adjoin R ↑s
⊢ h x ∈ Subalgebra.map h (Algebra.adjoin R ↑s)

State before:
case 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
x : S
hx✝ : x ∈ (PolynomialMap.φ R s).range
hx : x ∈ Algebra.adjoin R ↑s
⊢ h x ∈ Subalgebra.map h (Algebra.adjoin R ↑s)
Tactic:
exact ⟨x, hx, rfl⟩
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
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
⊢ (PolynomialMap.φ R s').comp (rename j) = h.comp (PolynomialMap.φ R s)
Tactic:
ext p
State after:
case hf
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
p : Fin s.card
⊢ ((PolynomialMap.φ R s').comp (rename j)) (X p) = (h.comp (PolynomialMap.φ R s)) (X p)

State before:
case hf
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
p : Fin s.card
⊢ ((PolynomialMap.φ R s').comp (rename j)) (X p) = (h.comp (PolynomialMap.φ R s)) (X p)
Tactic:
simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]
State after:
case hf
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
p : Fin s.card
⊢ (aeval ((fun n => ↑(s'.equivFin.symm n)) ∘ j)) (X p) = (aeval fun i => h ↑(s.equivFin.symm i)) (X p)

State before:
case hf
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
p : Fin s.card
⊢ (aeval ((fun n => ↑(s'.equivFin.symm n)) ∘ j)) (X p) = (aeval fun i => h ↑(s.equivFin.symm i)) (X p)
Tactic:
congr
State after:
case hf.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
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
p : Fin s.card
⊢ (fun n => ↑(s'.equivFin.symm n)) ∘ j = fun i => h ↑(s.equivFin.symm i)

State before:
case hf.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
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
p : Fin s.card
⊢ (fun n => ↑(s'.equivFin.symm n)) ∘ j = fun i => h ↑(s.equivFin.symm i)
Tactic:
ext n
State after:
case hf.e_a.e_f.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
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
p n : Fin s.card
⊢ ((fun n => ↑(s'.equivFin.symm n)) ∘ j) n = h ↑(s.equivFin.symm n)

State before:
case hf.e_a.e_f.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
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
p n : Fin s.card
⊢ ((fun n => ↑(s'.equivFin.symm n)) ∘ j) n = h ↑(s.equivFin.symm n)
Tactic:
simp only [Function.comp_apply, Equiv.symm_apply_apply, j]
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
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
⊢ PolynomialMap.π R M T ⟨s', p'⟩ = (LinearMap.rTensor M h.toLinearMap) t
Tactic:
simp only [← ha, π, p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, eq_h_comp]
State after:
no goals

State before:
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
Tactic:
ext x
State after:
case intro.mk.hh'.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
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
x : ↥(PolynomialMap.φ R s).range
⊢ ((PolynomialMap.φ R s').range.val.comp h') x = (h.comp (PolynomialMap.φ R s).range.val) x

State before:
case intro.mk.hh'.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
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
x : ↥(PolynomialMap.φ R s).range
⊢ ((PolynomialMap.φ R s').range.val.comp h') x = (h.comp (PolynomialMap.φ R s).range.val) x
Tactic:
simp only [val_comp_codRestrict, AlgHom.coe_comp, Subalgebra.coe_val,Function.comp_apply, h']
State after:
no goals

State before:
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'
Tactic:
simp only [p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
State after:
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.comp (rename j)).toLinearMap) p

State before:
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.comp (rename j)).toLinearMap) p
Tactic:
apply LinearMap.congr_fun
State after:
case intro.mk.hpq.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
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 =
    LinearMap.rTensor M ((PolynomialMap.φ R s').rangeRestrict.comp (rename j)).toLinearMap

State before:
case intro.mk.hpq.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
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 =
    LinearMap.rTensor M ((PolynomialMap.φ R s').rangeRestrict.comp (rename j)).toLinearMap
Tactic:
apply congr_arg
State after:
case intro.mk.hpq.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
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
⊢ (h'.comp (PolynomialMap.φ R s).rangeRestrict).toLinearMap =
    ((PolynomialMap.φ R s').rangeRestrict.comp (rename j)).toLinearMap

State before:
case intro.mk.hpq.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
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
⊢ (h'.comp (PolynomialMap.φ R s).rangeRestrict).toLinearMap =
    ((PolynomialMap.φ R s').rangeRestrict.comp (rename j)).toLinearMap
Tactic:
apply congr_arg
State after:
case intro.mk.hpq.h.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
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
⊢ h'.comp (PolynomialMap.φ R s).rangeRestrict = (PolynomialMap.φ R s').rangeRestrict.comp (rename j)

State before:
case intro.mk.hpq.h.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
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
⊢ h'.comp (PolynomialMap.φ R s).rangeRestrict = (PolynomialMap.φ R s').rangeRestrict.comp (rename j)
Tactic:
ext n
State after:
case intro.mk.hpq.h.h.h.hf.a
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
n : Fin s.card
⊢ ↑((h'.comp (PolynomialMap.φ R s).rangeRestrict) (X n)) =
    ↑(((PolynomialMap.φ R s').rangeRestrict.comp (rename j)) (X n))

State before:
case intro.mk.hpq.h.h.h.hf.a
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
n : Fin s.card
⊢ ↑((h'.comp (PolynomialMap.φ R s).rangeRestrict) (X n)) =
    ↑(((PolynomialMap.φ R s').rangeRestrict.comp (rename j)) (X n))
Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply, coe_codRestrict,
  Subalgebra.coe_val, rename_X, h', j]
State after:
case intro.mk.hpq.h.h.h.hf.a
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
n : Fin s.card
⊢ h ((PolynomialMap.φ R s) (X n)) = (PolynomialMap.φ R s') (X (s'.equivFin ⟨h ↑(s.equivFin.symm n), ⋯⟩))

State before:
case intro.mk.hpq.h.h.h.hf.a
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
n : Fin s.card
⊢ h ((PolynomialMap.φ R s) (X n)) = (PolynomialMap.φ R s') (X (s'.equivFin ⟨h ↑(s.equivFin.symm n), ⋯⟩))
Tactic:
simp only [φ, aeval_X, Equiv.symm_apply_apply]
State after:
no goals