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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
m : ℕ
x : R
h : v evr.valtn x = ↑m
⊢ v evr.valtn (decr_val evr x) = ↑m - 1
Tactic:
cases m with
| zero => rwa [evr.zero_valtn_decr h]
| succ m =>
  have x_pos_val : evr.valtn x > 0 := by
    rw [h]
    exact NeZero.pos _
  simp at * sorry
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = ↑Nat.zero
⊢ v evr.valtn (decr_val evr x) = ↑Nat.zero - 1
Tactic:
rwa [evr.zero_valtn_decr h]
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 = ↑(Nat.succ m)
⊢ v evr.valtn (decr_val evr x) = ↑(Nat.succ m) - 1
Tactic:
have x_pos_val : evr.valtn x > 0 := by
  rw [h]
  exact NeZero.pos _
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
x_pos_val : v evr.valtn x > 0
⊢ v evr.valtn (decr_val evr x) = ↑(Nat.succ m) - 1

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 = ↑(Nat.succ m)
x_pos_val : v evr.valtn x > 0
⊢ v evr.valtn (decr_val evr x) = ↑(Nat.succ m) - 1
Tactic:
simp at *
State after:
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 + 1
x_pos_val : 0 < v evr.valtn x
⊢ v evr.valtn (decr_val evr x) = ↑m + 1 - 1

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 + 1
x_pos_val : 0 < v evr.valtn x
⊢ v evr.valtn (decr_val evr x) = ↑m + 1 - 1
Tactic:
sorry
State after:
no goals

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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
⊢ ↑(Nat.succ m) > 0
Tactic:
exact NeZero.pos _
State after:
no goals