Theorem: SurjVal.val_pow_eq_of_eq (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
k : ℕ
ha : v nav a = m
⊢ v nav (a ^ k) = ↑k * m
Tactic:
induction k with
| zero => simp
| succ k ih =>
  simp only [pow_succ, Nat.cast_succ, add_mul, one_mul, add_comm]
  rw [nav.v_mul_eq_add_v, ha, ih]
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
⊢ v nav (a ^ Nat.zero) = ↑Nat.zero * m
Tactic:
simp
State after:
no goals

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
k : ℕ
ih : v nav (a ^ k) = ↑k * m
⊢ v nav (a ^ Nat.succ k) = ↑(Nat.succ k) * m
Tactic:
simp only [pow_succ, Nat.cast_succ, add_mul, one_mul, add_comm]
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
k : ℕ
ih : v nav (a ^ k) = ↑k * m
⊢ v nav (a * a ^ k) = m + ↑k * m

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
k : ℕ
ih : v nav (a ^ k) = ↑k * m
⊢ v nav (a * a ^ k) = m + ↑k * m
Tactic:
rw [nav.v_mul_eq_add_v, ha, ih]
State after:
no goals