internlm/Lean-Github huggingface dataset:
Theorem: ENatValRing.decr_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ decr_val evr 0 = 0
Tactic:
have v_decr_zero : p * evr.decr_val 0 = 0 := by
  symm
  apply evr.pos_valtn_decr
  rw [val_zero]
  decide
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p * decr_val evr 0 = 0
⊢ decr_val evr 0 = 0
Theorem: ENatValRing.decr_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p * decr_val evr 0 = 0
⊢ decr_val evr 0 = 0
Tactic:
rw [mul_eq_zero] at v_decr_zero
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p = 0 ∨ decr_val evr 0 = 0
⊢ decr_val evr 0 = 0
Theorem: ENatValRing.decr_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p = 0 ∨ decr_val evr 0 = 0
⊢ decr_val evr 0 = 0
Tactic:
exact Or.resolve_left v_decr_zero (p_non_zero evr.valtn)
Proof state after:
no goals
Theorem: ENatValRing.decr_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ p * decr_val evr 0 = 0
Tactic:
symm
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ 0 = p * decr_val evr 0
Theorem: ENatValRing.decr_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ 0 = p * decr_val evr 0
Tactic:
apply evr.pos_valtn_decr
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ v evr.valtn 0 > 0
Theorem: ENatValRing.decr_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ v evr.valtn 0 > 0
Tactic:
rw [val_zero]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ ⊤ > 0
Theorem: ENatValRing.decr_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ ⊤ > 0
Tactic:
decide
Proof state after:
no goals
Theorem: ENatValRing.decr_val_neg
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
cases @eq_zero_or_pos _ _ (evr.valtn x) with
| inl h =>
  have hm : evr.valtn (-x) = 0 := by simp [h]
  rw [evr.zero_valtn_decr h, evr.zero_valtn_decr hm]
| inr h =>
  have hm : evr.valtn (-x) > 0 := by simp [h]
  apply nzero_mul_left_cancel p _ _ (p_non_zero evr.valtn)
  rw [←neg_mul_eq_mul_neg, ←evr.pos_valtn_decr h, ←evr.pos_valtn_decr hm]
Proof state after:
no goals
Theorem: ENatValRing.decr_val_neg
Proof state before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
have hm : evr.valtn (-x) = 0 := by simp [h]
Proof state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
hm : v evr.valtn (-x) = 0
⊢ decr_val evr (-x) = -decr_val evr x
Theorem: ENatValRing.decr_val_neg
Proof state before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
hm : v evr.valtn (-x) = 0
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
rw [evr.zero_valtn_decr h, evr.zero_valtn_decr hm]
Proof state after:
no goals
Theorem: ENatValRing.decr_val_neg
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
⊢ v evr.valtn (-x) = 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: ENatValRing.decr_val_neg
Proof state before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
have hm : evr.valtn (-x) > 0 := by simp [h]
Proof state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ decr_val evr (-x) = -decr_val evr x
Theorem: ENatValRing.decr_val_neg
Proof state before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ decr_val evr (-x) = -decr_val evr x
Tactic:
apply nzero_mul_left_cancel p _ _ (p_non_zero evr.valtn)
Proof state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ p * decr_val evr (-x) = p * -decr_val evr x
Theorem: ENatValRing.decr_val_neg
Proof state before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ p * decr_val evr (-x) = p * -decr_val evr x
Tactic:
rw [←neg_mul_eq_mul_neg, ←evr.pos_valtn_decr h, ←evr.pos_valtn_decr hm]
Proof state after:
no goals
Theorem: ENatValRing.decr_val_neg
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
⊢ v evr.valtn (-x) > 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: ENatValRing.decr_val_p_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ decr_val evr (p * x) = x
Tactic:
have h : (p * x) = p * decr_val evr (p * x) := by
  apply evr.pos_valtn_decr
  rw [evr.valtn.v_mul_eq_add_v, evr.valtn.v_uniformizer]
  rw [add_comm]
  simp
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : p * x = p * decr_val evr (p * x)
⊢ decr_val evr (p * x) = x
Theorem: ENatValRing.decr_val_p_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : p * x = p * decr_val evr (p * x)
⊢ decr_val evr (p * x) = x
Tactic:
apply nzero_mul_left_cancel p _ _ (p_non_zero evr.valtn)
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : p * x = p * decr_val evr (p * x)
⊢ p * decr_val evr (p * x) = p * x
Theorem: ENatValRing.decr_val_p_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : p * x = p * decr_val evr (p * x)
⊢ p * decr_val evr (p * x) = p * x
Tactic:
exact h.symm
Proof state after:
no goals
Theorem: ENatValRing.decr_val_p_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ p * x = p * decr_val evr (p * x)
Tactic:
apply evr.pos_valtn_decr
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn (p * x) > 0
Theorem: ENatValRing.decr_val_p_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn (p * x) > 0
Tactic:
rw [evr.valtn.v_mul_eq_add_v, evr.valtn.v_uniformizer]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ 1 + v evr.valtn x > 0
Theorem: ENatValRing.decr_val_p_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ 1 + v evr.valtn x > 0
Tactic:
rw [add_comm]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn x + 1 > 0
Theorem: ENatValRing.decr_val_p_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn x + 1 > 0
Tactic:
simp
Proof state after:
no goals
Theorem: ENatValRing.sub_val_zero_n
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
n : ℕ
⊢ sub_val evr n 0 = 0
Tactic:
induction n with
| zero => simp [sub_val_eq]
| succ n ih => simpa [sub_val_eq, decr_val_zero] using ih
Proof state after:
no goals
Theorem: ENatValRing.sub_val_zero_n
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ sub_val evr Nat.zero 0 = 0
Tactic:
simp [sub_val_eq]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_zero_n
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
n : ℕ
ih : sub_val evr n 0 = 0
⊢ sub_val evr (Nat.succ n) 0 = 0
Tactic:
simpa [sub_val_eq, decr_val_zero] using ih
Proof state after:
no goals
Theorem: ENatValRing.sub_val_x_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr 0 x = x
Tactic:
simp [sub_val_eq]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = 0
⊢ sub_val evr m x = x
Tactic:
induction m with
| zero => exact sub_val_x_zero evr x
| succ m ih => simpa [sub_val_eq, zero_valtn_decr _ h] using ih
Proof state after:
no goals
Theorem: ENatValRing.sub_val_val_zero
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
⊢ sub_val evr Nat.zero x = x
Tactic:
exact sub_val_x_zero evr x
Proof state after:
no goals
Theorem: ENatValRing.sub_val_val_zero
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
m : ℕ
ih : sub_val evr m x = x
⊢ sub_val evr (Nat.succ m) x = x
Tactic:
simpa [sub_val_eq, zero_valtn_decr _ h] using ih
Proof state after:
no goals
Theorem: ENatValRing.sub_val_val_pos_succ
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
⊢ sub_val evr (Nat.succ m) x = sub_val evr m (decr_val evr x)
Tactic:
simp [sub_val_eq]
Proof state after:
no goals
Theorem: ENatValRing.val_decr_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
m : ℕ
x : R
h : v evr.valtn x = ↑m
⊢ v evr.valtn (decr_val evr x) = ↑m - 1
Tactic:
cases m with
| zero => rwa [evr.zero_valtn_decr h]
| succ m =>
  have x_pos_val : evr.valtn x > 0 := by
    rw [h]
    exact NeZero.pos _
  simp at * sorry
