Theorem: PolynomialMap.isHomogeneousOfDegree_coeff (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
⊢ ((coeff m) f) d = 0
Tactic:
let e (b : ι →₀ ℕ) (k : ℕ) : Option ι →₀ ℕ :=
  Finsupp.update (Finsupp.mapDomainEmbedding (Function.Embedding.some) b) none k
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
⊢ ((coeff m) f) d = 0
Tactic:
have he : ∀ b k, (X none ^ k * (Finset.prod Finset.univ
  fun x => X (some x) ^ b x) : MvPolynomial (Option ι) R) = monomial (e b k) 1 := fun b k ↦ by
  rw [monomial_eq, Finsupp.prod_pow, Fintype.prod_option, _root_.map_one, one_mul]
  simp only [Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply, Finsupp.coe_update,
    Function.update_same, ne_eq, not_false_eq_true, Function.update_noteq, e]
  exact congr_arg₂ _ rfl (Finset.prod_congr rfl (fun _ _ => by
    rw [Finsupp.mapDomain_apply (Option.some_injective ι)]))
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
⊢ ((coeff m) f) d = 0
Tactic:
have he_some : ∀ b k i, e b k (some i) = b i := fun b k i ↦ by
  simp only [Finsupp.update, Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply,
    Finsupp.coe_mk, Function.update, ↓reduceDite,
    Finsupp.mapDomain_apply (Option.some_injective ι), e]
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
⊢ ((coeff m) f) d = 0
Tactic:
have he_none : ∀ b k, k = e b k none := fun b k ↦ by
  simp only [Finsupp.update, Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply,
    Finsupp.coe_mk, Function.update, ↓reduceDite, e]
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
⊢ ((coeff m) f) d = 0
Tactic:
let μ : MvPolynomial (Option ι) R ⊗[R] M := Finset.univ.sum (fun i => X (some i) ⊗ₜ[R] m i)
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
⊢ ((coeff m) f) d = 0
Tactic:
have hf' := isHomogeneousOfDegree_toFun hf (MvPolynomial (Option ι) R) (X none) μ
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' : f.toFun (MvPolynomial (Option ι) R) (X none • μ) = X none ^ p • f.toFun (MvPolynomial (Option ι) R) μ
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' : f.toFun (MvPolynomial (Option ι) R) (X none • μ) = X none ^ p • f.toFun (MvPolynomial (Option ι) R) μ
⊢ ((coeff m) f) d = 0
Tactic:
simp only [μ, Finset.smul_sum, TensorProduct.smul_tmul', image_eq_coeff_sum, Finsupp.smul_sum,
  TensorProduct.smul_tmul'] at hf'
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
⊢ ((coeff m) f) d = 0
Tactic:
let φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  (TensorProduct.lid R N).toLinearMap.comp
    (LinearMap.rTensor N (lcoeff R (e d (d.sum fun _ n => n))))
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
⊢ ((coeff m) f) d = 0
Tactic:
let hφ := LinearMap.congr_arg (f := φ) hf'
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : φ (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
  φ (((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b) :=
  LinearMap.congr_arg hf'
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : φ (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
  φ (((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b) :=
  LinearMap.congr_arg hf'
⊢ ((coeff m) f) d = 0
Tactic:
simp only [map_finsupp_sum, LinearMap.map_smul, smul_eq_mul, mul_pow, Finset.prod_mul_distrib,
  Finset.prod_pow_eq_pow_sum] at hφ
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ((coeff m) f) d = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ((coeff m) f) d = 0
Tactic:
rw [Finsupp.sum_eq_single d _ (by simp only [tmul_zero, map_zero, implies_true]),
  Finsupp.sum_eq_single d _ (by simp only [tmul_zero, map_zero, implies_true])] at hφ
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    φ ((X none ^ p * ∏ i : ι, X (some i) ^ d i) ⊗ₜ[R] ((coeff fun i => m i) f) d)
⊢ ((coeff m) f) d = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    φ ((X none ^ p * ∏ i : ι, X (some i) ^ d i) ⊗ₜ[R] ((coeff fun i => m i) f) d)
⊢ ((coeff m) f) d = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0
Tactic:
simp only [lcoeff, coe_comp, LinearEquiv.coe_coe, Function.comp_apply, rTensor_tmul, coe_mk,
  AddHom.coe_mk, lid_tmul, φ] at hφ
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  MvPolynomial.coeff (e d (d.sum fun x n => n)) ((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) •
      ((coeff fun i => m i) f) d =
    MvPolynomial.coeff (e d (d.sum fun x n => n)) (X none ^ p * ∏ i : ι, X (some i) ^ d i) • ((coeff fun i => m i) f) d
⊢ ((coeff m) f) d = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  MvPolynomial.coeff (e d (d.sum fun x n => n)) ((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) •
      ((coeff fun i => m i) f) d =
    MvPolynomial.coeff (e d (d.sum fun x n => n)) (X none ^ p * ∏ i : ι, X (some i) ^ d i) • ((coeff fun i => m i) f) d
⊢ ((coeff m) f) d = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0
Tactic:
rw [he, coeff_monomial, if_pos, _root_.one_smul, he, coeff_monomial, if_neg, _root_.zero_smul]
  at hφ
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = 0
⊢ ((coeff m) f) d = 0

case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
⊢ ¬e d p = e d (d.sum fun x n => n)

case hc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (if e d (∑ i : ι, d i) = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d =
    MvPolynomial.coeff (e d (d.sum fun x n => n)) (X none ^ p * ∏ i : ι, X (some i) ^ d i) • ((coeff fun i => m i) f) d
⊢ e d (∑ i : ι, d i) = e d (d.sum fun x n => n)

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = 0
⊢ ((coeff m) f) d = 0

case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
⊢ ¬e d p = e d (d.sum fun x n => n)

case hc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (if e d (∑ i : ι, d i) = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d =
    MvPolynomial.coeff (e d (d.sum fun x n => n)) (X none ^ p * ∏ i : ι, X (some i) ^ d i) • ((coeff fun i => m i) f) d
⊢ e d (∑ i : ι, d i) = e d (d.sum fun x n => n)

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0
Tactic:
exact hφ
State after:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
⊢ ¬e d p = e d (d.sum fun x n => n)

case hc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (if e d (∑ i : ι, d i) = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d =
    MvPolynomial.coeff (e d (d.sum fun x n => n)) (X none ^ p * ∏ i : ι, X (some i) ^ d i) • ((coeff fun i => m i) f) d
⊢ e d (∑ i : ι, d i) = e d (d.sum fun x n => n)

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
b : ι →₀ ℕ
k : ℕ
⊢ X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
Tactic:
rw [monomial_eq, Finsupp.prod_pow, Fintype.prod_option, _root_.map_one, one_mul]
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
b : ι →₀ ℕ
k : ℕ
⊢ X none ^ k * ∏ x : ι, X (some x) ^ b x = X none ^ (e b k) none * ∏ i : ι, X (some i) ^ (e b k) (some i)

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
b : ι →₀ ℕ
k : ℕ
⊢ X none ^ k * ∏ x : ι, X (some x) ^ b x = X none ^ (e b k) none * ∏ i : ι, X (some i) ^ (e b k) (some i)
Tactic:
simp only [Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply, Finsupp.coe_update,
  Function.update_same, ne_eq, not_false_eq_true, Function.update_noteq, e]
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
b : ι →₀ ℕ
k : ℕ
⊢ X none ^ k * ∏ x : ι, X (some x) ^ b x = X none ^ k * ∏ x : ι, X (some x) ^ (Finsupp.mapDomain some b) (some x)

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
b : ι →₀ ℕ
k : ℕ
⊢ X none ^ k * ∏ x : ι, X (some x) ^ b x = X none ^ k * ∏ x : ι, X (some x) ^ (Finsupp.mapDomain some b) (some x)
Tactic:
exact congr_arg₂ _ rfl (Finset.prod_congr rfl (fun _ _ => by
  rw [Finsupp.mapDomain_apply (Option.some_injective ι)]))
State after:
no goals

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
b : ι →₀ ℕ
k : ℕ
x✝¹ : ι
x✝ : x✝¹ ∈ Finset.univ
⊢ X (some x✝¹) ^ b x✝¹ = X (some x✝¹) ^ (Finsupp.mapDomain some b) (some x✝¹)
Tactic:
rw [Finsupp.mapDomain_apply (Option.some_injective ι)]
State after:
no goals

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
b : ι →₀ ℕ
k : ℕ
i : ι
⊢ (e b k) (some i) = b i
Tactic:
simp only [Finsupp.update, Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply,
  Finsupp.coe_mk, Function.update, ↓reduceDite,
  Finsupp.mapDomain_apply (Option.some_injective ι), e]
State after:
no goals

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
b : ι →₀ ℕ
k : ℕ
⊢ k = (e b k) none
Tactic:
simp only [Finsupp.update, Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply,
  Finsupp.coe_mk, Function.update, ↓reduceDite, e]
State after:
no goals

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ((coeff fun i => m i) f) d = 0 → φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] 0) = 0
Tactic:
simp only [tmul_zero, map_zero, implies_true]
State after:
no goals

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ((coeff fun i => m i) f) d = 0 → φ ((X none ^ p * ∏ i : ι, X (some i) ^ d i) ⊗ₜ[R] 0) = 0
Tactic:
simp only [tmul_zero, map_zero, implies_true]
State after:
no goals

State before:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
⊢ ¬e d p = e d (d.sum fun x n => n)
Tactic:
intro hd'
State after:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
hd' : e d p = e d (d.sum fun x n => n)
⊢ False

State before:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
hd' : e d p = e d (d.sum fun x n => n)
⊢ False
Tactic:
apply hd
State after:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
hd' : e d p = e d (d.sum fun x n => n)
⊢ (d.sum fun x n => n) = p

State before:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
hd' : e d p = e d (d.sum fun x n => n)
⊢ (d.sum fun x n => n) = p
Tactic:
convert (DFunLike.ext_iff.mp hd'.symm) none <;> exact (he_none _ _)
State after:
no goals

State before:
case hc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (if e d (∑ i : ι, d i) = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d =
    MvPolynomial.coeff (e d (d.sum fun x n => n)) (X none ^ p * ∏ i : ι, X (some i) ^ d i) • ((coeff fun i => m i) f) d
⊢ e d (∑ i : ι, d i) = e d (d.sum fun x n => n)
Tactic:
simp only [Finset.mem_univ, forall_true_left, implies_true,
  Finsupp.sum_of_support_subset _ (Finset.subset_univ d.support)]
State after:
no goals

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0
Tactic:
intro b _ hb'
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
⊢ φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
⊢ φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0
Tactic:
simp only [lcoeff, coe_comp, LinearEquiv.coe_coe, Function.comp_apply, rTensor_tmul, coe_mk,
  AddHom.coe_mk, lid_tmul, φ]
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
⊢ MvPolynomial.coeff (e d (d.sum fun x n => n)) ((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) •
      ((coeff fun i => m i) f) b =
    0

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
⊢ MvPolynomial.coeff (e d (d.sum fun x n => n)) ((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) •
      ((coeff fun i => m i) f) b =
    0
Tactic:
rw [he, coeff_monomial, if_neg, _root_.zero_smul]
State after:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
⊢ ¬e b (∑ i : ι, b i) = e d (d.sum fun x n => n)

State before:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
⊢ ¬e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
Tactic:
intro h
State after:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
⊢ False

State before:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
⊢ False
Tactic:
apply hb'
State after:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
⊢ b = d

State before:
case hnc
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
⊢ b = d
Tactic:
ext i
State after:
case hnc.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
i : ι
⊢ b i = d i

State before:
case hnc.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
i : ι
⊢ b i = d i
Tactic:
rw [← he_some b _ i, h]
State after:
case hnc.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
i : ι
⊢ (e d (d.sum fun x n => n)) (some i) = d i

State before:
case hnc.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
i : ι
⊢ (e d (d.sum fun x n => n)) (some i) = d i
Tactic:
exact he_some d _ i
State after:
no goals