internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.smul_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
⊢ (r • f).toFun S t = (r • f.toFun S) 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
⊢ (r • f).toFun S t = (r • f.toFun S) t
Theorem: PolynomialMap.smul_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
⊢ (r • f).toFun S t = (r • f.toFun S) t
Tactic:
simp only [toFun_eq_toFunLifted_apply _ ha, smul_def, Pi.smul_apply, map_smul]
Proof state after:
no goals
Theorem: PolynomialMap.add_smul
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
⊢ (a + b) • f = a • f + b • f
Tactic:
ext S _ _ x
Proof state after:
case toFun'.h.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✝ : 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
x✝¹ : CommRing S
x✝ : Algebra R S
x : S ⊗[R] M
⊢ ((a + b) • f).toFun' S x = (a • f + b • f).toFun' S x
Theorem: PolynomialMap.add_smul
Proof state before:
case toFun'.h.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✝ : 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
x✝¹ : CommRing S
x✝ : Algebra R S
x : S ⊗[R] M
⊢ ((a + b) • f).toFun' S x = (a • f + b • f).toFun' S x
Tactic:
simp only [add_def, smul_def, _root_.add_smul]
Proof state after:
no goals
Theorem: PolynomialMap.zero_smul
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
⊢ 0 • f = 0
Tactic:
ext S _ _ x
Proof state after:
case toFun'.h.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✝ : 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
x✝¹ : CommRing S
x✝ : Algebra R S
x : S ⊗[R] M
⊢ (0 • f).toFun' S x = toFun' 0 S x
Theorem: PolynomialMap.zero_smul
Proof state before:
case toFun'.h.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✝ : 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
x✝¹ : CommRing S
x✝ : Algebra R S
x : S ⊗[R] M
⊢ (0 • f).toFun' S x = toFun' 0 S x
Tactic:
simp only [smul_def, _root_.zero_smul, zero_def, Pi.zero_apply]
Proof state after:
no goals
Theorem: PolynomialMap.one_smul
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
⊢ 1 • f = f
Tactic:
ext S _ _ x
Proof state after:
case toFun'.h.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✝ : 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
x✝¹ : CommRing S
x✝ : Algebra R S
x : S ⊗[R] M
⊢ (1 • f).toFun' S x = f.toFun' S x
Theorem: PolynomialMap.one_smul
Proof state before:
case toFun'.h.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✝ : 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
x✝¹ : CommRing S
x✝ : Algebra R S
x : S ⊗[R] M
⊢ (1 • f).toFun' S x = f.toFun' S x
Tactic:
simp only [smul_def, Pi.smul_apply, _root_.one_smul]
Proof state after:
no goals
Theorem: PolynomialMap.isCompat_apply'_ground
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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = f.toFun' S (1 ⊗ₜ[R] x)
Tactic:
simp only [ground]
Proof state after:
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : 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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun' R ∘ ⇑(TensorProduct.lid R M).symm) x = f.toFun' S (1 ⊗ₜ[R] x)
Theorem: PolynomialMap.isCompat_apply'_ground
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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun' R ∘ ⇑(TensorProduct.lid R M).symm) x = f.toFun' S (1 ⊗ₜ[R] x)
Tactic:
convert f.isCompat_apply' (algebraMap' R S) (1 ⊗ₜ[R] x)
Proof state after:
case h.e'_2
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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun' R ∘ ⇑(TensorProduct.lid R M).symm) x =
    (LinearMap.rTensor N (algebraMap' R S).toLinearMap) (f.toFun' R (1 ⊗ₜ[R] x))

case h.e'_3.h.e'_13
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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Theorem: PolynomialMap.isCompat_apply'_ground
Proof state before:
case h.e'_2
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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun' R ∘ ⇑(TensorProduct.lid R M).symm) x =
    (LinearMap.rTensor N (algebraMap' R S).toLinearMap) (f.toFun' R (1 ⊗ₜ[R] x))

case h.e'_3.h.e'_13
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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Tactic:
simp only [Function.comp_apply, TensorProduct.lid_symm_apply, TensorProduct.includeRight_lid]
Proof state after:
case h.e'_3.h.e'_13
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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Theorem: PolynomialMap.isCompat_apply'_ground
Proof state before:
case h.e'_3.h.e'_13
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
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Tactic:
rw [rTensor_tmul, toLinearMap_apply, map_one]
Proof state after:
no goals
Theorem: PolynomialMap.isCompat_apply_ground
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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = f.toFun S (1 ⊗ₜ[R] x)
Tactic:
simp only [ground, ← toFun_eq_toFun']
Proof state after:
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : 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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun R ∘ ⇑(TensorProduct.lid R M).symm) x = f.toFun S (1 ⊗ₜ[R] x)
Theorem: PolynomialMap.isCompat_apply_ground
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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun R ∘ ⇑(TensorProduct.lid R M).symm) x = f.toFun S (1 ⊗ₜ[R] x)
Tactic:
convert f.isCompat_apply (algebraMap' R S) (1 ⊗ₜ[R] x)
Proof state after:
case h.e'_2
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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun R ∘ ⇑(TensorProduct.lid R M).symm) x =
    (LinearMap.rTensor N (algebraMap' R S).toLinearMap) (f.toFun R (1 ⊗ₜ[R] x))

case h.e'_3.h.e'_13
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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Theorem: PolynomialMap.isCompat_apply_ground
Proof state before:
case h.e'_2
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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun R ∘ ⇑(TensorProduct.lid R M).symm) x =
    (LinearMap.rTensor N (algebraMap' R S).toLinearMap) (f.toFun R (1 ⊗ₜ[R] x))

case h.e'_3.h.e'_13
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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Tactic:
simp only [Function.comp_apply, TensorProduct.lid_symm_apply, TensorProduct.includeRight_lid]
Proof state after:
case h.e'_3.h.e'_13
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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Theorem: PolynomialMap.isCompat_apply_ground
Proof state before:
case h.e'_3.h.e'_13
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
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Tactic:
rw [rTensor_tmul, toLinearMap_apply, _root_.map_one]
Proof state after:
no goals
Theorem: PolynomialMap.comp_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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (g.comp f).toFun S = g.toFun S ∘ 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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t
Theorem: PolynomialMap.comp_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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) 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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
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
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t
Theorem: PolynomialMap.comp_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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
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
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t
Tactic:
have hb : PolynomialMap.π R N S ⟨s, f.toFun' _ p⟩ = f.toFun S t := by
  simp only [toFun_eq_toFunLifted_apply _ ha, π]
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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
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
hb : PolynomialMap.π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = f.toFun S t
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t
Theorem: PolynomialMap.comp_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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
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
hb : PolynomialMap.π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = f.toFun S t
⊢ (g.comp f).toFun S t = (g.toFun S ∘ f.toFun S) t
Tactic:
rw [Function.comp_apply, toFun_eq_toFunLifted_apply _ hb, toFun_eq_toFunLifted_apply _ ha,
  comp_toFun', Function.comp_apply]
Proof state after:
no goals
Theorem: PolynomialMap.comp_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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
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
⊢ PolynomialMap.π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = f.toFun S t
Tactic:
simp only [toFun_eq_toFunLifted_apply _ ha, π]
Proof state after:
no goals
Theorem: PolynomialMap.comp_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
P : Type u_5
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
Q : Type u_6
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
S : Type u_7
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (g.comp f).toFun S m = g.toFun S (f.toFun S m)
Tactic:
simp only [comp_toFun, Function.comp_apply]
Proof state after:
no goals