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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
⊢ v nav (p ^ n) = ↑n
Tactic:
induction n with
| zero      =>
  rw [pow_zero]
  exact val_of_one nav
| succ n ih =>
  rw [pow_succ, SurjVal.v_mul_eq_add_v nav, ih, SurjVal.v_uniformizer nav]
  simp [Nat.succ_eq_add_one, add_comm]
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (p ^ Nat.zero) = ↑Nat.zero
Tactic:
rw [pow_zero]
State after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 = ↑Nat.zero

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 = ↑Nat.zero
Tactic:
exact val_of_one nav
State after:
no goals

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
ih : v nav (p ^ n) = ↑n
⊢ v nav (p ^ Nat.succ n) = ↑(Nat.succ n)
Tactic:
rw [pow_succ, SurjVal.v_mul_eq_add_v nav, ih, SurjVal.v_uniformizer nav]
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
ih : v nav (p ^ n) = ↑n
⊢ 1 + ↑n = ↑(Nat.succ n)

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
ih : v nav (p ^ n) = ↑n
⊢ 1 + ↑n = ↑(Nat.succ n)
Tactic:
simp [Nat.succ_eq_add_one, add_comm]
State after:
no goals