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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ sub_val evr n (-x) = -sub_val evr n x
Tactic:
induction n with
| zero => simp [sub_val_x_zero]
| succ n ih =>
  cases @eq_zero_or_pos _ _ (evr.valtn x) with
  | inl h' =>
    have h'm : evr.valtn (-x) = 0 := by simp [h']
    rw [sub_val_val_zero evr _ _ h', sub_val_val_zero evr _ _ h'm]
  | inr h' =>
    rw [sub_val_val_pos_succ evr _ _, sub_val_val_pos_succ evr _ _, sub_val_decr_val_comm, ih,
    decr_val_neg, sub_val_decr_val_comm]
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr Nat.zero (-x) = -sub_val evr Nat.zero x
Tactic:
simp [sub_val_x_zero]
State after:
no goals

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Tactic:
cases @eq_zero_or_pos _ _ (evr.valtn x) with
| inl h' =>
  have h'm : evr.valtn (-x) = 0 := by simp [h']
  rw [sub_val_val_zero evr _ _ h', sub_val_val_zero evr _ _ h'm]
| inr h' =>
  rw [sub_val_val_pos_succ evr _ _, sub_val_val_pos_succ evr _ _, sub_val_decr_val_comm, ih,
  decr_val_neg, sub_val_decr_val_comm]
State after:
no goals

State before:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : v evr.valtn x = 0
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Tactic:
have h'm : evr.valtn (-x) = 0 := by simp [h']
State after:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : v evr.valtn x = 0
h'm : v evr.valtn (-x) = 0
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x

State before:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : v evr.valtn x = 0
h'm : v evr.valtn (-x) = 0
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Tactic:
rw [sub_val_val_zero evr _ _ h', sub_val_val_zero evr _ _ h'm]
State after:
no goals

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

State before:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : 0 < v evr.valtn x
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Tactic:
rw [sub_val_val_pos_succ evr _ _, sub_val_val_pos_succ evr _ _, sub_val_decr_val_comm, ih,
decr_val_neg, sub_val_decr_val_comm]
State after:
no goals