Theorem: PolynomialMap.coeff_comp_equiv (DividedPowers/PolynomialMap/Coeff.lean)

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]
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))

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))))
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))

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]
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

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]
State after:
no goals

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
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))

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]
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))

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
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)

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
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)

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]
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

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
⊢ (LinearMap.rTensor N (lcoeff R (Finsupp.equivMapDomain e k) ∘ₗ (aeval fun i => X (e i)).toLinearMap)) g =
    (LinearMap.rTensor N (lcoeff R k)) g
Tactic:
congr
State after:
case e_a.e_f
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
⊢ lcoeff R (Finsupp.equivMapDomain e k) ∘ₗ (aeval fun i => X (e i)).toLinearMap = lcoeff R k

State before:
case e_a.e_f
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
⊢ lcoeff R (Finsupp.equivMapDomain e k) ∘ₗ (aeval fun i => X (e i)).toLinearMap = lcoeff R k
Tactic:
ext p
State after:
case e_a.e_f.h.h
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
p : ι →₀ ℕ
⊢ ((lcoeff R (Finsupp.equivMapDomain e k) ∘ₗ (aeval fun i => X (e i)).toLinearMap) ∘ₗ monomial p) 1 =
    (lcoeff R k ∘ₗ monomial p) 1

State before:
case e_a.e_f.h.h
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
p : ι →₀ ℕ
⊢ ((lcoeff R (Finsupp.equivMapDomain e k) ∘ₗ (aeval fun i => X (e i)).toLinearMap) ∘ₗ monomial p) 1 =
    (lcoeff R k ∘ₗ monomial p) 1
Tactic:
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]
State after:
case e_a.e_f.h.h
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
p : ι →₀ ℕ
⊢ MvPolynomial.coeff (Finsupp.equivMapDomain e k) (∏ a : ι, X (e a) ^ p a) = MvPolynomial.coeff k ((monomial p) 1)

State before:
case e_a.e_f.h.h
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
p : ι →₀ ℕ
⊢ MvPolynomial.coeff (Finsupp.equivMapDomain e k) (∏ a : ι, X (e a) ^ p a) = MvPolynomial.coeff k ((monomial p) 1)
Tactic:
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)
State after:
case e_a.e_f.h.h
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
p : ι →₀ ℕ
⊢ ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1

State before:
case e_a.e_f.h.h
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
p : ι →₀ ℕ
⊢ ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
Tactic:
. 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]
State after:
no goals

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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
⊢ MvPolynomial.coeff (Finsupp.equivMapDomain e k) (∏ a : ι, X (e a) ^ p a) = MvPolynomial.coeff k ((monomial p) 1)
Tactic:
simp only [this, MvPolynomial.coeff_monomial]
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0

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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0
Tactic:
by_cases h : p = k
State after:
case pos
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : p = k
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0

case neg
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0

State before:
case pos
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : p = k
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0

case neg
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0
Tactic:
. rw [if_pos h, if_pos (by rw [h])]
State after:
case neg
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0

State before:
case neg
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0
Tactic:
. 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)
State after:
no goals

State before:
case pos
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : p = k
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0
Tactic:
rw [if_pos h, if_pos (by rw [h])]
State after:
no goals

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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : p = k
⊢ Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k
Tactic:
rw [h]
State after:
no goals

State before:
case neg
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
⊢ (if Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k then 1 else 0) = if p = k then 1 else 0
Tactic:
rw [if_neg h, if_neg]
State after:
case neg.hnc
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
⊢ ¬Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k

State before:
case neg.hnc
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
⊢ ¬Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k
Tactic:
intro h'
State after:
case neg.hnc
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k
⊢ False

State before:
case neg.hnc
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k
⊢ False
Tactic:
apply h
State after:
case neg.hnc
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k
⊢ p = k

State before:
case neg.hnc
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k
⊢ p = k
Tactic:
simp only [DFunLike.ext_iff] at h'
State after:
case neg.hnc
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : ∀ (x : κ), (Finsupp.equivMapDomain e p) x = (Finsupp.equivMapDomain e k) x
⊢ p = k

State before:
case neg.hnc
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : ∀ (x : κ), (Finsupp.equivMapDomain e p) x = (Finsupp.equivMapDomain e k) x
⊢ p = k
Tactic:
ext i
State after:
case neg.hnc.h
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : ∀ (x : κ), (Finsupp.equivMapDomain e p) x = (Finsupp.equivMapDomain e k) x
i : ι
⊢ p i = k i

State before:
case neg.hnc.h
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
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : ∀ (x : κ), (Finsupp.equivMapDomain e p) x = (Finsupp.equivMapDomain e k) x
i : ι
⊢ p i = k i
Tactic:
simpa only [Finsupp.equivMapDomain_apply, Equiv.symm_apply_apply] using h' (e i)
State after:
no goals

State before:
case e_a.e_f.h.h
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
p : ι →₀ ℕ
⊢ ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
Tactic:
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]
State after:
no goals

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]
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)) = f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)

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)) = f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)
Tactic:
apply congr_arg
State after:
case h
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))
⊢ ∑ x : ι, X (e x) ⊗ₜ[R] m (e x) = ∑ i : κ, X i ⊗ₜ[R] m i

State before:
case h
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))
⊢ ∑ x : ι, X (e x) ⊗ₜ[R] m (e x) = ∑ i : κ, X i ⊗ₜ[R] m i
Tactic:
simp only [sum_congr_equiv e, map_univ_equiv, Function.comp_apply, Equiv.apply_symm_apply]
State after:
no goals