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

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

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

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

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

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

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