internlm/Lean-Github huggingface dataset:
Theorem: Polynomial.rTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ p.toFinsupp i ⊗ₜ[R] n = p.coeff i ⊗ₜ[R] n
Tactic:
rfl
Proof state after:
no goals
Theorem: Polynomial.rTensor_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (rTensor R N S) (p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
simp only [rTensor, LinearEquiv.trans_apply, finsuppLeft'_apply,
  LinearEquiv.rTensor'_apply, LinearEquiv.rTensor]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ)
      ((TensorProduct.congr (LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)) (LinearEquiv.refl R N))
        (p ⊗ₜ[R] n)) =
    p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Theorem: Polynomial.rTensor_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ)
      ((TensorProduct.congr (LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)) (LinearEquiv.refl R N))
        (p ⊗ₜ[R] n)) =
    p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
simp only [congr_tmul, LinearEquiv.restrictScalars_apply, refl_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ) ((toFinsuppLinearEquiv S) p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Theorem: Polynomial.rTensor_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ) ((toFinsuppLinearEquiv S) p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
simp only [toFinsuppLinearEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
  Equiv.invFun_as_coe, LinearEquiv.coe_mk, toFinsuppIso_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ) (p.toFinsupp ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Theorem: Polynomial.rTensor_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ) (p.toFinsupp ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
rw [finsuppLeft_apply_tmul]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (Finsupp.sum p.toFinsupp fun i m => Finsupp.single i (m ⊗ₜ[R] n)) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Theorem: Polynomial.rTensor_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
⊢ (Finsupp.sum p.toFinsupp fun i m => Finsupp.single i (m ⊗ₜ[R] n)) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
rfl
Proof state after:
no goals
Theorem: Polynomial.rTensor_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ ((rTensor R N S) t) d = (LinearMap.rTensor N (↑R (lcoeff S d))) t
Tactic:
simp only [rTensor, LinearEquiv.trans_apply, finsuppLeft'_apply,
  LinearEquiv.rTensor'_apply, LinearEquiv.rTensor]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ ((finsuppLeft R S N ℕ)
        ((TensorProduct.congr (LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)) (LinearEquiv.refl R N)) t))
      d =
    (LinearMap.rTensor N (↑R (lcoeff S d))) t
Theorem: Polynomial.rTensor_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ ((finsuppLeft R S N ℕ)
        ((TensorProduct.congr (LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)) (LinearEquiv.refl R N)) t))
      d =
    (LinearMap.rTensor N (↑R (lcoeff S d))) t
Tactic:
simp only [TensorProduct.congr, refl_toLinearMap, refl_symm, ofLinear_apply, finsuppLeft_apply,
  LinearMap.rTensor]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ (TensorProduct.map (Finsupp.lapply d) LinearMap.id)
      ((TensorProduct.map (↑(LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S))) LinearMap.id) t) =
    (TensorProduct.map (↑R (lcoeff S d)) LinearMap.id) t
Theorem: Polynomial.rTensor_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ (TensorProduct.map (Finsupp.lapply d) LinearMap.id)
      ((TensorProduct.map (↑(LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S))) LinearMap.id) t) =
    (TensorProduct.map (↑R (lcoeff S d)) LinearMap.id) t
Tactic:
rw [← LinearMap.comp_apply, ← TensorProduct.map_comp]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ (TensorProduct.map (Finsupp.lapply d ∘ₗ ↑(LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)))
        (LinearMap.id ∘ₗ LinearMap.id))
      t =
    (TensorProduct.map (↑R (lcoeff S d)) LinearMap.id) t
Theorem: Polynomial.rTensor_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ (TensorProduct.map (Finsupp.lapply d ∘ₗ ↑(LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)))
        (LinearMap.id ∘ₗ LinearMap.id))
      t =
    (TensorProduct.map (↑R (lcoeff S d)) LinearMap.id) t
Tactic:
rfl
Proof state after:
no goals
Theorem: Polynomial.rTensorAlgHom_coeff_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((rTensorAlgHom R N S) (p ⊗ₜ[R] n)).coeff d = p.coeff d ⊗ₜ[R] n
Tactic:
rw [rTensorAlgHom, Algebra.TensorProduct.lift_tmul]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
          ((IsScalarTower.toAlgHom R (S ⊗[R] N) (S ⊗[R] N)[X]).comp Algebra.TensorProduct.includeRight) n).coeff
      d =
    p.coeff d ⊗ₜ[R] n
Theorem: Polynomial.rTensorAlgHom_coeff_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
          ((IsScalarTower.toAlgHom R (S ⊗[R] N) (S ⊗[R] N)[X]).comp Algebra.TensorProduct.includeRight) n).coeff
      d =
    p.coeff d ⊗ₜ[R] n
