internlm/Lean-Github huggingface dataset:
Theorem: Polynomial.rTensor'_sum
Proof state before:
case add
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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
⊢ (((Polynomial.rTensor R N S) p + (Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p + q)
Tactic:
rw [Finsupp.sum_add_index, hp, hq, LinearMap.map_add]
Proof state after:
case add.h_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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
⊢ ∀ a ∈ ((Polynomial.rTensor R N S) p).support ∪ ((Polynomial.rTensor R N S) q).support, φ a • 0 = 0

case add.h_add
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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
⊢ ∀ a ∈ ((Polynomial.rTensor R N S) p).support ∪ ((Polynomial.rTensor R N S) q).support,
    ∀ (b₁ b₂ : S ⊗[R] N), φ a • (b₁ + b₂) = φ a • b₁ + φ a • b₂
Theorem: Polynomial.rTensor'_sum
Proof state before:
case add.h_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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
⊢ ∀ a ∈ ((Polynomial.rTensor R N S) p).support ∪ ((Polynomial.rTensor R N S) q).support, φ a • 0 = 0
Tactic:
intro x _
Proof state after:
case add.h_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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
x : ℕ
a✝ : x ∈ ((Polynomial.rTensor R N S) p).support ∪ ((Polynomial.rTensor R N S) q).support
⊢ φ x • 0 = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case add.h_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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
x : ℕ
a✝ : x ∈ ((Polynomial.rTensor R N S) p).support ∪ ((Polynomial.rTensor R N S) q).support
⊢ φ x • 0 = 0
Tactic:
exact smul_zero _
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case add.h_add
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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
⊢ ∀ a ∈ ((Polynomial.rTensor R N S) p).support ∪ ((Polynomial.rTensor R N S) q).support,
    ∀ (b₁ b₂ : S ⊗[R] N), φ a • (b₁ + b₂) = φ a • b₁ + φ a • b₂
Tactic:
intro x _
Proof state after:
case add.h_add
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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
x : ℕ
a✝ : x ∈ ((Polynomial.rTensor R N S) p).support ∪ ((Polynomial.rTensor R N S) q).support
⊢ ∀ (b₁ b₂ : S ⊗[R] N), φ x • (b₁ + b₂) = φ x • b₁ + φ x • b₂
Theorem: Polynomial.rTensor'_sum
Proof state before:
case add.h_add
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
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
x : ℕ
a✝ : x ∈ ((Polynomial.rTensor R N S) p).support ∪ ((Polynomial.rTensor R N S) q).support
⊢ ∀ (b₁ b₂ : S ⊗[R] N), φ x • (b₁ + b₂) = φ x • b₁ + φ x • b₂
Tactic:
exact smul_add _
Proof state after:
no goals
Theorem: PolynomialMap.recompose_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
⊢ (lfsum fun p => component p f) = 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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (lfsum fun p => component p f).toFun' S sm = f.toFun' S sm
Theorem: PolynomialMap.recompose_component
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (lfsum fun p => component p f).toFun' S sm = f.toFun' S sm
Tactic:
rw [lfsum_eq (LocFinsupp_component f), LocFinsupp_component_eq]
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    f.toFun' S sm
Theorem: PolynomialMap.recompose_component
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    f.toFun' S sm
Tactic:
have hsm : sm = ((aeval 1).restrictScalars R).toLinearMap.rTensor M
  (((monomial 1).restrictScalars R).rTensor M sm) := by
  rw [← LinearMap.rTensor_comp_apply, LinearMap.rTensor, eq_comm]
  convert DFunLike.congr_fun TensorProduct.map_id sm
  ext s
  simp only [coe_comp, coe_restrictScalars, Function.comp_apply, AlgHom.toLinearMap_apply,
    AlgHom.coe_restrictScalars', aeval_monomial, Algebra.id.map_eq_id, RingHom.id_apply, pow_one,
    mul_one, id_coe, id_eq]
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    f.toFun' S sm
Theorem: PolynomialMap.recompose_component
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    f.toFun' S sm
Tactic:
conv_rhs => rw [hsm, ← f.isCompat_apply']
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    (LinearMap.rTensor N (AlgHom.restrictScalars R (aeval 1)).toLinearMap)
      (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))
Theorem: PolynomialMap.recompose_component
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ (((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))).sum fun x m => m) =
    (LinearMap.rTensor N (AlgHom.restrictScalars R (aeval 1)).toLinearMap)
      (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))
Tactic:
generalize f.toFun' S[X] (((monomial 1).restrictScalars R).rTensor M sm) = sn
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
⊢ (((Polynomial.rTensor R N S) sn).sum fun x m => m) =
    (LinearMap.rTensor N (AlgHom.restrictScalars R (aeval 1)).toLinearMap) sn
Theorem: PolynomialMap.recompose_component
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
⊢ (((Polynomial.rTensor R N S) sn).sum fun x m => m) =
    (LinearMap.rTensor N (AlgHom.restrictScalars R (aeval 1)).toLinearMap) sn
