Theorem: SurjVal.val_pow_ge_of_ge (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 : m ≤ v nav a
⊢ k • m ≤ v nav (a ^ k)
Tactic:
induction k with
| zero => simp [zero_nsmul]
| succ k ih =>
  simp only [succ_nsmul, pow_succ]
  apply val_mul_ge_of_both_ge _ 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 : m ≤ v nav a
⊢ Nat.zero • m ≤ v nav (a ^ Nat.zero)
Tactic:
simp [zero_nsmul]
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 : m ≤ v nav a
k : ℕ
ih : k • m ≤ v nav (a ^ k)
⊢ Nat.succ k • m ≤ v nav (a ^ Nat.succ k)
Tactic:
simp only [succ_nsmul, pow_succ]
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : m ≤ v nav a
k : ℕ
ih : k • m ≤ v nav (a ^ k)
⊢ m + k • m ≤ v nav (a * a ^ k)

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : m ≤ v nav a
k : ℕ
ih : k • m ≤ v nav (a ^ k)
⊢ m + k • m ≤ v nav (a * a ^ k)
Tactic:
apply val_mul_ge_of_both_ge _ ha ih
State after:
no goals