A DVR is a valuation ring which is a PID

dvr.lean

import ring_theory.principal_ideal_domain

class DVR (A : Type*) extends principal_ideal_domain A  :=
(val_cond : ∀ x y : A, ∃ z : A, x * z = y ∨ y * z = x) -- i.e. a valuation ring
(nonfield : ∃ u : A, ∀ v : A, u * v ≠ 1) -- or a better formulation

open DVR 

instance local_ring_of_dvr (A : Type*) [DVR A] : local_ring A := 
begin
  split,
  intro a,
  cases val_cond a (1-a) with z hz,
  cases hz,
  {
    left,
    refine ⟨⟨a,1+z,_,_⟩,rfl⟩,
    { 
      rw [mul_add,hz],
      ring,
    },
    {
      rw [mul_comm,mul_add,hz],
      ring,
    }
  },
  {
    right,
    refine ⟨⟨1-a,1+z,_,_⟩,rfl⟩,
    {
      rw [mul_add, hz],
      ring,
    },
    {
      rw [mul_comm,mul_add,hz],
      ring,
    }
  }
end