Tactic:
convert rTensor'_sum (R := R) (fun _ ↦ 1) sn
Proof state after:
case h.e'_2.h.e'_7.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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝² : CommRing S
x✝¹ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
x✝ : S ⊗[R] N
⊢ x✝ = 1 • x✝

case h.e'_3.h.e'_5.h.e'_12.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
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap = Polynomial.lsum fun n => ↑R ((lsmul S S) 1)
Theorem: PolynomialMap.recompose_component
Proof state before:
case h.e'_2.h.e'_7.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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝² : CommRing S
x✝¹ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
x✝ : S ⊗[R] N
⊢ x✝ = 1 • x✝

case h.e'_3.h.e'_5.h.e'_12.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
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap = Polynomial.lsum fun n => ↑R ((lsmul S S) 1)
Tactic:
simp only [_root_.one_smul]
Proof state after:
case h.e'_3.h.e'_5.h.e'_12.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
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap = Polynomial.lsum fun n => ↑R ((lsmul S S) 1)
Theorem: PolynomialMap.recompose_component
Proof state before:
case h.e'_3.h.e'_5.h.e'_12.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
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap = Polynomial.lsum fun n => ↑R ((lsmul S S) 1)
Tactic:
ext p
Proof state after:
case h.e'_3.h.e'_5.h.e'_12.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✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap p = (Polynomial.lsum fun n => ↑R ((lsmul S S) 1)) p
Theorem: PolynomialMap.recompose_component
Proof state before:
case h.e'_3.h.e'_5.h.e'_12.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✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap p = (Polynomial.lsum fun n => ↑R ((lsmul S S) 1)) p
Tactic:
simp only [AlgHom.toLinearMap_apply, AlgHom.coe_restrictScalars', coe_aeval_eq_eval,
  Polynomial.lsum_apply, coe_restrictScalars, lsmul_apply, smul_eq_mul, one_mul, eval_eq_sum]
Proof state after:
case h.e'_3.h.e'_5.h.e'_12.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✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (p.sum fun e a => a * 1 ^ e) = p.sum fun x x => x
Theorem: PolynomialMap.recompose_component
Proof state before:
case h.e'_3.h.e'_5.h.e'_12.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✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (p.sum fun e a => a * 1 ^ e) = p.sum fun x x => x
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
case h.e'_3.h.e'_5.h.e'_12.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✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (fun e a => a * 1 ^ e) = fun x x => x
Theorem: PolynomialMap.recompose_component
Proof state before:
case h.e'_3.h.e'_5.h.e'_12.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✝ : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
hsm :
  sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
sn : S[X] ⊗[R] N
e_10✝ : Algebra.toModule = Polynomial.module
p : S[X]
⊢ (fun e a => a * 1 ^ e) = fun x x => x
Tactic:
simp only [one_pow, mul_one]
Proof state after:
no goals
Theorem: PolynomialMap.recompose_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
sm : S ⊗[R] M
⊢ sm =
    (LinearMap.rTensor M (AlgHom.restrictScalars R (aeval 1)).toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Tactic:
rw [← LinearMap.rTensor_comp_apply, LinearMap.rTensor, eq_comm]
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 : ℕ
f : M →ₚ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
⊢ (TensorProduct.map ((AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1)) LinearMap.id) sm = sm
Theorem: PolynomialMap.recompose_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
sm : S ⊗[R] M
⊢ (TensorProduct.map ((AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1)) LinearMap.id) sm = sm
Tactic:
convert DFunLike.congr_fun TensorProduct.map_id sm
Proof state after:
case h.e'_2.h.e'_5.h.e'_15
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
sm : S ⊗[R] M
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1) = LinearMap.id
Theorem: PolynomialMap.recompose_component
Proof state before:
case h.e'_2.h.e'_5.h.e'_15
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
sm : S ⊗[R] M
⊢ (AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1) = LinearMap.id
Tactic:
ext s
Proof state after:
case h.e'_2.h.e'_5.h.e'_15.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
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
s : S
⊢ ((AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1)) s = LinearMap.id s
Theorem: PolynomialMap.recompose_component
Proof state before:
case h.e'_2.h.e'_5.h.e'_15.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
x✝¹ : CommRing S
x✝ : Algebra R S
sm : S ⊗[R] M
s : S
⊢ ((AlgHom.restrictScalars R (aeval 1)).toLinearMap ∘ₗ ↑R (monomial 1)) s = LinearMap.id s
Tactic:
simp only [coe_comp, coe_restrictScalars, Function.comp_apply, AlgHom.toLinearMap_apply,
  AlgHom.coe_restrictScalars', aeval_monomial, Algebra.id.map_eq_id, RingHom.id_apply, pow_one,
  mul_one, id_coe, id_eq]
Proof state after:
no goals
Theorem: DividedPowers.isExponential_dpowExp
Proof state before:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (hI.dpowExp a).IsExponential
Tactic:
rw [isExponential_iff]
Proof state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (constantCoeff R) (hI.dpowExp a) = 1 ∧
    ∀ (p q : ℕ),
      ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)