Theorem: DividedPowerAlgebra.mem_grade_iff (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
a : DividedPowerAlgebra R M
n : ℕ
⊢ a ∈ grade R M n ↔ ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst n, mk p = a
Tactic:
simp only [grade, _root_.quotSubmodule, Submodule.mem_map]
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
a : DividedPowerAlgebra R M
n : ℕ
⊢ (∃ y ∈ weightedHomogeneousSubmodule R Prod.fst n, (mkAlgHom R (Rel R M)) y = a) ↔
    ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst n, mk p = a

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
a : DividedPowerAlgebra R M
n : ℕ
⊢ (∃ y ∈ weightedHomogeneousSubmodule R Prod.fst n, (mkAlgHom R (Rel R M)) y = a) ↔
    ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst n, mk p = a
Tactic:
rfl
State after:
no goals