internlm/Lean-Github huggingface dataset:
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
hd' : e d p = e d (d.sum fun x n => n)
⊢ False
Tactic:
apply 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)
⊢ (d.sum fun x n => n) = p
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
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 _ _)
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof 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)]
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)
⊢ ∀ (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'
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)
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
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)
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, φ]
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)
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
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)
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]
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).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)
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).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
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).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
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).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'
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).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
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).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
Proof 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