internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
case H.hf.mk
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1
Tactic:
by_cases hn : 0 < n
Proof state after:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : 0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1

case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : ¬0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : 0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1
Tactic:
simp only [if_pos hn, liftAlgHom_apply, LinearMap.zero_apply, aeval_X]
Proof state after:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : 0 < n
⊢ (dividedPowersBot R).dpow n 0 = 0
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : 0 < n
⊢ (dividedPowersBot R).dpow n 0 = 0
Tactic:
rw [DividedPowers.dpow_eval_zero _ (ne_of_gt hn)]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : ¬0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1
Tactic:
rw [if_neg hn]
Proof state after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : ¬0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = 1
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : ¬0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = 1
Tactic:
rw [not_lt, le_zero_iff] at hn
Proof state after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : n = 0
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = 1
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : n = 0
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = 1
Tactic:
simp only [hn, liftAlgHom_apply, LinearMap.zero_apply, aeval_X,
  DividedPowers.dpow_zero _ (mem_bot.mpr rfl)]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.proj'_zero_comp_algebraMap
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ ↑((⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) x) = (algebraMap R (DividedPowerAlgebra R M)) x
Tactic:
simp only [proj', proj, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
  Algebra.algebraMap_eq_smul_one, decompose_smul, decompose_one]
Proof state after:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ ↑((x • 1) 0) = x • 1
Theorem: DividedPowerAlgebra.proj'_zero_comp_algebraMap
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ ↑((x • 1) 0) = x • 1
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_leftInverse
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m : R
⊢ (algebraMapInv R M) ((algebraMap R (DividedPowerAlgebra R M)) m) = m
Tactic:
simp only [AlgHom.commutes, Algebra.id.map_eq_id, RingHom.id_apply]
Proof state after:
no goals
Theorem: MvPolynomial.mkₐ_eq_aeval
Proof state before:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
⊢ mkₐ C I = aeval fun d => (Ideal.Quotient.mk I) (X d)
Tactic:
ext d
Proof state after:
case hf
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : D
⊢ (mkₐ C I) (X d) = (aeval fun d => (Ideal.Quotient.mk I) (X d)) (X d)
Theorem: MvPolynomial.mkₐ_eq_aeval
Proof state before:
case hf
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : D
⊢ (mkₐ C I) (X d) = (aeval fun d => (Ideal.Quotient.mk I) (X d)) (X d)
Tactic:
simp only [mkₐ_eq_mk, aeval_X]
Proof state after:
no goals
Theorem: MvPolynomial.mk_eq_eval₂
Proof state before:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
⊢ (↑↑(Ideal.Quotient.mk I)).toFun = eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) fun d => (Ideal.Quotient.mk I) (X d)
Tactic:
ext d
Proof state after:
case h
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : MvPolynomial D C
⊢ (↑↑(Ideal.Quotient.mk I)).toFun d =
    eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) (fun d => (Ideal.Quotient.mk I) (X d)) d
Theorem: MvPolynomial.mk_eq_eval₂
Proof state before:
case h
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : MvPolynomial D C
⊢ (↑↑(Ideal.Quotient.mk I)).toFun d =
    eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) (fun d => (Ideal.Quotient.mk I) (X d)) d
Tactic:
simp_rw [RingHom.toFun_eq_coe, ← mkₐ_eq_mk C, mkₐ_eq_aeval, aeval_X]
Proof state after:
case h
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : MvPolynomial D C
⊢ (aeval fun d => (Ideal.Quotient.mk I) (X d)) d =
    eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) (fun d => (Ideal.Quotient.mk I) (X d)) d
