awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
mem₁ : LE.le (α := Associates (Ideal R)) (Associates.mk v.asIdeal) (Associates.mk (Ideal.span {π}))
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
have notMem₁ : ¬LE.le (α := Associates (Ideal R)) (Associates.mk (HPow.hPow (β := ℕ) v.asIdeal 2)) (Associates.mk (Ideal.span {π}))
Tactic: rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
Cleared hypotheses: mem, notMem, hπ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : LE.le (α := Associates (Ideal R)) (Associates.mk v.asIdeal) (Associates.mk (Ideal.span {π}))
notMem :
  ¬LE.le (α := Associates (Ideal R)) (Associates.mk (HPow.hPow (β := ℕ) v.asIdeal 2)) (Associates.mk (Ideal.span {π}))
hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
have mem₁ : 1 ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))
Tactic: rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem
Cleared hypotheses: mem, notMem, hπ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : 1 ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))
notMem :
  ¬LE.le (α := Associates (Ideal R)) (Associates.mk (HPow.hPow (β := ℕ) v.asIdeal 2)) (Associates.mk (Ideal.span {π}))
hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
have notMem₁ : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) < 2
Tactic: rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at notMem
Cleared hypotheses: notMem, hπ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have have : ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)),
  ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: classical
  have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
  have hlt : v.asIdeal ^ 2 < v.asIdeal := by
    rw [← Ideal.dvdNotUnit_iff_lt]
    exact ⟨v.ne_bot, v.asIdeal, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩
  obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt
  have hπ : Associates.mk (Ideal.span {π}) ≠ 0 := by
    rw [Associates.mk_ne_zero']
    intro h
    rw [h] at notMem
    exact notMem (Submodule.zero_mem (v.asIdeal ^ 2))
  use π
  rw [intValuation_if_neg _ (Associates.mk_ne_zero'.mp hπ), exp_inj]
  apply congr_arg
  rw [← Int.ofNat_one, Int.natCast_inj]
  rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
  rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem
  rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at notMem
  exact Nat.eq_of_le_of_lt_succ mem notMem
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
have have₁ have₂ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)),
    ∃ (π : R),
      Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have have₃ : ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
  (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal),
  ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: classical
  have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
  have hlt : v.asIdeal ^ 2 < v.asIdeal := by
    rw [← Ideal.dvdNotUnit_iff_lt]
    exact ⟨v.ne_bot, v.asIdeal, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩
  obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt
  have hπ : Associates.mk (Ideal.span {π}) ≠ 0 := by
    rw [Associates.mk_ne_zero']
    intro h
    rw [h] at notMem
    exact notMem (Submodule.zero_mem (v.asIdeal ^ 2))
  use π
  rw [intValuation_if_neg _ (Associates.mk_ne_zero'.mp hπ), exp_inj]
  apply congr_arg
  rw [← Int.ofNat_one, Int.natCast_inj]
  rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
  rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem
  rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at notMem
  exact Nat.eq_of_le_of_lt_succ mem notMem
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
have have₁ have₂ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)),
    ∃ (π : R),
      Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))
have₃ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
    (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal),
    ∃ (π : R),
      Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have have₄ : ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
  (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal) (π : R) (mem : π ∈ v.asIdeal)
  (notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2),
  ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: classical
  have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
  have hlt : v.asIdeal ^ 2 < v.asIdeal := by
    rw [← Ideal.dvdNotUnit_iff_lt]
    exact ⟨v.ne_bot, v.asIdeal, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩
  obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt
  have hπ : Associates.mk (Ideal.span {π}) ≠ 0 := by
    rw [Associates.mk_ne_zero']
    intro h
    rw [h] at notMem
    exact notMem (Submodule.zero_mem (v.asIdeal ^ 2))
  use π
  rw [intValuation_if_neg _ (Associates.mk_ne_zero'.mp hπ), exp_inj]
  apply congr_arg
  rw [← Int.ofNat_one, Int.natCast_inj]
  rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
  rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem
  rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at notMem
  exact Nat.eq_of_le_of_lt_succ mem notMem
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
have have₁ have₂ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)),
    ∃ (π : R),
      Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))
have₃ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
    (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal),
    ∃ (π : R),
      Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))
