∀ {V : Type u_1} (G : SimpleGraph V) (s t : V) [inst : DecidableEq V],
  G.replaceVertex s t =
    { Adj := fun v w => if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
      symm := ⋯, loopless := ⋯ }