awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (↑(n - a * d) : K) :
      WithZero (Multiplicative ℤ))
⊢ 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 ℤ))
have 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 ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      ((algebraMap R K : (a : R) → K) (n - a * d)) :
    WithZero (Multiplicative ℤ))
Tactic: rw [← valuation_of_algebraMap (K := K), Algebra.cast, map_sub _ n, map_mul, ← hnd, ← sub_mul,
    map_mul, valuation_of_algebraMap, hd, mul_one, Valuation.map_sub_swap]
-- 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
v : HeightOneSpectrum R
⊢ MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v =
    MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v)
have 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
Tactic: ext n
-- 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
v : HeightOneSpectrum R
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
have 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
Tactic: simp only [MonoidWithZeroHom.mem_valueGroup_iff_of_comm, ne_eq, map_eq_zero]
-- 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
v : HeightOneSpectrum R
n : (WithZero (Multiplicative ℤ))ˣ
⊢ (∃ (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
have 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
Tactic: refine ⟨fun ⟨a, ha0, x, hx⟩ ↦ ?_, fun ⟨a, ha0, x, hx⟩  ↦ ⟨a, by simp [ha0], x, by simp [hx]⟩⟩
-- 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
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
have 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
Tactic: obtain ⟨b, hb⟩ := valuation_surjective K v (Valued.v a)
-- 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
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
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
have 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
Tactic: obtain ⟨y, hy⟩ := valuation_surjective K v (Valued.v x)
-- 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
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
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 ℤ))
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
have h : ¬b = 0
Tactic: refine ⟨b, ?_, y, by simp [hb, hy, hx]⟩
-- 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
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
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 ℤ))
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 ℤ))
⊢ ¬b = 0
have h : b ≠ 0
Tactic: rwa [← ne_eq, ← (valuation K v).ne_zero_iff, hb, Valuation.ne_zero_iff]
-- 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
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 ℤ))
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 ℤ))
h : b ≠ 0
⊢ ¬b = 0
have h₁ : Ne (α := WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) b :
    WithZero (Multiplicative ℤ))
  (0 : WithZero (Multiplicative ℤ))
Tactic: rwa [← ne_eq, ← (valuation K v).ne_zero_iff, hb, Valuation.ne_zero_iff]
-- 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
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 ℤ))
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 ℤ))
h : b ≠ 0
h₁ :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) b :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ ¬b = 0
have h₂ : Ne (α := WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
        (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
      a :
    WithZero (Multiplicative ℤ))
  (0 : WithZero (Multiplicative ℤ))
Tactic: rwa [← ne_eq, ← (valuation K v).ne_zero_iff, hb, Valuation.ne_zero_iff]