Theorem: DividedPowerAlgebra.surjective_of_supported' (DividedPowers/DPAlgebra/Graded/Basic.lean)

State before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑p
Tactic:
obtain ⟨p', hpn', hp'⟩ := (mem_grade_iff R M _ _).mpr p.2
State after:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑p

State before:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑p
Tactic:
use toSupported R p'
State after:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ IsWeightedHomogeneous Prod.fst (↑((toSupported R) p')) n ∧ mk ↑((toSupported R) p') = ↑p

State before:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ IsWeightedHomogeneous Prod.fst (↑((toSupported R) p')) n ∧ mk ↑((toSupported R) p') = ↑p
Tactic:
refine ⟨toSupported_isHomogeneous' _ _ _ hpn', ?_⟩
State after:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ mk ↑((toSupported R) p') = ↑p

State before:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ mk ↑((toSupported R) p') = ↑p
Tactic:
erw [DFunLike.congr_fun (mk_comp_toSupported R M) p', hp']
State after:
no goals