internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.isCompat_apply
Proof 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]
Proof 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
Theorem: PolynomialMap.isCompat_apply
Proof 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
Proof 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
Theorem: PolynomialMap.isCompat_apply
Proof 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
Proof 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
Theorem: PolynomialMap.isCompat_apply
Proof 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
Proof 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)
Theorem: PolynomialMap.isCompat_apply
Proof 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
Proof 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))
Theorem: PolynomialMap.isCompat_apply
Proof 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]
Proof 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), ⋯⟩))
Theorem: PolynomialMap.isCompat_apply
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.isCompat
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
⊢ ⇑(LinearMap.rTensor N h.toLinearMap) ∘ f.toFun S = f.toFun T ∘ ⇑(LinearMap.rTensor M h.toLinearMap)
Tactic:
ext t
Proof state after:
case 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
⊢ (⇑(LinearMap.rTensor N h.toLinearMap) ∘ f.toFun S) t = (f.toFun T ∘ ⇑(LinearMap.rTensor M h.toLinearMap)) t
Theorem: PolynomialMap.isCompat
Proof state before:
case 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
⊢ (⇑(LinearMap.rTensor N h.toLinearMap) ∘ f.toFun S) t = (f.toFun T ∘ ⇑(LinearMap.rTensor M h.toLinearMap)) t
Tactic:
simp only [Function.comp_apply, PolynomialMap.isCompat_apply]
Proof state after:
no goals
Theorem: PolynomialMap.zero_toFun
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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ toFun 0 S = 0
Tactic:
ext t
Proof state after:
case 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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ toFun 0 S t = 0 t
Theorem: PolynomialMap.zero_toFun
Proof state before:
case 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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ toFun 0 S t = 0 t
Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
Proof state after:
case h.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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ toFun 0 S t = 0 t
Theorem: PolynomialMap.zero_toFun
Proof state before:
case h.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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ toFun 0 S t = 0 t
Tactic:
simp only [toFun_eq_toFunLifted_apply _ ha, zero_def, Pi.zero_apply, map_zero]
Proof state after:
no goals
Theorem: PolynomialMap.add_toFun_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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ (f + g).toFun S t = f.toFun S t + g.toFun S t
Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ (f + g).toFun S t = f.toFun S t + g.toFun S t
Theorem: PolynomialMap.add_toFun_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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ (f + g).toFun S t = f.toFun S t + g.toFun S t
Tactic:
simp only [Pi.add_apply, toFun_eq_toFunLifted_apply _ ha, add_def, map_add]
Proof state after:
no goals
Theorem: PolynomialMap.add_toFun
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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (f + g).toFun S = f.toFun S + g.toFun S
Tactic:
ext t
Proof state after:
case 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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ (f + g).toFun S t = (f.toFun S + g.toFun S) t
Theorem: PolynomialMap.add_toFun
Proof state before:
case 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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ (f + g).toFun S t = (f.toFun S + g.toFun S) t
Tactic:
simp only [Pi.add_apply, add_toFun_apply]
Proof state after:
no goals
Theorem: PolynomialMap.smul_toFun
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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (r • f).toFun S = r • f.toFun S
Tactic:
ext t
Proof state after:
case 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✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
r a b : R
f g : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ (r • f).toFun S t = (r • f.toFun S) t