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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
h : v evr.valtn x = ↑m
⊢ v evr.valtn (sub_val evr n x) = ↑m - ↑n
Tactic:
induction n with
| zero =>
  simpa [sub_val_x_zero]
| succ n ih =>
  cases m with
  | zero =>
    simp only [Nat.zero_eq, CharP.cast_eq_zero, Nat.cast_succ,
      ge_iff_le, zero_le, tsub_eq_zero_of_le] at ih ⊢
    rw [sub_val_val_zero evr x n.succ h]
    exact h
  | succ m =>
    rw [sub_val_val_pos_succ, sub_val_decr_val_comm, val_decr_val evr (sub_val evr n x) ih,
      Nat.succ_eq_add_one n]
    norm_cast
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑m
⊢ v evr.valtn (sub_val evr Nat.zero x) = ↑m - ↑Nat.zero
Tactic:
simpa [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
m : ℕ
h : v evr.valtn x = ↑m
n : ℕ
ih : v evr.valtn (sub_val evr n x) = ↑m - ↑n
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = ↑m - ↑(Nat.succ n)
Tactic:
cases m with
| zero =>
  simp only [Nat.zero_eq, CharP.cast_eq_zero, Nat.cast_succ,
    ge_iff_le, zero_le, tsub_eq_zero_of_le] at ih ⊢
  rw [sub_val_val_zero evr x n.succ h]
  exact h
| succ m =>
  rw [sub_val_val_pos_succ, sub_val_decr_val_comm, val_decr_val evr (sub_val evr n x) ih,
    Nat.succ_eq_add_one n]
  norm_cast
State after:
no goals

State before:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = ↑Nat.zero - ↑n
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = ↑Nat.zero - ↑(Nat.succ n)
Tactic:
simp only [Nat.zero_eq, CharP.cast_eq_zero, Nat.cast_succ,
  ge_iff_le, zero_le, tsub_eq_zero_of_le] at ih ⊢
State after:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = 0

State before:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = 0
Tactic:
rw [sub_val_val_zero evr x n.succ h]
State after:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn x = 0

State before:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn x = 0
Tactic:
exact h
State after:
no goals

State before:
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
ih : v evr.valtn (sub_val evr n x) = ↑(Nat.succ m) - ↑n
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = ↑(Nat.succ m) - ↑(Nat.succ n)
Tactic:
rw [sub_val_val_pos_succ, sub_val_decr_val_comm, val_decr_val evr (sub_val evr n x) ih,
  Nat.succ_eq_add_one n]
State after:
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
ih : v evr.valtn (sub_val evr n x) = ↑(Nat.succ m) - ↑n
⊢ ↑(Sub.sub ↑(Nat.succ m) ↑n) - 1 = ↑(Nat.succ m) - ↑(n + 1)

State before:
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
ih : v evr.valtn (sub_val evr n x) = ↑(Nat.succ m) - ↑n
⊢ ↑(Sub.sub ↑(Nat.succ m) ↑n) - 1 = ↑(Nat.succ m) - ↑(n + 1)
Tactic:
norm_cast
State after:
no goals