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 : WithZero (Multiplicative ℤ)
inl :
  ∃ (a : K),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
inr :
  ∀ (x : (WithZero (Multiplicative ℤ))ˣ),
    ∃ (a : K),
      ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a =
        (↑x : WithZero (Multiplicative ℤ))
⊢ ∃ (a : K), ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a = x

Tactic:
rcases GroupWithZero.eq_zero_or_unit x with (rfl | ⟨x, rfl⟩)

Premises used: GroupWithZero.eq_zero_or_unit, 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
⊢ ∃ (a : K),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))

Tactic:
simp
-- 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 : (WithZero (Multiplicative ℤ))ˣ
inr :
  ∀ (π : K)
    (hπ :
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
          WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))),
    ∃ (a : K),
      ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a =
        (↑x : WithZero (Multiplicative ℤ))
⊢ ∃ (a : K),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a =
      (↑x : WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer
-- 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 : (WithZero (Multiplicative ℤ))ˣ
π : K
hπ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ∃ (a : K),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a =
      (↑x : WithZero (Multiplicative ℤ))

Tactic:
⟨π ^ (- log x.val), ?_⟩

Premises used: Units.val, WithZero.log, HPow.hPow, Exists.intro, Neg.neg
-- 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 : (WithZero (Multiplicative ℤ))ˣ
π : K
hπ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
inr :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (π ^ (-(↑x : WithZero (Multiplicative ℤ)).log)) =
    (↑x : WithZero (Multiplicative ℤ))
⊢ ∃ (a : K),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a =
      (↑x : WithZero (Multiplicative ℤ))

Tactic:
refine ⟨π ^ (- log x.val), ?_⟩
-- 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 : (WithZero (Multiplicative ℤ))ˣ
π : K
hπ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (π ^ (-(↑x : WithZero (Multiplicative ℤ)).log)) =
    (↑x : WithZero (Multiplicative ℤ))

Tactic:
simp [hπ, exp_log]

Premises used: WithZero.exp_log
-- 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
⊢ Classical.choose (p := fun (x : K) ↦
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ)))
      ⋯ ≠
    0

Tactic:
haveI hu := Classical.choose_spec (v.valuation_exists_uniformizer K)
  (Valuation.ne_zero_iff _).mp (ne_of_eq_of_ne hu WithZero.coe_ne_zero)

Premises used: WithZero.coe_ne_zero, ne_of_eq_of_ne, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer, Valuation.ne_zero_iff, Classical.choose_spec, IsDedekindDomain.HeightOneSpectrum.valuation, Iff.mp
-- 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
x : K
h :
  ∀ (v : HeightOneSpectrum R),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
obtain :
  ∀ (n d : R) (hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d)
    (hx :
      HMul.hMul (β := K) x
          ((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),
    Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R K)) x
⊢ Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R K)) x

Tactic:
obtain ⟨⟨n, d, hd⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors R) x

Premises used: IsLocalization.surj, nonZeroDivisors
-- 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
x : K
h :
  ∀ (v : HeightOneSpectrum R),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hx :
  HMul.hMul (β := K) x
      ((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
⊢ x =
    IsLocalization.mk' K n
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd)

Tactic:
IsLocalization.eq_mk'_iff_mul_eq.mpr hx

Premises used: Iff.mpr, IsLocalization.eq_mk'_iff_mul_eq
-- 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
x : K
h :
  ∀ (v : HeightOneSpectrum R),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hx :
  HMul.hMul (β := K) x
      ((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
obtain :
  ∀
    (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),
    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))
⊢ Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R K)) x

Tactic:
obtain rfl : x = IsLocalization.mk' K n ⟨d, hd⟩ := IsLocalization.eq_mk'_iff_mul_eq.mpr hx

Premises used: Iff.mpr, Subtype.mk, IsLocalization.mk', IsLocalization.eq_mk'_iff_mul_eq, 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
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 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))

Tactic:
simp
-- 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
⊢ d ≠ 0

Tactic:
have hd0 := nonZeroDivisors.ne_zero hd
-- 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
d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hd0 : d ≠ 0
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})
h₁ :
  ((algebraMap R K : R →+* K) : (a : R) → K) z =
    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 (d * z)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))

Tactic:
use z
-- 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
d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hd0 : d ≠ 0
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})
⊢ 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) z ∨
    Eq.{u_2 + 1} (α := 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).2 :
            R) :
        K)
      (0 : K)

Tactic:
rw [map_mul, mul_comm, mul_eq_mul_left_iff] at hx

Premises used: mul_eq_mul_left_iff, map_mul, mul_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
d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hd0 : d ≠ 0
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})
hx₁ :
  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) z ∨
    Eq.{u_2 + 1} (α := 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).2 :
            R) :
        K)
      (0 : K)
⊢ d * z ≠ 0

Tactic:
rw [map_mul, mul_comm, mul_eq_mul_left_iff] at hx

Premises used: mul_eq_mul_left_iff, map_mul, mul_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
d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hd0 : d ≠ 0
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})
hx₁ :
  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) z ∨
    Eq.{u_2 + 1} (α := 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).2 :
            R) :
        K)
      (0 : K)
hn0₁ : d * z ≠ 0
⊢ Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {d * z})

Tactic:
rw [map_mul, mul_comm, mul_eq_mul_left_iff] at hx

Premises used: mul_eq_mul_left_iff, map_mul, mul_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
d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hd0 : d ≠ 0
z : R
h_1 :
  ∀ (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 :
  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) z ∨
    Eq.{u_2 + 1} (α := 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).2 :
            R) :
        K)
      (0 : K)
hn0 : d * z ≠ 0
this : Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {d * z})
h :
  Eq.{u_2 + 1} (α := 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).2 :
          R) :
      K)
    (0 : K)
⊢ False

Tactic:
simp [hd0] at h