internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.rTensor_lcoeff
Proof state before:
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
sn : MvPolynomial σ R ⊗[R] N
k : σ →₀ ℕ
⊢ (LinearMap.rTensor N (lcoeff R k)) sn = 1 ⊗ₜ[R] (scalarRTensor sn) k
Tactic:
induction sn using TensorProduct.induction_on with
| zero => simp
| tmul s n =>
  simp only [rTensor_tmul, scalarRTensor_apply_tmul, Finsupp.sum_apply]
  rw [Finsupp.sum_eq_single k (fun b _ hb => by rw [Finsupp.single_eq_of_ne hb])
    (fun _ => by rw [_root_.zero_smul, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]),
    Finsupp.single_eq_same, lcoeff_apply, ← smul_tmul, smul_eq_mul, mul_one]
  congr
| add x y hx hy => simp only [LinearMap.map_add, LinearEquiv.map_add, hx, hy,
    Finsupp.add_apply, tmul_add]
Proof state after:
no goals
Theorem: MvPolynomial.rTensor_lcoeff
Proof state before:
case zero
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
⊢ (LinearMap.rTensor N (lcoeff R k)) 0 = 1 ⊗ₜ[R] (scalarRTensor 0) k
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.rTensor_lcoeff
Proof state before:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ (LinearMap.rTensor N (lcoeff R k)) (s ⊗ₜ[R] n) = 1 ⊗ₜ[R] (scalarRTensor (s ⊗ₜ[R] n)) k
Tactic:
simp only [rTensor_tmul, scalarRTensor_apply_tmul, Finsupp.sum_apply]
Proof state after:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ (lcoeff R k) s ⊗ₜ[R] n = 1 ⊗ₜ[R] Finsupp.sum s fun a₁ b => (Finsupp.single a₁ (b • n)) k
Theorem: MvPolynomial.rTensor_lcoeff
Proof state before:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ (lcoeff R k) s ⊗ₜ[R] n = 1 ⊗ₜ[R] Finsupp.sum s fun a₁ b => (Finsupp.single a₁ (b • n)) k
Tactic:
rw [Finsupp.sum_eq_single k (fun b _ hb => by rw [Finsupp.single_eq_of_ne hb])
  (fun _ => by rw [_root_.zero_smul, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]),
  Finsupp.single_eq_same, lcoeff_apply, ← smul_tmul, smul_eq_mul, mul_one]
Proof state after:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ MvPolynomial.coeff k s ⊗ₜ[R] n = s k ⊗ₜ[R] n
Theorem: MvPolynomial.rTensor_lcoeff
Proof state before:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ MvPolynomial.coeff k s ⊗ₜ[R] n = s k ⊗ₜ[R] n
Tactic:
congr
Proof state after:
no goals
Theorem: MvPolynomial.rTensor_lcoeff
Proof state before:
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
b : σ →₀ ℕ
x✝ : s b ≠ 0
hb : b ≠ k
⊢ (Finsupp.single b (s b • n)) k = 0
Tactic:
rw [Finsupp.single_eq_of_ne hb]
Proof state after:
no goals
Theorem: MvPolynomial.rTensor_lcoeff
Proof state before:
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
x✝ : s k = 0
⊢ (Finsupp.single k (0 • n)) k = 0
Tactic:
rw [_root_.zero_smul, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]
Proof state after:
no goals
Theorem: MvPolynomial.rTensor_lcoeff
Proof state before:
case add
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
x y : MvPolynomial σ R ⊗[R] N
hx : (LinearMap.rTensor N (lcoeff R k)) x = 1 ⊗ₜ[R] (scalarRTensor x) k
hy : (LinearMap.rTensor N (lcoeff R k)) y = 1 ⊗ₜ[R] (scalarRTensor y) k
⊢ (LinearMap.rTensor N (lcoeff R k)) (x + y) = 1 ⊗ₜ[R] (scalarRTensor (x + y)) k
Tactic:
simp only [LinearMap.map_add, LinearEquiv.map_add, hx, hy,
Finsupp.add_apply, tmul_add]
Proof state after:
no goals
Theorem: MvPolynomial.scalarRTensor_apply
Proof state before:
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
sn : MvPolynomial σ R ⊗[R] N
k : σ →₀ ℕ
⊢ (scalarRTensor sn) k = (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) sn)
Tactic:
rw [← LinearEquiv.symm_apply_eq, TensorProduct.lid_symm_apply, rTensor_lcoeff]
Proof state after:
no goals
Theorem: PolynomialMap.coeff_eq
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) k =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)))
Tactic:
rw [coeff, coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ]
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ (scalarRTensor ((generize m) f)) k =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)))
Theorem: PolynomialMap.coeff_eq
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ (scalarRTensor ((generize m) f)) k =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)))
Tactic:
exact scalarRTensor_apply _ _
Proof state after:
no goals
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) (Finsupp.equivMapDomain e k) = ((coeff (m ∘ ⇑e)) f) k
Tactic:
simp only [coeff, coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  MvPolynomial.scalarRTensor_apply, Function.comp]
Proof state after:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k))) ((generize m) f)) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
⊢ (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k))) ((generize m) f)) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Tactic:
let hf := f.isCompat_apply (MvPolynomial.aeval (fun i ↦ MvPolynomial.X (e i)) :
  MvPolynomial ι R →ₐ[R] MvPolynomial κ R) (univ.sum (fun i ↦ MvPolynomial.X i ⊗ₜ[R] (m (e i))))
