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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) = v nav a
Tactic:
apply le_antisymm
State after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) ≤ v nav a

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)

State before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) ≤ v nav a

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
Tactic:
. apply le_of_not_lt
  intro h'
  have hm : nav a < nav (-b) := by rwa [val_neg]
  apply lt_irrefl (nav a)
  apply lt_of_lt_of_le (lt_min h' hm)
  convert nav.v_add_ge_min_v (a + b) (-b)
  simp
State after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)

State before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
Tactic:
. exact le_trans (le_min (le_of_eq rfl) (le_of_lt h)) (SurjVal.v_add_ge_min_v nav a b)
State after:
no goals

State before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav (a + b) ≤ v nav a
Tactic:
apply le_of_not_lt
State after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ ¬v nav a < v nav (a + b)

State before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ ¬v nav a < v nav (a + b)
Tactic:
intro h'
State after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
⊢ False

State before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
⊢ False
Tactic:
have hm : nav a < nav (-b) := by rwa [val_neg]
State after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ False

State before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ False
Tactic:
apply lt_irrefl (nav a)
State after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ v nav a < v nav a

State before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ v nav a < v nav a
Tactic:
apply lt_of_lt_of_le (lt_min h' hm)
State after:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ min (v nav (a + b)) (v nav (-b)) ≤ v nav a

State before:
case a.h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ min (v nav (a + b)) (v nav (-b)) ≤ v nav a
Tactic:
convert nav.v_add_ge_min_v (a + b) (-b)
State after:
case h.e'_4.h.e'_6
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ a = a + b + -b

State before:
case h.e'_4.h.e'_6
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
hm : v nav a < v nav (-b)
⊢ a = a + b + -b
Tactic:
simp
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
h' : v nav a < v nav (a + b)
⊢ v nav a < v nav (-b)
Tactic:
rwa [val_neg]
State after:
no goals

State before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
a b : R
h : v nav a < v nav b
⊢ v nav a ≤ v nav (a + b)
Tactic:
exact le_trans (le_min (le_of_eq rfl) (le_of_lt h)) (SurjVal.v_add_ge_min_v nav a b)
State after:
no goals