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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ decr_val evr (p * x) = x
Tactic:
have h : (p * x) = p * decr_val evr (p * x) := by
  apply evr.pos_valtn_decr
  rw [evr.valtn.v_mul_eq_add_v, evr.valtn.v_uniformizer]
  rw [add_comm]
  simp
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : p * x = p * decr_val evr (p * x)
⊢ decr_val evr (p * x) = x

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : p * x = p * decr_val evr (p * x)
⊢ decr_val evr (p * x) = x
Tactic:
apply nzero_mul_left_cancel p _ _ (p_non_zero evr.valtn)
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : p * x = p * decr_val evr (p * x)
⊢ p * decr_val evr (p * x) = p * x

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : p * x = p * decr_val evr (p * x)
⊢ p * decr_val evr (p * x) = p * x
Tactic:
exact h.symm
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ p * x = p * decr_val evr (p * x)
Tactic:
apply evr.pos_valtn_decr
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn (p * x) > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn (p * x) > 0
Tactic:
rw [evr.valtn.v_mul_eq_add_v, evr.valtn.v_uniformizer]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ 1 + v evr.valtn x > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ 1 + v evr.valtn x > 0
Tactic:
rw [add_comm]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn x + 1 > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn x + 1 > 0
Tactic:
simp
State after:
no goals