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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : ↑n ≤ v evr.valtn x
⊢ x = p ^ n * sub_val evr n x
Tactic:
induction n with
| zero => simp [sub_val_eq]
| succ n ih =>
  rw [sub_val_val_pos_succ, sub_val_decr_val_comm, pow_succ', mul_assoc]
  have pos_val : evr.valtn (sub_val evr n x) > 0 := by
    have h' := val_sub_val_le evr x n h
    rw [Nat.succ_eq_add_one] at h'
    norm_cast at h'
    rw [Nat.add_sub_self_left] at h'
    exact one_le_iff_pos.mp h'
  rw [←evr.pos_valtn_decr pos_val]
  apply ih
  rw [Nat.cast_succ] at h
  exact le_of_add_le_left h
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : ↑Nat.zero ≤ v evr.valtn x
⊢ x = p ^ Nat.zero * sub_val evr Nat.zero x
Tactic:
simp [sub_val_eq]
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 : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
⊢ x = p ^ Nat.succ n * sub_val evr (Nat.succ n) x
Tactic:
rw [sub_val_val_pos_succ, sub_val_decr_val_comm, pow_succ', mul_assoc]
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
⊢ x = p ^ n * (p * decr_val evr (sub_val evr n x))

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
⊢ x = p ^ n * (p * decr_val evr (sub_val evr n x))
Tactic:
have pos_val : evr.valtn (sub_val evr n x) > 0 := by
  have h' := val_sub_val_le evr x n h
  rw [Nat.succ_eq_add_one] at h'
  norm_cast at h'
  rw [Nat.add_sub_self_left] at h'
  exact one_le_iff_pos.mp h'
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ x = p ^ n * (p * decr_val evr (sub_val evr n x))

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ x = p ^ n * (p * decr_val evr (sub_val evr n x))
Tactic:
rw [←evr.pos_valtn_decr pos_val]
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ x = p ^ n * sub_val evr n x

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ x = p ^ n * sub_val evr n x
Tactic:
apply ih
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ ↑n ≤ v evr.valtn x

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ ↑n ≤ v evr.valtn x
Tactic:
rw [Nat.cast_succ] at h
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑n + 1 ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ ↑n ≤ v evr.valtn x

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑n + 1 ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ ↑n ≤ v evr.valtn x
Tactic:
exact le_of_add_le_left h
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
⊢ v evr.valtn (sub_val evr n x) > 0
Tactic:
have h' := val_sub_val_le evr x n h
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
h' : v evr.valtn (sub_val evr n x) ≥ ↑(Nat.succ n) - ↑n
⊢ v evr.valtn (sub_val evr n x) > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
h' : v evr.valtn (sub_val evr n x) ≥ ↑(Nat.succ n) - ↑n
⊢ v evr.valtn (sub_val evr n x) > 0
Tactic:
rw [Nat.succ_eq_add_one] at h'
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
h' : v evr.valtn (sub_val evr n x) ≥ ↑(n + 1) - ↑n
⊢ v evr.valtn (sub_val evr n x) > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
h' : v evr.valtn (sub_val evr n x) ≥ ↑(n + 1) - ↑n
⊢ v evr.valtn (sub_val evr n x) > 0
Tactic:
norm_cast at h'
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
h' : v evr.valtn (sub_val evr n x) ≥ ↑(n + 1 - n)
⊢ v evr.valtn (sub_val evr n x) > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
h' : v evr.valtn (sub_val evr n x) ≥ ↑(n + 1 - n)
⊢ v evr.valtn (sub_val evr n x) > 0
Tactic:
rw [Nat.add_sub_self_left] at h'
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
h' : v evr.valtn (sub_val evr n x) ≥ ↑1
⊢ v evr.valtn (sub_val evr n x) > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
h' : v evr.valtn (sub_val evr n x) ≥ ↑1
⊢ v evr.valtn (sub_val evr n x) > 0
Tactic:
exact one_le_iff_pos.mp h'
State after:
no goals