Theorem: ENatValRing.decr_val_zero (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ decr_val evr 0 = 0
Tactic:
have v_decr_zero : p * evr.decr_val 0 = 0 := by
  symm
  apply evr.pos_valtn_decr
  rw [val_zero]
  decide
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p * decr_val evr 0 = 0
⊢ decr_val evr 0 = 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p * decr_val evr 0 = 0
⊢ decr_val evr 0 = 0
Tactic:
rw [mul_eq_zero] at v_decr_zero
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p = 0 ∨ decr_val evr 0 = 0
⊢ decr_val evr 0 = 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p = 0 ∨ decr_val evr 0 = 0
⊢ decr_val evr 0 = 0
Tactic:
exact Or.resolve_left v_decr_zero (p_non_zero evr.valtn)
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ p * decr_val evr 0 = 0
Tactic:
symm
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ 0 = p * decr_val evr 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ 0 = p * decr_val evr 0
Tactic:
apply evr.pos_valtn_decr
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ v evr.valtn 0 > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ v evr.valtn 0 > 0
Tactic:
rw [val_zero]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ ⊤ > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ ⊤ > 0
Tactic:
decide
State after:
no goals