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

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))
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)

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)]
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)

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
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)

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
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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

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
State after:
no goals