-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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})
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))
⊢ 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))

Tactic:
obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)

Premises used: Ideal.span_singleton_le_span_singleton, Ideal.le_of_dvd, Iff.mp, rfl