internlm/Lean-Github huggingface dataset:
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) ≥ ↑(n + 1) - ↑n
⊢ v evr.valtn (sub_val evr n x) > 0
Tactic:
norm_cast 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
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) ≥ ↑(n + 1 - n)
⊢ v evr.valtn (sub_val evr n x) > 0
Tactic:
rw [Nat.add_sub_self_left] 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) ≥ ↑1
⊢ 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) ≥ ↑1
⊢ v evr.valtn (sub_val evr n x) > 0
Tactic:
exact one_le_iff_pos.mp h'
Proof state after:
no goals
Theorem: ENatValRing.sub_val_p_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ sub_val evr n (p ^ n * x) = x
Tactic:
induction n with
| zero      =>
  rw [pow_zero, one_mul]
  exact sub_val_x_zero evr x
| succ n ih =>
  rwa [sub_val_val_pos_succ evr, pow_succ, mul_assoc, decr_val_p_mul]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_p_mul
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr Nat.zero (p ^ Nat.zero * x) = x
Tactic:
rw [pow_zero, one_mul]
Proof state after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr Nat.zero x = x
Theorem: ENatValRing.sub_val_p_mul
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr Nat.zero x = x
Tactic:
exact sub_val_x_zero evr x
Proof state after:
no goals
Theorem: ENatValRing.sub_val_p_mul
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (p ^ n * x) = x
⊢ sub_val evr (Nat.succ n) (p ^ Nat.succ n * x) = x
Tactic:
rwa [sub_val_val_pos_succ evr, pow_succ, mul_assoc, decr_val_p_mul]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_neg
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ sub_val evr n (-x) = -sub_val evr n x
Tactic:
induction n with
| zero => simp [sub_val_x_zero]
| succ n ih =>
  cases @eq_zero_or_pos _ _ (evr.valtn x) with
  | inl h' =>
    have h'm : evr.valtn (-x) = 0 := by simp [h']
    rw [sub_val_val_zero evr _ _ h', sub_val_val_zero evr _ _ h'm]
  | inr h' =>
    rw [sub_val_val_pos_succ evr _ _, sub_val_val_pos_succ evr _ _, sub_val_decr_val_comm, ih,
    decr_val_neg, sub_val_decr_val_comm]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_neg
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ sub_val evr Nat.zero (-x) = -sub_val evr Nat.zero x
Tactic:
simp [sub_val_x_zero]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_neg
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Tactic:
cases @eq_zero_or_pos _ _ (evr.valtn x) with
| inl h' =>
  have h'm : evr.valtn (-x) = 0 := by simp [h']
  rw [sub_val_val_zero evr _ _ h', sub_val_val_zero evr _ _ h'm]
| inr h' =>
  rw [sub_val_val_pos_succ evr _ _, sub_val_val_pos_succ evr _ _, sub_val_decr_val_comm, ih,
  decr_val_neg, sub_val_decr_val_comm]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_neg
