Theorem: DividedPowerAlgebra.dp_mem_augIdeal_iff (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
inst✝ : Nontrivial R
n : ℕ
m : M
⊢ dp R n m ∈ augIdeal R M ↔ 0 < n
Tactic:
rw [mem_augIdeal_iff, dp, algebraMapInv_eq, aeval_X]
State after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
inst✝ : Nontrivial R
n : ℕ
m : M
⊢ (if 0 < (n, m).1 then 0 else 1) = 0 ↔ 0 < n

State before:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : DecidableEq R
inst✝¹ : DecidableEq M
inst✝ : Nontrivial R
n : ℕ
m : M
⊢ (if 0 < (n, m).1 then 0 else 1) = 0 ↔ 0 < n
Tactic:
simp only [ite_eq_left_iff, not_not, one_ne_zero, imp_false]
State after:
no goals