Theorem: MvPolynomial.mk_eq_eval₂
Proof state before:
case h
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
C : Type u_1
inst✝ : CommRing C
D : Type u_2
I : Ideal (MvPolynomial D C)
d : MvPolynomial D C
⊢ (aeval fun d => (Ideal.Quotient.mk I) (X d)) d =
    eval₂ (algebraMap C (MvPolynomial D C ⧸ I)) (fun d => (Ideal.Quotient.mk I) (X d)) d
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Tactic:
obtain ⟨p, hp0, hpx⟩ := (mem_grade_iff' _ _ _).mp x.2
Proof state after:
case intro.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case intro.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Tactic:
suffices ∃ (a : R), p.val = C a by
  obtain ⟨a, ha⟩ := this
  simp only [← hpx, ha, mk_C, AlgHom.commutes, Algebra.id.map_eq_id, RingHom.id_apply]
Proof state after:
case intro.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ ∃ a, ↑p = C a
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case intro.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ ∃ a, ↑p = C a
Tactic:
use constantCoeff p.val
Proof state after:
case h
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ ↑p = C (constantCoeff ↑p)
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case h
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ ↑p = C (constantCoeff ↑p)
Tactic:
ext exp
Proof state after:
case h.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
⊢ coeff exp ↑p = coeff exp (C (constantCoeff ↑p))
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case h.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
⊢ coeff exp ↑p = coeff exp (C (constantCoeff ↑p))
Tactic:
simp only [coeff_C]
Proof state after:
case h.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
⊢ coeff exp ↑p = if 0 = exp then constantCoeff ↑p else 0
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case h.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
⊢ coeff exp ↑p = if 0 = exp then constantCoeff ↑p else 0
Tactic:
split_ifs with hexp
Proof state after:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : 0 = exp
⊢ coeff exp ↑p = constantCoeff ↑p

case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : 0 = exp
⊢ coeff exp ↑p = constantCoeff ↑p

case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Tactic:
. rw [← hexp, constantCoeff_eq]
Proof state after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Tactic:
. simp only [IsWeightedHomogeneous] at hp0
  by_contra h
  rw [eq_comm, ← Finsupp.support_eq_empty] at hexp
  obtain  ⟨nm, hnm⟩ := nonempty_of_ne_empty hexp
  specialize hp0 h
  simp only [weightedDegree, LinearMap.toAddMonoidHom_coe, Finsupp.total_apply, Finsupp.sum,
    sum_eq_zero_iff] at hp0
  specialize hp0 nm hnm
  simp only [smul_eq_mul, mul_eq_zero] at hp0
  cases' hp0 with hnm0 hnm0
  . simp only [Finsupp.mem_support_iff] at hnm
    exact hnm hnm0
  . apply lt_irrefl 0
    nth_rewrite 2 [← hnm0]
    apply MvPolynomial.mem_supported.mp p.prop
    simp only [mem_coe, mem_vars, Finsupp.mem_support_iff, ne_eq, mem_support_iff, exists_prop]
    simp only [Finsupp.mem_support_iff] at hnm
    exact ⟨exp, h, hnm⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
this : ∃ a, ↑p = C a
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Tactic:
obtain ⟨a, ha⟩ := this
Proof state after:
case intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
a : R
ha : ↑p = C a
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
a : R
ha : ↑p = C a
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Tactic:
simp only [← hpx, ha, mk_C, AlgHom.commutes, Algebra.id.map_eq_id, RingHom.id_apply]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : 0 = exp
⊢ coeff exp ↑p = constantCoeff ↑p
Tactic:
rw [← hexp, constantCoeff_eq]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Tactic:
simp only [IsWeightedHomogeneous] at hp0
Proof state after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Tactic:
by_contra h
Proof state after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
h : ¬coeff exp ↑p = 0
⊢ False
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
h : ¬coeff exp ↑p = 0
⊢ False
Tactic:
rw [eq_comm, ← Finsupp.support_eq_empty] at hexp
Proof state after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
⊢ False
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
⊢ False
Tactic:
obtain  ⟨nm, hnm⟩ := nonempty_of_ne_empty hexp
Proof state after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
⊢ False
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
⊢ False
Tactic:
specialize hp0 h
Proof state after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : (weightedDegree Prod.fst) exp = 0
⊢ False
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : (weightedDegree Prod.fst) exp = 0
⊢ False
Tactic:
simp only [weightedDegree, LinearMap.toAddMonoidHom_coe, Finsupp.total_apply, Finsupp.sum,
  sum_eq_zero_iff] at hp0
Proof state after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : ∀ x ∈ exp.support, exp x • x.1 = 0
⊢ False
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : ∀ x ∈ exp.support, exp x • x.1 = 0
⊢ False
Tactic:
specialize hp0 nm hnm
Proof state after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : exp nm • nm.1 = 0
⊢ False
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof state before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : exp nm • nm.1 = 0
⊢ False
Tactic:
simp only [smul_eq_mul, mul_eq_zero] at hp0
Proof state after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : exp nm = 0 ∨ nm.1 = 0
⊢ False