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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (-1) = 0
Tactic:
by_contra
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ False

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ False
Tactic:
have contradiction : nav 1 > 0 := by
  rw [←neg_neg 1, ←one_mul 1, neg_mul_eq_neg_mul, neg_mul_eq_mul_neg, nav.v_mul_eq_add_v]
  simpa [pos_iff_ne_zero]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : v nav 1 > 0
⊢ False

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : v nav 1 > 0
⊢ False
Tactic:
rw [val_of_one] at contradiction
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : 0 > 0
⊢ False

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
contradiction : 0 > 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ v nav 1 > 0
Tactic:
rw [←neg_neg 1, ←one_mul 1, neg_mul_eq_neg_mul, neg_mul_eq_mul_neg, nav.v_mul_eq_add_v]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ v nav (-1) + v nav (-1) > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x✝ : ¬v nav (-1) = 0
⊢ v nav (-1) + v nav (-1) > 0
Tactic:
simpa [pos_iff_ne_zero]
State after:
no goals