-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
h :
  ∀ (v : HeightOneSpectrum R),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (IsLocalization.mk' K n
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
              hd)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
hx :
  HMul.hMul (β := K)
      (IsLocalization.mk' K n
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))
      ((algebraMap R K : (a : R) → K)
          (↑(n,
                  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x)
                    d hd).2 :
            R) :
        K) =
    (algebraMap R K : (a : R) → K)
      (n, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd).1
hn0 : n ≠ 0
hd0 : d ≠ 0
this : Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {n})
⊢ Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R K))
    (IsLocalization.mk' K n
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))
have obtain : ∀ (z : R)
  (h :
    ∀ (v : HeightOneSpectrum R),
      LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (IsLocalization.mk' K (d * z)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
                hd)) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)))
  (hx :
    HMul.hMul (β := K)
        (IsLocalization.mk' K (d * z)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))
        ((algebraMap R K : (a : R) → K)
            (↑(d * z,
                    Subtype.mk (p := fun (x : R) ↦
                      Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd).2 :
              R) :
          K) =
      (algebraMap R K : (a : R) → K)
        (d * z,
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
              hd).1)
  (hn0 : d * z ≠ 0) (this : Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {d * z})),
  Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R K))
    (IsLocalization.mk' K (d * z)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))
Tactic: obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)
Cleared hypotheses: n, h, hx, hn0, this