Theorem: ENatValRing.sub_val_pow (ECTate/Algebra/ValuedRing.lean)

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
nm : ℕ
h : Nat.zero * n = nm
⊢ sub_val evr nm (x ^ Nat.zero) = sub_val evr n x ^ Nat.zero
Tactic:
simp [← h]
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 : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ sub_val evr nm (x ^ Nat.succ k) = sub_val evr n x ^ Nat.succ k
Tactic:
rw [pow_succ, sub_val_mul _ n (k * n), pow_succ, ← ih]
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ k * n = k * n

case succ.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ n + k * n = nm

case succ.hx
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ ↑n ≤ v evr.valtn x

case succ.hy
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ ↑(k * n) ≤ v evr.valtn (x ^ k)

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ k * n = k * n
Tactic:
rfl
State after:
no goals

State before:
case succ.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ n + k * n = nm
Tactic:
rw [← h, Nat.succ_mul, add_comm]
State after:
no goals

State before:
case succ.hx
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ ↑n ≤ v evr.valtn x
Tactic:
exact hx
State after:
no goals

State before:
case succ.hy
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ ↑(k * n) ≤ v evr.valtn (x ^ k)
Tactic:
convert val_pow_ge_of_ge evr.valtn k hx
State after:
case h.e'_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ ↑(k * n) = k • ↑n

State before:
case h.e'_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
k : ℕ
ih : ∀ {nm : ℕ}, k * n = nm → sub_val evr nm (x ^ k) = sub_val evr n x ^ k
nm : ℕ
h : Nat.succ k * n = nm
⊢ ↑(k * n) = k • ↑n
Tactic:
simp
State after:
no goals