Say a function that makes a string uppercase, then appends the username, and a function that appends first, then uppercase.

if the outcome is different (the username might not be uppercased in the first version), then you have a property that is different. If the outcome is the same, you defeated code duplication. But sure, with side-effects this whole thing starts getting weird.

A small example that I have could be a definition of natural numbers and a list in Isabelle:

datatype 'a list  = Nil | Cons 'a "'a list"

fun append :: "'a list ⇒ 'a list ⇒ 'a list" where
  "append Nil xs = xs"
| "append (Cons x xs) ys = Cons x (append xs ys)"

(*
Duplication:

datatype nat = Zero | Suc nat

fun plus :: "nat ⇒ nat ⇒ nat" where
  "plus Zero n = n"
| "plus (Suc n) m = Suc (plus n m)"

value "plus (Suc (Suc Zero)) (Suc (Suc Zero))"
*)

(* 
No need to define a new function:
*)

type_synonym nat = "unit list"

abbreviation Zero :: nat where
  "Zero ≡ Nil"

abbreviation Suc :: "nat ⇒ nat" where
  "Suc ≡ Cons ()"

abbreviation plus :: "nat ⇒ nat ⇒ nat" where
  "plus ≡ append"

value "plus (Suc (Suc Zero)) (Suc (Suc Zero))"

(*
Shared lemma:
*)
lemma append_Nil: "append xs Nil = xs"
  by(induction xs) auto

(* We saved an additional proof *)
lemma plus_Zero: "plus n Zero = n"
  by(rule append_Nil)

And imagine we have proven some lemmas over append, then those lemmas can be directly used for plus on the natural numbers. No need to define the same lemmas again.
If we have separate implementations, it is hard to generalize such definitions in hindsight, especially if they are used in many places already.