have₄ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
    (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal) (π : R) (mem : π ∈ v.asIdeal)
    (notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2),
    ∃ (π : R),
      Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have have₅ : ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
  (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal) (π : R) (mem : π ∈ v.asIdeal)
  (notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2)
  (hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0),
  ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: classical
  have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
  have hlt : v.asIdeal ^ 2 < v.asIdeal := by
    rw [← Ideal.dvdNotUnit_iff_lt]
    exact ⟨v.ne_bot, v.asIdeal, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩
  obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt
  have hπ : Associates.mk (Ideal.span {π}) ≠ 0 := by
    rw [Associates.mk_ne_zero']
    intro h
    rw [h] at notMem
    exact notMem (Submodule.zero_mem (v.asIdeal ^ 2))
  use π
  rw [intValuation_if_neg _ (Associates.mk_ne_zero'.mp hπ), exp_inj]
  apply congr_arg
  rw [← Int.ofNat_one, Int.natCast_inj]
  rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
  rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem
  rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at notMem
  exact Nat.eq_of_le_of_lt_succ mem notMem
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
Tactic: rw [v.intValuation_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
  (exp (-1))
Tactic: classical
  rw [v.intValuation_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one]
  exact v.associates_irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
    (exp (-1))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw₁ : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk v.asIdeal))) : ℤ))) (exp (-1))
Tactic: classical
  rw [v.intValuation_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one]
  exact v.associates_irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
    (exp (-1))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk v.asIdeal))) : ℤ)))
    (exp (-1))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw₂ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑1 : ℤ))) (exp (-1))
Tactic: classical
  rw [v.intValuation_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one]
  exact v.associates_irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
    (exp (-1))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk v.asIdeal))) : ℤ)))
    (exp (-1))
rw₂ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑1 : ℤ))) (exp (-1))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw₃ : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
Tactic: classical
  rw [v.intValuation_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one]
  exact v.associates_irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
    (exp (-1))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk v.asIdeal))) : ℤ)))
    (exp (-1))
rw₂ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑1 : ℤ))) (exp (-1))
rw₃ : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-1)) (exp (-1))
Tactic: classical
  rw [v.intValuation_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one]
  exact v.associates_irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
⊢ Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    x ∉ v.asIdeal
have refine : ∀ (h : x ∉ v.asIdeal),
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
Tactic: refine ⟨fun h ↦ by simp [← (intValuation_lt_one_iff_mem _ _).not, h], fun h ↦ ?_⟩
-- 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
r : R
s : ↥(nonZeroDivisors R)
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (IsLocalization.mk' K r s) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R) : WithZero (Multiplicative ℤ))
have rw : ((v.intValuation.extendToLocalization (S := nonZeroDivisors R) sorry K : Valuation K (WithZero (Multiplicative ℤ))) :
      (a : K) → WithZero (Multiplicative ℤ))
    (IsLocalization.mk' K r s) =
  HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R) : WithZero (Multiplicative ℤ))
Tactic: rw [valuation_def, Valuation.extendToLocalization_mk', div_eq_mul_inv]
-- 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
r : R
s : ↥(nonZeroDivisors R)
rw :
  ((v.intValuation.extendToLocalization (S := nonZeroDivisors R) ⋯ K : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      (IsLocalization.mk' K r s) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R) : WithZero (Multiplicative ℤ))
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (IsLocalization.mk' K r s) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R) : WithZero (Multiplicative ℤ))
have rw₁ : HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R))⁻¹ : WithZero (Multiplicative ℤ)) =
  HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R) : WithZero (Multiplicative ℤ))
Tactic: rw [valuation_def, Valuation.extendToLocalization_mk', div_eq_mul_inv]
-- 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
r : R
s : ↥(nonZeroDivisors R)
rw :
  ((v.intValuation.extendToLocalization (S := nonZeroDivisors R) ⋯ K : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      (IsLocalization.mk' K r s) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R) : WithZero (Multiplicative ℤ))
rw₁ :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R))⁻¹ : WithZero (Multiplicative ℤ)) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R) : WithZero (Multiplicative ℤ))
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (IsLocalization.mk' K r s) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R) : WithZero (Multiplicative ℤ))
have rw₂ : HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R))⁻¹ : WithZero (Multiplicative ℤ)) =
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑s : R))⁻¹ : WithZero (Multiplicative ℤ))
Tactic: rw [valuation_def, Valuation.extendToLocalization_mk', div_eq_mul_inv]
-- 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
r : R
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑r : K) :
      WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
have rw : Eq (α := WithZero (Multiplicative ℤ))
  (((v.intValuation.extendToLocalization (S := nonZeroDivisors R) sorry K : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      (↑r : K) :
    WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
Tactic: rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]