Theorem: ENatValRing.sub_val_decr_val_comm (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 (decr_val evr x) = decr_val evr (sub_val evr n x)
Tactic:
simp [sub_val_eq]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ evr.decr_val^[n] (decr_val evr x) = decr_val evr (evr.decr_val^[n] x)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ evr.decr_val^[n] (decr_val evr x) = decr_val evr (evr.decr_val^[n] x)
Tactic:
rw [← Function.iterate_succ_apply' evr.decr_val]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ evr.decr_val^[n] (decr_val evr x) = evr.decr_val^[Nat.succ n] x

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ evr.decr_val^[n] (decr_val evr x) = evr.decr_val^[Nat.succ n] x
Tactic:
rw [← Function.iterate_succ_apply evr.decr_val]
State after:
no goals