internlm/Lean-Github huggingface dataset:
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
⊢ (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
Proof 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
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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
Proof 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
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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]
Proof 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)
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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)
Proof 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
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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]
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
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]
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
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
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
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
Proof 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
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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])]
Proof 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
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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)
Proof state after:
no goals
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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])]
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
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]
Proof state after:
no goals
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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]
Proof 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
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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'
Proof 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
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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
Proof 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