Proof state after:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k))) ((generize m) f)) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k))) ((generize m) f)) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Tactic:
suffices toFun f (MvPolynomial κ R)
  (Finset.sum univ (fun x ↦ MvPolynomial.X (e x) ⊗ₜ[R] m (e x))) = generize m f by
  simp only [map_sum, rTensor_tmul, AlgHom.toLinearMap_apply,
    MvPolynomial.aeval_X, this] at hf
  rw [← hf]
  generalize h : generize (fun x ↦ m (e x)) f = g
  simp only [generize, coe_mk, AddHom.coe_mk] at h
  rw [h, EmbeddingLike.apply_eq_iff_eq, ← LinearMap.rTensor_comp_apply]
  congr
  ext p
  simp only [coe_comp, Function.comp_apply, AlgHom.toLinearMap_apply, MvPolynomial.aeval_monomial,
    _root_.map_one, Finsupp.prod_pow, _root_.one_mul, MvPolynomial.lcoeff_apply]
  suffices Finset.prod univ (fun x ↦ MvPolynomial.X (e x) ^ p x) =
      MvPolynomial.monomial (Finsupp.equivMapDomain e p) (1 : R) by
    simp only [this, MvPolynomial.coeff_monomial]
    by_cases h : p = k
    . rw [if_pos h, if_pos (by rw [h])]
    . rw [if_neg h, if_neg]
      intro h'; apply h
      simp only [DFunLike.ext_iff] at h'
      ext i
      simpa only [Finsupp.equivMapDomain_apply, Equiv.symm_apply_apply] using h' (e i)
  . simp only [monomial_eq, _root_.map_one, Finsupp.prod_pow, Finsupp.equivMapDomain_apply,
      _root_.one_mul, prod_congr_equiv e, map_univ_equiv, Function.comp_apply,
       Equiv.apply_symm_apply]
Proof state after:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
Tactic:
. rw [generize, coe_mk, AddHom.coe_mk]
  apply congr_arg
  simp only [sum_congr_equiv e, map_univ_equiv, Function.comp_apply, Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
⊢ (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k))) ((generize m) f)) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Tactic:
simp only [map_sum, rTensor_tmul, AlgHom.toLinearMap_apply,
  MvPolynomial.aeval_X, this] at hf
Proof state after:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
⊢ (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k))) ((generize m) f)) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
⊢ (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k))) ((generize m) f)) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Tactic:
rw [← hf]
Proof state after:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
⊢ (TensorProduct.lid R N)
      ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k)))
        ((LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
          (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))))) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
⊢ (TensorProduct.lid R N)
      ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k)))
        ((LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
          (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))))) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) ((generize fun x => m (e x)) f))
Tactic:
generalize h : generize (fun x ↦ m (e x)) f = g
Proof state after:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h : (generize fun x => m (e x)) f = g
⊢ (TensorProduct.lid R N)
      ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k)))
        ((LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
          (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))))) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) g)
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h : (generize fun x => m (e x)) f = g
⊢ (TensorProduct.lid R N)
      ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k)))
        ((LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
          (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))))) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) g)
Tactic:
simp only [generize, coe_mk, AddHom.coe_mk] at h
Proof state after:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
⊢ (TensorProduct.lid R N)
      ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k)))
        ((LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
          (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))))) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) g)
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
⊢ (TensorProduct.lid R N)
      ((LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k)))
        ((LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
          (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))))) =
    (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) g)
Tactic:
rw [h, EmbeddingLike.apply_eq_iff_eq, ← LinearMap.rTensor_comp_apply]
Proof state after:
R : Type u
inst✝¹⁰ : CommRing R
M : Type uM
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type uN
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
ι✝ : Type uι
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : Fintype ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
⊢ (LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k) ∘ₗ (aeval fun i => X (e i)).toLinearMap)) g =
    (LinearMap.rTensor N (lcoeff R k)) g