Tactic:
rw [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply,
  Algebra.TensorProduct.includeRight_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((mapAlgHom Algebra.TensorProduct.includeLeft) p * (algebraMap (S ⊗[R] N) (S ⊗[R] N)[X]) (1 ⊗ₜ[R] n)).coeff d =
    p.coeff d ⊗ₜ[R] n
Theorem: Polynomial.rTensorAlgHom_coeff_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ ((mapAlgHom Algebra.TensorProduct.includeLeft) p * (algebraMap (S ⊗[R] N) (S ⊗[R] N)[X]) (1 ⊗ₜ[R] n)).coeff d =
    p.coeff d ⊗ₜ[R] n
Tactic:
rw [← C_eq_algebraMap, mul_comm, coeff_C_mul]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ 1 ⊗ₜ[R] n * ((mapAlgHom Algebra.TensorProduct.includeLeft) p).coeff d = p.coeff d ⊗ₜ[R] n
Theorem: Polynomial.rTensorAlgHom_coeff_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
d : ℕ
⊢ 1 ⊗ₜ[R] n * ((mapAlgHom Algebra.TensorProduct.includeLeft) p).coeff d = p.coeff d ⊗ₜ[R] n
Tactic:
simp [mapAlgHom, coeff_map]
Proof state after:
no goals
Theorem: Polynomial.rTensorLinearEquiv_coeff_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).coeff e = p.coeff e ⊗ₜ[R] n
Tactic:
dsimp [coeff]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp e = p.toFinsupp e ⊗ₜ[R] n
Theorem: Polynomial.rTensorLinearEquiv_coeff_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp e = p.toFinsupp e ⊗ₜ[R] n
Tactic:
have h : (rTensorLinearEquiv R N S (p ⊗ₜ[R] n)).toFinsupp
  = TensorProduct.finsuppLeft' _ _ _ _ S (p.toFinsupp ⊗ₜ[R] n) := by
  rfl
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
h : ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp = (finsuppLeft' R S N ℕ S) (p.toFinsupp ⊗ₜ[R] n)
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp e = p.toFinsupp e ⊗ₜ[R] n
Theorem: Polynomial.rTensorLinearEquiv_coeff_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
h : ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp = (finsuppLeft' R S N ℕ S) (p.toFinsupp ⊗ₜ[R] n)
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp e = p.toFinsupp e ⊗ₜ[R] n
Tactic:
rw [h, finsuppLeft'_apply, finsuppLeft_apply_tmul_apply]
Proof state after:
no goals
Theorem: Polynomial.rTensorLinearEquiv_coeff_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp = (finsuppLeft' R S N ℕ S) (p.toFinsupp ⊗ₜ[R] n)
Tactic:
rfl
Proof state after:
no goals
Theorem: Polynomial.rTensorAlgHom_toLinearMap
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (rTensorAlgHom R N S).toLinearMap = ↑(rTensorLinearEquiv R N S)
Tactic:
ext d n e
Proof state after:
case a.h.h.h.a
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
d : ℕ
n : N
e : ℕ
⊢ (((AlgebraTensorModule.curry (rTensorAlgHom R N S).toLinearMap ∘ₗ monomial d) 1) n).coeff e =
    (((AlgebraTensorModule.curry ↑(rTensorLinearEquiv R N S) ∘ₗ monomial d) 1) n).coeff e
Theorem: Polynomial.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h.a
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
d : ℕ
n : N
e : ℕ
⊢ (((AlgebraTensorModule.curry (rTensorAlgHom R N S).toLinearMap ∘ₗ monomial d) 1) n).coeff e =
    (((AlgebraTensorModule.curry ↑(rTensorLinearEquiv R N S) ∘ₗ monomial d) 1) n).coeff e
Tactic:
simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
  LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply, LinearEquiv.coe_coe]
Proof state after:
case a.h.h.h.a
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
d : ℕ
n : N
e : ℕ
⊢ ((rTensorAlgHom R N S) ((monomial d) 1 ⊗ₜ[R] n)).coeff e =
    ((rTensorLinearEquiv R N S) ((monomial d) 1 ⊗ₜ[R] n)).coeff e
Theorem: Polynomial.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h.a
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
d : ℕ
n : N
e : ℕ
⊢ ((rTensorAlgHom R N S) ((monomial d) 1 ⊗ₜ[R] n)).coeff e =
    ((rTensorLinearEquiv R N S) ((monomial d) 1 ⊗ₜ[R] n)).coeff e
Tactic:
rw [rTensorAlgHom_coeff_apply_tmul, rTensorLinearEquiv_coeff_tmul]
Proof state after:
no goals
Theorem: Polynomial.rTensorAlgHom_apply_eq
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X] ⊗[R] N
⊢ (rTensorAlgHom R N S) p = (rTensorLinearEquiv R N S) p
Tactic:
rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X] ⊗[R] N
⊢ ↑(rTensorLinearEquiv R N S) p = (rTensorLinearEquiv R N S) p
Theorem: Polynomial.rTensorAlgHom_apply_eq
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X] ⊗[R] N
⊢ ↑(rTensorLinearEquiv R N S) p = (rTensorLinearEquiv R N S) p
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.prod_congr_equiv
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
s : Finset α
e : α ≃ β
⊢ s.prod f = (map e.toEmbedding s).prod (f ∘ ⇑e.symm)
Tactic:
simp only [Function.comp_apply, prod_map, Equiv.coe_toEmbedding, Equiv.symm_apply_apply]
Proof state after:
no goals
Theorem: Finset.prod_congr_equiv'
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : β → M
s : Finset α
e : α ≃ β
⊢ s.prod (f ∘ ⇑e) = (map e.toEmbedding s).prod f
Tactic:
simp only [Function.comp_apply, prod_map, Equiv.coe_toEmbedding]
Proof state after:
no goals
Theorem: Finsupp.ofSupportFinite_support
Proof state before:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι → α
hf : (Function.support f).Finite
⊢ (ofSupportFinite f hf).support = hf.toFinset
Tactic:
ext
Proof state after:
case a
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι → α
hf : (Function.support f).Finite
a✝ : ι
⊢ a✝ ∈ (ofSupportFinite f hf).support ↔ a✝ ∈ hf.toFinset
Theorem: Finsupp.ofSupportFinite_support
Proof state before:
case a
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι → α
hf : (Function.support f).Finite
a✝ : ι
⊢ a✝ ∈ (ofSupportFinite f hf).support ↔ a✝ ∈ hf.toFinset
Tactic:
simp only [Finsupp.ofSupportFinite_coe, Finsupp.mem_support_iff,
  Set.Finite.mem_toFinset, mem_support]