Proof state before:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : v evr.valtn x = 0
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Tactic:
have h'm : evr.valtn (-x) = 0 := by simp [h']
Proof state after:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : v evr.valtn x = 0
h'm : v evr.valtn (-x) = 0
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Theorem: ENatValRing.sub_val_neg
Proof state before:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : v evr.valtn x = 0
h'm : v evr.valtn (-x) = 0
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Tactic:
rw [sub_val_val_zero evr _ _ h', sub_val_val_zero evr _ _ h'm]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_neg
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : v evr.valtn x = 0
⊢ v evr.valtn (-x) = 0
Tactic:
simp [h']
Proof state after:
no goals
Theorem: ENatValRing.sub_val_neg
Proof state before:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : sub_val evr n (-x) = -sub_val evr n x
h' : 0 < v evr.valtn x
⊢ sub_val evr (Nat.succ n) (-x) = -sub_val evr (Nat.succ n) x
Tactic:
rw [sub_val_val_pos_succ evr _ _, sub_val_val_pos_succ evr _ _, sub_val_decr_val_comm, ih,
decr_val_neg, sub_val_decr_val_comm]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_add
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ sub_val evr n (x + y) = sub_val evr n x + sub_val evr n y
Tactic:
apply nzero_mul_left_cancel (p ^ n)
Proof state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n ≠ 0

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n * sub_val evr n (x + y) = p ^ n * (sub_val evr n x + sub_val evr n y)
Theorem: ENatValRing.sub_val_add
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n ≠ 0

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n * sub_val evr n (x + y) = p ^ n * (sub_val evr n x + sub_val evr n y)
Tactic:
. exact pow_ne_zero n (p_non_zero evr.valtn)
Proof state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n * sub_val evr n (x + y) = p ^ n * (sub_val evr n x + sub_val evr n y)
Theorem: ENatValRing.sub_val_add
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n * sub_val evr n (x + y) = p ^ n * (sub_val evr n x + sub_val evr n y)
Tactic:
. rw [← factor_p_of_le_val evr (_ : n ≤ evr.valtn (x + y)), mul_add, ← factor_p_of_le_val evr hx,
    ← factor_p_of_le_val evr hy]
  exact le_trans (le_min hx hy) (evr.valtn.v_add_ge_min_v x y)
Proof state after:
no goals
Theorem: ENatValRing.sub_val_add
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n ≠ 0
Tactic:
exact pow_ne_zero n (p_non_zero evr.valtn)
Proof state after:
no goals
Theorem: ENatValRing.sub_val_add
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ p ^ n * sub_val evr n (x + y) = p ^ n * (sub_val evr n x + sub_val evr n y)
Tactic:
rw [← factor_p_of_le_val evr (_ : n ≤ evr.valtn (x + y)), mul_add, ← factor_p_of_le_val evr hx,
  ← factor_p_of_le_val evr hy]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn (x + y)
Theorem: ENatValRing.sub_val_add
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn (x + y)
Tactic:
exact le_trans (le_min hx hy) (evr.valtn.v_add_ge_min_v x y)
Proof state after:
no goals
Theorem: ENatValRing.sub_val_sub
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ sub_val evr n (x - y) = sub_val evr n x - sub_val evr n y
Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, sub_val_add evr hx, sub_val_neg]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn (-y)
Theorem: ENatValRing.sub_val_sub
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑n ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn (-y)
Tactic:
simpa
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul_left
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ sub_val evr n (x * y) = sub_val evr n x * y
Tactic:
apply nzero_mul_left_cancel (p ^ n)
Proof state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ p ^ n ≠ 0

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ p ^ n * sub_val evr n (x * y) = p ^ n * (sub_val evr n x * y)
Theorem: ENatValRing.sub_val_mul_left
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ p ^ n ≠ 0

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ p ^ n * sub_val evr n (x * y) = p ^ n * (sub_val evr n x * y)
Tactic:
. exact pow_ne_zero n (p_non_zero evr.valtn)
Proof state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ p ^ n * sub_val evr n (x * y) = p ^ n * (sub_val evr n x * y)
Theorem: ENatValRing.sub_val_mul_left
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ p ^ n * sub_val evr n (x * y) = p ^ n * (sub_val evr n x * y)
Tactic:
. rw [← factor_p_of_le_val evr (_ : n ≤ evr.valtn (x * y)), ← mul_assoc,
    ← factor_p_of_le_val evr hx]
  exact le_trans hx (val_mul_ge_left evr.valtn x y)
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul_left
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ p ^ n ≠ 0
Tactic:
exact pow_ne_zero n (p_non_zero evr.valtn)
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul_left
Proof state before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ p ^ n * sub_val evr n (x * y) = p ^ n * (sub_val evr n x * y)
Tactic:
rw [← factor_p_of_le_val evr (_ : n ≤ evr.valtn (x * y)), ← mul_assoc,
  ← factor_p_of_le_val evr hx]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ ↑n ≤ v evr.valtn (x * y)
