Theorem: SurjVal.val_sub_ge_of_ge (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (a - b)
Tactic:
rw [sub_eq_add_neg]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (a + -b)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (a + -b)
Tactic:
apply val_add_ge_of_ge
State after:
case ha
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav a

case hb
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (-b)

State before:
case ha
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav a

case hb
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (-b)
Tactic:
assumption
State after:
case hb
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (-b)

State before:
case hb
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ∞
p : R
nav : SurjVal p
a b : R
ha : n ≤ v nav a
hb : n ≤ v nav b
⊢ n ≤ v nav (-b)
Tactic:
simpa
State after:
no goals