Proof state after:
no goals
Theorem: LinearForm.baseChange_apply_tmul
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] R
r : S
m : M
⊢ (baseChange R S M f) (r ⊗ₜ[R] m) = r * f m • 1
Tactic:
simp only [baseChange, coe_comp, Function.comp_apply, baseChange_tmul,
  AlgHom.toLinearMap_apply, rid'_tmul, Algebra.mul_smul_comm, _root_.mul_one]
Proof state after:
no goals
Theorem: LinearForm.baseChange_compat_apply
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
m : S ⊗[R] M
⊢ φ ((baseChange R S M f) m) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) m)
Tactic:
induction' m using TensorProduct.induction_on with r m x y hx hy
Proof state after:
case zero
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
⊢ φ ((baseChange R S M f) 0) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) 0)

case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
r : S
m : M
⊢ φ ((baseChange R S M f) (r ⊗ₜ[R] m)) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) (r ⊗ₜ[R] m))

case add
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
x y : S ⊗[R] M
hx : φ ((baseChange R S M f) x) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) x)
hy : φ ((baseChange R S M f) y) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) y)
⊢ φ ((baseChange R S M f) (x + y)) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) (x + y))
Theorem: LinearForm.baseChange_compat_apply
Proof state before:
case zero
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
⊢ φ ((baseChange R S M f) 0) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) 0)
Tactic:
simp only [map_zero]
Proof state after:
no goals
Theorem: LinearForm.baseChange_compat_apply
Proof state before:
case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
r : S
m : M
⊢ φ ((baseChange R S M f) (r ⊗ₜ[R] m)) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) (r ⊗ₜ[R] m))
Tactic:
simp only [baseChange, coe_comp, Function.comp_apply, baseChange_tmul,
  AlgHom.toLinearMap_apply, rid'_tmul, map_smul, rTensor_tmul]
Proof state after:
no goals
Theorem: LinearForm.baseChange_compat_apply
Proof state before:
case add
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
x y : S ⊗[R] M
hx : φ ((baseChange R S M f) x) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) x)
hy : φ ((baseChange R S M f) y) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) y)
⊢ φ ((baseChange R S M f) (x + y)) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) (x + y))
Tactic:
simp only [map_add, hx, hy]
Proof state after:
no goals
Theorem: PolynomialMap.LocFinsupp_zero
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
ι : Type u_3
S : Type u
x✝² : CommRing S
x✝¹ : Algebra R S
x✝ : S ⊗[R] M
⊢ (Function.support fun i => (0 i).toFun' S x✝).Finite
Tactic:
simp only [Pi.zero_apply, zero_def, Function.support_zero, Set.finite_empty]
Proof state after:
no goals