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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ (fun x => x + v nav p) (v nav 1) = (fun x => x + v nav p) 0
Tactic:
dsimp
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 + v nav p = 0 + v nav p

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav 1 + v nav p = 0 + v nav p
Tactic:
rw [← v_mul_eq_add_v]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (1 * p) = 0 + v nav p

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ v nav (1 * p) = 0 + v nav p
Tactic:
simp
State after:
no goals

State before:
case inj
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ Function.Injective fun x => x + v nav p
Tactic:
intro x y h
State after:
case inj
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x y : ℕ∞
h : (fun x => x + v nav p) x = (fun x => x + v nav p) y
⊢ x = y

State before:
case inj
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
x y : ℕ∞
h : (fun x => x + v nav p) x = (fun x => x + v nav p) y
⊢ x = y
Tactic:
induction x using ENat.recTopCoe <;>
induction y using ENat.recTopCoe <;>
simp at * <;>
sorry
State after:
no goals