-- 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
v : HeightOneSpectrum R
n : (WithZero (Multiplicative ℤ))ˣ
h_1 :
  ∃ (a : adicCompletion K v),
    ¬a = 0 ∧
      ∃ (x : adicCompletion K v),
        HMul.hMul (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                a :
              WithZero (Multiplicative ℤ))
            (↑n : WithZero (Multiplicative ℤ)) =
          ((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            x
a : adicCompletion K v
ha0 : ¬a = 0
x : adicCompletion K v
hx :
  HMul.hMul (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (↑n : WithZero (Multiplicative ℤ)) =
    ((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
        (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
      x
b : K
hb :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) b :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
h :
  ∀ (y : K)
    (hy :
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y :
          WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))),
    ∃ (a : K),
      ¬a = 0 ∧
        ∃ (x : K),
          HMul.hMul (α := WithZero (Multiplicative ℤ))
              (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a :
                WithZero (Multiplicative ℤ))
              (↑n : WithZero (Multiplicative ℤ)) =
            ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x
⊢ ∃ (a : K),
    ¬a = 0 ∧
      ∃ (x : K),
        HMul.hMul (α := WithZero (Multiplicative ℤ))
            (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a :
              WithZero (Multiplicative ℤ))
            (↑n : WithZero (Multiplicative ℤ)) =
          ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x

Tactic:
obtain ⟨y, hy⟩ := valuation_surjective K v (Valued.v x)

Premises used: Valued.v, IsDedekindDomain.HeightOneSpectrum.valuation_surjective, DFunLike.coe