∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v v_1 : Valuation A Γ)
  (e_v : v = v_1) [hv : v.IsRankOneDiscrete] (π π_1 : A), π = π_1 → v.IsUniformizer π = v_1.IsUniformizer π_1