internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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) μ
Proof 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
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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'
Proof 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
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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))))
Proof 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
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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'
Proof 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
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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φ
Proof 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
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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]
Proof 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)
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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]
Proof 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)
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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 ι)]))
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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 ι)]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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'
Proof 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