-- 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
inl :
  ∀
    (h :
      ∀ (v : HeightOneSpectrum R),
        LE.le (α := WithZero (Multiplicative ℤ))
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
              (IsLocalization.mk' K 0
                (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 0
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
              hd))
          ((algebraMap R K : (a : R) → K)
              (↑(0,
                      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)
          (0,
              Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
                hd).1),
    Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R K))
      (IsLocalization.mk' K 0
        (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))
have inr : ∀ (hn0 : n ≠ 0),
  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 rfl | hn0 := eq_or_ne n 0