Theorem: ENatValRing.sub_val_mul_left
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hx : ↑n ≤ v evr.valtn x
⊢ ↑n ≤ v evr.valtn (x * y)
Tactic:
exact le_trans hx (val_mul_ge_left evr.valtn x y)
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul_right
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n : ℕ
hy : ↑n ≤ v evr.valtn y
⊢ sub_val evr n (x * y) = x * sub_val evr n y
Tactic:
rw [mul_comm x y, sub_val_mul_left evr hy, mul_comm]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ sub_val evr n x * sub_val evr m y = sub_val evr (n + m) (x * y)
Tactic:
apply nzero_mul_left_cancel (p ^ (n + m)) _ _ (pow_ne_zero _ (p_non_zero evr.valtn))
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ p ^ (n + m) * (sub_val evr n x * sub_val evr m y) = p ^ (n + m) * sub_val evr (n + m) (x * y)
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ p ^ (n + m) * (sub_val evr n x * sub_val evr m y) = p ^ (n + m) * sub_val evr (n + m) (x * y)
Tactic:
rw [←factor_p_of_le_val evr, pow_add, mul_assoc,
  mul_comm (p ^ m), ← mul_assoc,
  ← mul_assoc,
  ←factor_p_of_le_val evr (_ : n ≤ evr.valtn x), mul_assoc, mul_comm _ (p ^ m),
  ←factor_p_of_le_val evr (_ : m ≤ evr.valtn y)]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑m ≤ v evr.valtn y

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn x

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn (x * y)
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑m ≤ v evr.valtn y

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn x

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn (x * y)
Tactic:
. assumption
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn x

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn (x * y)
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn x

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn (x * y)
Tactic:
. assumption
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn (x * y)
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn (x * y)
Tactic:
. rw [SurjVal.v_mul_eq_add_v]
  exact add_le_add hx hy
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑m ≤ v evr.valtn y
Tactic:
assumption
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑n ≤ v evr.valtn x
Tactic:
assumption
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn (x * y)
Tactic:
rw [SurjVal.v_mul_eq_add_v]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn x + v evr.valtn y
Theorem: ENatValRing.sub_val_mul_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m : ℕ
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ ↑(n + m) ≤ v evr.valtn x + v evr.valtn y
Tactic:
exact add_le_add hx hy
Proof state after:
no goals
Theorem: ENatValRing.sub_val_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x y : R
n m nm : ℕ
h : n + m = nm
hx : ↑n ≤ v evr.valtn x
hy : ↑m ≤ v evr.valtn y
⊢ sub_val evr nm (x * y) = sub_val evr n x * sub_val evr m y
Tactic:
rw [← h, sub_val_mul_sub_val _ _ _ hx hy]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_pow
Proof 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]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_pow
Proof 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]
Proof 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)
Theorem: ENatValRing.sub_val_pow
Proof 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
Proof state after:
no goals
Theorem: ENatValRing.sub_val_pow
Proof 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]
Proof state after:
no goals
Theorem: ENatValRing.sub_val_pow
Proof 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
Proof state after:
no goals
Theorem: ENatValRing.sub_val_pow
Proof 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
Proof 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
Theorem: ENatValRing.sub_val_pow
Proof 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
Proof state after:
no goals
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x
Tactic:
have general : ∀ y : R, sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y := by
  induction m with
  | zero => simp [sub_val_x_zero]
  | succ m ih =>
    intro y
    cases @eq_zero_or_pos _ _ (evr.valtn y) with
    | inl h' => simp [sub_val_val_zero evr y _ h']
    | inr h' =>
      rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
      exact ih (evr.decr_val y)
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
general : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
general : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x
Tactic:
exact general x
Proof state after:
no goals
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
⊢ ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
Tactic:
induction m with
| zero => simp [sub_val_x_zero]
| succ m ih =>
  intro y
  cases @eq_zero_or_pos _ _ (evr.valtn y) with
  | inl h' => simp [sub_val_val_zero evr y _ h']
  | inr h' =>
    rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
    exact ih (evr.decr_val y)
Proof state after:
no goals
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ ∀ (y : R), sub_val evr n (sub_val evr Nat.zero y) = sub_val evr (Nat.zero + n) y
Tactic:
simp [sub_val_x_zero]
Proof state after:
no goals