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