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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
cases @eq_zero_or_pos _ _ (evr.valtn x) with
| inl h =>
  have hm : evr.valtn (-x) = 0 := by simp [h]
  rw [evr.zero_valtn_decr h, evr.zero_valtn_decr hm]
| inr h =>
  have hm : evr.valtn (-x) > 0 := by simp [h]
  apply nzero_mul_left_cancel p _ _ (p_non_zero evr.valtn)
  rw [←neg_mul_eq_mul_neg, ←evr.pos_valtn_decr h, ←evr.pos_valtn_decr hm]
State after:
no goals

State before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
have hm : evr.valtn (-x) = 0 := by simp [h]
State after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
hm : v evr.valtn (-x) = 0
⊢ decr_val evr (-x) = -decr_val evr x

State before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
hm : v evr.valtn (-x) = 0
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
rw [evr.zero_valtn_decr h, evr.zero_valtn_decr hm]
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
⊢ v evr.valtn (-x) = 0
Tactic:
simp [h]
State after:
no goals

State before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
have hm : evr.valtn (-x) > 0 := by simp [h]
State after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ decr_val evr (-x) = -decr_val evr x

State before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
apply nzero_mul_left_cancel p _ _ (p_non_zero evr.valtn)
State after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ p * decr_val evr (-x) = p * -decr_val evr x

State before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ p * decr_val evr (-x) = p * -decr_val evr x
Tactic:
rw [←neg_mul_eq_mul_neg, ←evr.pos_valtn_decr h, ←evr.pos_valtn_decr hm]
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
⊢ v evr.valtn (-x) > 0
Tactic:
simp [h]
State after:
no goals