internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.componentIsHomogeneous
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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) =
    lift ((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯))
Tactic:
apply lift.unique
Proof state after:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ∀ (x : S) (y : M),
    (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) (x ⊗ₜ[R] y) =
      (((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯)) x) y
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ∀ (x : S) (y : M),
    (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) (x ⊗ₜ[R] y) =
      (((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯)) x) y
Tactic:
intro r m
Proof state after:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
r : S
m : M
⊢ (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) (r ⊗ₜ[R] m) =
    (((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯)) r) m
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
r : S
m : M
⊢ (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) (r ⊗ₜ[R] m) =
    (((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯)) r) m
Tactic:
simp only [coe_restrictScalars, IsLinearMap.mk'_apply, compl₂_id, coe_comp, Function.comp_apply,
  mk_apply, smul_tmul', smul_eq_mul]
Proof state after:
no goals
Theorem: PolynomialMap.componentIsHomogeneous
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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Tactic:
simp only [this, ← rTensor_comp_apply]
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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ (LinearMap.rTensor M (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm =
    (LinearMap.rTensor M (ψ.toLinearMap ∘ₗ ↑R (monomial 1))) sm
Theorem: PolynomialMap.componentIsHomogeneous
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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ (LinearMap.rTensor M (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm =
    (LinearMap.rTensor M (ψ.toLinearMap ∘ₗ ↑R (monomial 1))) sm
Tactic:
apply LinearMap.congr_fun
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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ LinearMap.rTensor M (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) =
    LinearMap.rTensor M (ψ.toLinearMap ∘ₗ ↑R (monomial 1))
Theorem: PolynomialMap.componentIsHomogeneous
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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ LinearMap.rTensor M (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) =
    LinearMap.rTensor M (ψ.toLinearMap ∘ₗ ↑R (monomial 1))
Tactic:
apply congr_arg
Proof state after:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ ↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) = ψ.toLinearMap ∘ₗ ↑R (monomial 1)
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ ↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) = ψ.toLinearMap ∘ₗ ↑R (monomial 1)
Tactic:
rw [LinearMap.ext_iff]
Proof state after:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ ∀ (x : S), (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) x = (ψ.toLinearMap ∘ₗ ↑R (monomial 1)) x
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
⊢ ∀ (x : S), (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) x = (ψ.toLinearMap ∘ₗ ↑R (monomial 1)) x
Tactic:
intro r
Proof state after:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) r = (ψ.toLinearMap ∘ₗ ↑R (monomial 1)) r
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (↑R (monomial 1) ∘ₗ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) r = (ψ.toLinearMap ∘ₗ ↑R (monomial 1)) r
Tactic:
simp only [compl₂_id, smul_eq_mul, lift.tmul, coe_comp, coe_restrictScalars,
  Function.comp_apply, IsLinearMap.mk'_apply, mk_apply, AlgHom.toLinearMap_apply,
  AlgHom.coe_restrictScalars', aeval_monomial, pow_one]
Proof state after:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (monomial 1) (s * r) = ψ ((monomial 1) r)
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (monomial 1) (s * r) = ψ ((monomial 1) r)
Tactic:
rw [mul_comm]
Proof state after:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (monomial 1) (r * s) = ψ ((monomial 1) r)
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case 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
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this : ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
r : S
⊢ (monomial 1) (r * s) = ψ ((monomial 1) r)
Tactic:
simp only [AlgHom.coe_restrictScalars', aeval_monomial, pow_one, ψ, ← smul_eq_mul,
  algebraMap_smul, Polynomial.smul_monomial]
Proof state after:
no goals
Theorem: PolynomialMap.component_add
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
p✝ p : ℕ
f g : M →ₚ[R] N
⊢ component p (f + g) = component p f + component p g
Tactic:
ext S _ _ sm
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
p✝ p : ℕ
f g : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (component p (f + g)).toFun' S sm = (component p f + component p g).toFun' S sm
Theorem: PolynomialMap.component_add
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
p✝ p : ℕ
f g : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (component p (f + g)).toFun' S sm = (component p f + component p g).toFun' S sm
Tactic:
simp only [component, add_def_apply, map_add, Finsupp.coe_add, Pi.add_apply]
Proof state after:
no goals
Theorem: PolynomialMap.component_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
p : ℕ
r : R
f : M →ₚ[R] N
⊢ component p (r • f) = r • component p f
Tactic:
ext S _ _ sm
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
p : ℕ
r : R
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (component p (r • f)).toFun' S sm = (r • component p f).toFun' S sm
Theorem: PolynomialMap.component_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
p : ℕ
r : R
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (component p (r • f)).toFun' S sm = (r • component p f).toFun' S sm
Tactic:
simp only [component, smul_def_apply, rTensor_apply, LinearMapClass.map_smul]
Proof state after:
no goals
Theorem: PolynomialMap.support_component'
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
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (Function.support fun i => ((fun p => component p f) i).toFun' S m) =
    ↑((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
Tactic:
ext n
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
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
n : ℕ
⊢ (n ∈ Function.support fun i => ((fun p => component p f) i).toFun' S m) ↔
    n ∈ ↑((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
Theorem: PolynomialMap.support_component'
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
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
n : ℕ
⊢ (n ∈ Function.support fun i => ((fun p => component p f) i).toFun' S m) ↔
    n ∈ ↑((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
Tactic:
simp only [component, Finsupp.fun_support_eq, Finset.mem_coe, Finsupp.mem_support_iff, ne_eq]
Proof state after:
no goals
Theorem: PolynomialMap.support_component
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
p : ℕ
f : M →ₚ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (Function.support fun i => ((fun p => component p f) i).toFun S m) =
    ↑((Polynomial.rTensor R N S) (f.toFun S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
Tactic:
ext i
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
p : ℕ
f : M →ₚ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
i : ℕ
⊢ (i ∈ Function.support fun i => ((fun p => component p f) i).toFun S m) ↔
    i ∈ ↑((Polynomial.rTensor R N S) (f.toFun S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
Theorem: PolynomialMap.support_component
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
p : ℕ
f : M →ₚ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
i : ℕ
⊢ (i ∈ Function.support fun i => ((fun p => component p f) i).toFun S m) ↔
    i ∈ ↑((Polynomial.rTensor R N S) (f.toFun S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))).support
Tactic:
rw [Function.mem_support, ne_eq, Finset.mem_coe, Finsupp.mem_support_iff, not_iff_not,
  component_toFun]
Proof state after:
no goals
Theorem: PolynomialMap.LocFinsupp_component
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
p : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (Function.support fun i => ((fun p => component p f) i).toFun' S m).Finite
Tactic:
simp only [support_component', Finset.finite_toSet]
Proof state after:
no goals
Theorem: PolynomialMap.LocFinsupp_component_eq
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
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ Finsupp.ofSupportFinite (fun i => (component i f).toFun' S m) ⋯ =
    (Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))
Tactic:
ext n
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
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
n : ℕ
⊢ (Finsupp.ofSupportFinite (fun i => (component i f).toFun' S m) ⋯) n =
    ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))) n
Theorem: PolynomialMap.LocFinsupp_component_eq
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
p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
n : ℕ
⊢ (Finsupp.ofSupportFinite (fun i => (component i f).toFun' S m) ⋯) n =
    ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))) n
Tactic:
simp only [component, Finsupp.ofSupportFinite_coe]
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case zero
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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
⊢ (((Polynomial.rTensor R N S) 0).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) 0
Tactic:
simp only [map_zero, Finsupp.sum_zero_index]
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_C
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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ (((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (C s ⊗ₜ[R] n)
Tactic:
rw [Finsupp.sum_eq_single 0, rTensor_apply, rTensor_tmul, rTensor_tmul]
Proof state after:
case tmul.h_C
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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ φ 0 • (↑R (lcoeff S 0)) (C s) ⊗ₜ[R] n = (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n))) (C s) ⊗ₜ[R] n

case tmul.h_C.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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ∀ (b : ℕ),
    ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0 → b ≠ 0 → φ b • ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b = 0

case tmul.h_C.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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) 0 = 0 → φ 0 • 0 = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_C
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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ φ 0 • (↑R (lcoeff S 0)) (C s) ⊗ₜ[R] n = (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n))) (C s) ⊗ₜ[R] n

case tmul.h_C.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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ∀ (b : ℕ),
    ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0 → b ≠ 0 → φ b • ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b = 0

case tmul.h_C.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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) 0 = 0 → φ 0 • 0 = 0
Tactic:
simp only [coe_restrictScalars, lcoeff_apply, coeff_C_zero, Polynomial.lsum_apply,
  lsmul_apply, smul_eq_mul, mul_zero, sum_C_index]
Proof state after:
case tmul.h_C
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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ φ 0 • s ⊗ₜ[R] n = (φ 0 * s) ⊗ₜ[R] n

case tmul.h_C.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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ∀ (b : ℕ),
    ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0 → b ≠ 0 → φ b • ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b = 0

case tmul.h_C.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
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) 0 = 0 → φ 0 • 0 = 0