Theorem: ENatValRing.sub_val_p_mul (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 (p ^ n * x) = x
Tactic:
induction n with
| zero      =>
  rw [pow_zero, one_mul]
  exact sub_val_x_zero evr x
| succ n ih =>
  rwa [sub_val_val_pos_succ evr, pow_succ, mul_assoc, decr_val_p_mul]
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 (p ^ Nat.zero * x) = x
Tactic:
rw [pow_zero, one_mul]
State after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr Nat.zero x = x

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 = x
Tactic:
exact sub_val_x_zero evr x
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 (p ^ n * x) = x
⊢ sub_val evr (Nat.succ n) (p ^ Nat.succ n * x) = x
Tactic:
rwa [sub_val_val_pos_succ evr, pow_succ, mul_assoc, decr_val_p_mul]
State after:
no goals