awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
obtain :
  ∀ (a : R)
    (hval :
      LT.lt (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))
        ((↑((unitsWithZeroEquiv : (a : (WithZero (Multiplicative ℤ))ˣ) → Multiplicative ℤ) γ) :
            WithZero (Multiplicative ℤ)) :
          WithZero (Multiplicative ℤ))),
    ∃ (a : R),
      ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
        (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨a, hval⟩ := exists_intValuation_mul_sub_lt v hd' (WithZero.unitsWithZeroEquiv γ)

Premises used: IsDedekindDomain.HeightOneSpectrum.exists_intValuation_mul_sub_lt, WithZero.unitsWithZeroEquiv, DFunLike.coe
-- 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
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))
    ((↑((unitsWithZeroEquiv : (a : (WithZero (Multiplicative ℤ))ˣ) → Multiplicative ℤ) γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))

Tactic:
rw [unitsWithZeroEquiv_apply, coe_unzero] at hval

Premises used: WithZero.coe_unzero, WithZero.unitsWithZeroEquiv_apply
-- 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
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
h :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
    (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))

Tactic:
use a
-- 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
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))
rwa rwa₁ rwa₂ rwa₃ :
  (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
    (↑γ : WithZero (Multiplicative ℤ))

Tactic:
rwa [h]
-- 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
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
    (↑γ : WithZero (Multiplicative ℤ))

Tactic:
suffices h : v.valuation K (algebraMap R K a - x) = v.intValuation (n - a * d) by rwa [h]
-- 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
x : K
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))

Tactic:
rfl

Premises used: rfl
-- 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
x : WithVal (valuation K v)
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        ((WithVal.equiv (valuation K v) : (a : WithVal (valuation K v)) → K) x) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        ((WithVal.equiv (valuation K v) : (a : WithVal (valuation K v)) → K) x) :
      WithZero (Multiplicative ℤ))

Tactic:
rfl

Premises used: rfl
-- 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
x : adicCompletion K v
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((Valued.extensionValuation :
            Valuation (UniformSpace.Completion (WithVal (valuation K v))) (WithZero (Multiplicative ℤ))) :
          (a : UniformSpace.Completion (WithVal (valuation K v))) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Function.Surjective.{u_2 + 1, 1} (α := adicCompletion K v) (β := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : adicCompletion K v) → WithZero (Multiplicative ℤ))

Tactic:
Valued.valuedCompletion_surjective_iff.mpr <| .of_comp (v.valuation_surjective K)

Premises used: Iff.mpr, Valued.valuedCompletion_surjective_iff, Function.Surjective.of_comp, IsDedekindDomain.HeightOneSpectrum.valuation_surjective
-- 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
h :
  ∀ (n : (WithZero (Multiplicative ℤ))ˣ),
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
        (MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v) n ↔
      Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
        (MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v)) n
⊢ MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v =
    MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v)

Tactic:
ext n
-- 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 :
  (∃ (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 : 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
⊢ Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
      (MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v) n ↔
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
      (MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v)) n

Tactic:
simp only [MonoidWithZeroHom.mem_valueGroup_iff_of_comm, ne_eq, map_eq_zero]

Premises used: map_eq_zero, ne_eq, MonoidWithZeroHom.mem_valueGroup_iff_of_comm
-- 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 :
  ∃ (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
ha0 : ¬a = 0
x : K
hx :
  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
⊢ ¬Eq (α := adicCompletion K v)
      ((↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) a) :
          UniformSpace.Completion (WithVal (valuation K v))) :
        UniformSpace.Completion (WithVal (valuation K v)))
      (0 : adicCompletion K v)

Tactic:
simp [ha0]
-- 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 :
  ∃ (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
ha0 : ¬a = 0
x : K
hx :
  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
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) a) :
            UniformSpace.Completion (WithVal (valuation K v))) :
        WithZero (Multiplicative ℤ))
      (↑n : WithZero (Multiplicative ℤ)) =
    ((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
        (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
      (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) x) :
        UniformSpace.Completion (WithVal (valuation K v)))

Tactic:
simp [hx]
-- 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 :
  (∃ (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),
      ∃ (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 : 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 : 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:
refine ⟨fun ⟨a, ha0, x, hx⟩ ↦ ?_, fun ⟨a, ha0, x, hx⟩  ↦ ⟨a, by simp [ha0], x, by simp [hx]⟩⟩
-- 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
h :
  ∀ (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 ℤ))),
    ∃ (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 ⟨b, hb⟩ := valuation_surjective K v (Valued.v a)

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