Proof state after:
no goals
Theorem: ENatValRing.val_decr_val
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = ↑Nat.zero
⊢ v evr.valtn (decr_val evr x) = ↑Nat.zero - 1
Tactic:
rwa [evr.zero_valtn_decr h]
Proof state after:
no goals
Theorem: ENatValRing.val_decr_val
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
⊢ v evr.valtn (decr_val evr x) = ↑(Nat.succ m) - 1
Tactic:
have x_pos_val : evr.valtn x > 0 := by
  rw [h]
  exact NeZero.pos _
Proof state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
x_pos_val : v evr.valtn x > 0
⊢ v evr.valtn (decr_val evr x) = ↑(Nat.succ m) - 1
Theorem: ENatValRing.val_decr_val
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
x_pos_val : v evr.valtn x > 0
⊢ v evr.valtn (decr_val evr x) = ↑(Nat.succ m) - 1
Tactic:
simp at *
Proof state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑m + 1
x_pos_val : 0 < v evr.valtn x
⊢ v evr.valtn (decr_val evr x) = ↑m + 1 - 1
Theorem: ENatValRing.val_decr_val
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑m + 1
x_pos_val : 0 < v evr.valtn x
⊢ v evr.valtn (decr_val evr x) = ↑m + 1 - 1
Tactic:
sorry
Proof state after:
no goals
Theorem: ENatValRing.val_decr_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
⊢ v evr.valtn x > 0
Tactic:
rw [h]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
⊢ ↑(Nat.succ m) > 0
Theorem: ENatValRing.val_decr_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
⊢ ↑(Nat.succ m) > 0
Tactic:
exact NeZero.pos _
Proof state after:
no goals
Theorem: ENatValRing.sub_val_decr_val_comm
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ sub_val evr n (decr_val evr x) = decr_val evr (sub_val evr n x)
Tactic:
simp [sub_val_eq]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ evr.decr_val^[n] (decr_val evr x) = decr_val evr (evr.decr_val^[n] x)
Theorem: ENatValRing.sub_val_decr_val_comm
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ evr.decr_val^[n] (decr_val evr x) = decr_val evr (evr.decr_val^[n] x)
Tactic:
rw [← Function.iterate_succ_apply' evr.decr_val]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ evr.decr_val^[n] (decr_val evr x) = evr.decr_val^[Nat.succ n] x
Theorem: ENatValRing.sub_val_decr_val_comm
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ evr.decr_val^[n] (decr_val evr x) = evr.decr_val^[Nat.succ n] x
Tactic:
rw [← Function.iterate_succ_apply evr.decr_val]
Proof state after:
no goals
Theorem: ENatValRing.val_sub_val_eq
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
h : v evr.valtn x = ↑m
⊢ v evr.valtn (sub_val evr n x) = ↑m - ↑n
Tactic:
induction n with
| zero =>
  simpa [sub_val_x_zero]
| succ n ih =>
  cases m with
  | zero =>
    simp only [Nat.zero_eq, CharP.cast_eq_zero, Nat.cast_succ,
      ge_iff_le, zero_le, tsub_eq_zero_of_le] at ih ⊢
    rw [sub_val_val_zero evr x n.succ h]
    exact h
  | succ m =>
    rw [sub_val_val_pos_succ, sub_val_decr_val_comm, val_decr_val evr (sub_val evr n x) ih,
      Nat.succ_eq_add_one n]
    norm_cast
Proof state after:
no goals
Theorem: ENatValRing.val_sub_val_eq
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑m
⊢ v evr.valtn (sub_val evr Nat.zero x) = ↑m - ↑Nat.zero
Tactic:
simpa [sub_val_x_zero]
Proof state after:
no goals
Theorem: ENatValRing.val_sub_val_eq
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m : ℕ
h : v evr.valtn x = ↑m
n : ℕ
ih : v evr.valtn (sub_val evr n x) = ↑m - ↑n
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = ↑m - ↑(Nat.succ n)
Tactic:
cases m with
| zero =>
  simp only [Nat.zero_eq, CharP.cast_eq_zero, Nat.cast_succ,
    ge_iff_le, zero_le, tsub_eq_zero_of_le] at ih ⊢
  rw [sub_val_val_zero evr x n.succ h]
  exact h
| succ m =>
  rw [sub_val_val_pos_succ, sub_val_decr_val_comm, val_decr_val evr (sub_val evr n x) ih,
    Nat.succ_eq_add_one n]
  norm_cast
Proof state after:
no goals
Theorem: ENatValRing.val_sub_val_eq
Proof state before:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = ↑Nat.zero - ↑n
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = ↑Nat.zero - ↑(Nat.succ n)
Tactic:
simp only [Nat.zero_eq, CharP.cast_eq_zero, Nat.cast_succ,
  ge_iff_le, zero_le, tsub_eq_zero_of_le] at ih ⊢
Proof state after:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = 0
Theorem: ENatValRing.val_sub_val_eq
Proof state before:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = 0
Tactic:
rw [sub_val_val_zero evr x n.succ h]
Proof state after:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn x = 0
Theorem: ENatValRing.val_sub_val_eq
Proof state before:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
h : v evr.valtn x = ↑Nat.zero
ih : v evr.valtn (sub_val evr n x) = 0
⊢ v evr.valtn x = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: ENatValRing.val_sub_val_eq
Proof state before:
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
ih : v evr.valtn (sub_val evr n x) = ↑(Nat.succ m) - ↑n
⊢ v evr.valtn (sub_val evr (Nat.succ n) x) = ↑(Nat.succ m) - ↑(Nat.succ n)
Tactic:
rw [sub_val_val_pos_succ, sub_val_decr_val_comm, val_decr_val evr (sub_val evr n x) ih,
  Nat.succ_eq_add_one n]
Proof state after:
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
ih : v evr.valtn (sub_val evr n x) = ↑(Nat.succ m) - ↑n
⊢ ↑(Sub.sub ↑(Nat.succ m) ↑n) - 1 = ↑(Nat.succ m) - ↑(n + 1)
Theorem: ENatValRing.val_sub_val_eq
Proof state before:
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
h : v evr.valtn x = ↑(Nat.succ m)
ih : v evr.valtn (sub_val evr n x) = ↑(Nat.succ m) - ↑n
⊢ ↑(Sub.sub ↑(Nat.succ m) ↑n) - 1 = ↑(Nat.succ m) - ↑(n + 1)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: ENatValRing.val_sub_val_le
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
h : ↑m ≤ v evr.valtn x
⊢ v evr.valtn (sub_val evr n x) ≥ ↑m - ↑n
Tactic:
sorry
Proof state after:
no goals
Theorem: ENatValRing.factor_p_of_le_val
Proof 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
Proof state after:
no goals
Theorem: ENatValRing.factor_p_of_le_val
Proof 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]
Proof state after:
no goals
Theorem: ENatValRing.factor_p_of_le_val
Proof 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]
Proof 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))
Theorem: ENatValRing.factor_p_of_le_val
Proof 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'
Proof 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))
Theorem: ENatValRing.factor_p_of_le_val
Proof 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]
Proof 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
Theorem: ENatValRing.factor_p_of_le_val
Proof 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
Proof 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
Theorem: ENatValRing.factor_p_of_le_val
Proof 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
Proof 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
Theorem: ENatValRing.factor_p_of_le_val
Proof 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
Proof state after:
no goals
Theorem: ENatValRing.factor_p_of_le_val
Proof 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
Proof 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
Theorem: ENatValRing.factor_p_of_le_val
Proof 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'
Proof 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