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
⊢ Surjective ⇑(mk.comp (supported R {nm | 0 < nm.1}).val)
Tactic:
intro f
State after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
⊢ ∃ a, (mk.comp (supported R {nm | 0 < nm.1}).val) a = f

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
f : DividedPowerAlgebra R M
⊢ ∃ a, (mk.comp (supported R {nm | 0 < nm.1}).val) a = f
Tactic:
obtain ⟨p', hp'⟩ := DividedPowerAlgebra.mk_surjective f
State after:
case 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
f : DividedPowerAlgebra R M
p' : MvPolynomial (ℕ × M) R
hp' : mk p' = f
⊢ ∃ a, (mk.comp (supported R {nm | 0 < nm.1}).val) a = f

State before:
case 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
f : DividedPowerAlgebra R M
p' : MvPolynomial (ℕ × M) R
hp' : mk p' = f
⊢ ∃ a, (mk.comp (supported R {nm | 0 < nm.1}).val) a = f
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
f : DividedPowerAlgebra R M
p' : MvPolynomial (ℕ × M) R
hp' : mk p' = f
⊢ (mk.comp (supported R {nm | 0 < nm.1}).val) ((toSupported R) p') = f

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
f : DividedPowerAlgebra R M
p' : MvPolynomial (ℕ × M) R
hp' : mk p' = f
⊢ (mk.comp (supported R {nm | 0 < nm.1}).val) ((toSupported R) p') = f
Tactic:
rw [← AlgHom.comp_apply, AlgHom.comp_assoc, mk_comp_toSupported, ← hp']
State after:
no goals