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
r : R
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
v.intValuation_le_one r

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_le_one
-- 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
r : R
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
exact v.intValuation_le_one r

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_le_one
-- 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
r : R
rw :
  LT.lt (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ∣ Ideal.span {r}
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑r : K) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ∣ Ideal.span {r}

Tactic:
rw [valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap
-- 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
r : R
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ∣ Ideal.span {r}

Tactic:
v.intValuation_lt_one_iff_dvd r

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd
-- 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
r : R
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ∣ Ideal.span {r}

Tactic:
exact v.intValuation_lt_one_iff_dvd r

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd
-- 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
r : R
rw :
  LT.lt (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    r ∈ v.asIdeal
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑r : K) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    r ∈ v.asIdeal

Tactic:
rw [valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap
-- 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
r : R
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    r ∈ v.asIdeal

Tactic:
v.intValuation_lt_one_iff_mem r

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem
-- 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
r : R
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    r ∈ v.asIdeal

Tactic:
exact v.intValuation_lt_one_iff_mem r

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem
-- 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
r : R
rw :
  LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            ((algebraMap R K : (a : R) → K) r) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) ∧
      LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            ((algebraMap R K : (a : R) → K) r) :
          WithZero (Multiplicative ℤ)) ↔
    ¬LT.lt (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (↑r : K) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) r) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    r ∉ v.asIdeal

Tactic:
rw [← HeightOneSpectrum.valuation_lt_one_iff_mem (K := K), le_antisymm_iff]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, le_antisymm_iff
-- 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
r : R
⊢ LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            ((algebraMap R K : (a : R) → K) r) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) ∧
      LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            ((algebraMap R K : (a : R) → K) r) :
          WithZero (Multiplicative ℤ)) ↔
    ¬LT.lt (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (↑r : K) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [HeightOneSpectrum.valuation_le_one]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_le_one
-- 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 b : R
hb_1 : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hb : b ∉ v.asIdeal
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [valuation_of_algebraMap, intValuation_eq_one_iff.2 hb, intValuation_le_one]

Premises used: Iff.mpr, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
refine :
  ∀
    (hv :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    b ∉ v.asIdeal
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    b ∉ v.asIdeal

Tactic:
refine ⟨fun hv ↦ ?_, fun hb ↦ by
    simp [valuation_of_algebraMap, intValuation_eq_one_iff.2 hb, intValuation_le_one]⟩
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
contrapose! :
  ∀ (hv : b ∈ v.asIdeal),
    LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) :
        WithZero (Multiplicative ℤ))
⊢ b ∉ v.asIdeal

Tactic:
contrapose! hv
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
h_1 : a = 0
⊢ False

Tactic:
simp_all
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
⊢ a ≠ 0

Tactic:
have ha₀ : a ≠ 0 := fun _ ↦ by simp_all
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
⊢ Ne.{u_2 + 1} (α := K) (↑a : K) 0

Tactic:
simp [ha₀]
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
⊢ Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑a : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
have hva : v.valuation K a ≠ 0 := (Valuation.ne_zero_iff _).2 (by simp [ha₀])
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
hva :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑a : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ Ne.{u_2 + 1} (α := K) (↑b : K) 0

Tactic:
simp [hb]
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
hva :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑a : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑b : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
have hvb : v.valuation K b ≠ 0 := (Valuation.ne_zero_iff _).2 (by simp [hb])
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
hva :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑a : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
hvb :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑b : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ HDiv.hDiv (α := K) (↑a : K) (↑b : K) ≠ 0

Tactic:
simp [ha₀, hb]
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
hva :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑a : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
hvb :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑b : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
rw :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑b : K) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑a : K) :
      WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) :
      WithZero (Multiplicative ℤ))

Tactic:
rw [← WithZero.log_lt_log one_ne_zero ((Valuation.ne_zero_iff _).2 (by simp [ha₀, hb])),
    map_div₀, WithZero.log_div hva hvb, WithZero.log_one, Int.sub_pos,
    WithZero.log_lt_log hvb hva]

Premises used: WithZero.log_one, WithZero.log_div, WithZero.log_lt_log, map_div₀, Int.sub_pos, one_ne_zero
-- 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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
hva :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑a : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
hvb :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑b : K) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑b : K) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑a : K) :
      WithZero (Multiplicative ℤ))

Tactic:
simpa [valuation_of_algebraMap, intValuation_eq_one_iff.2 <| h hv, intValuation_lt_one_iff_mem]

Premises used: Iff.mpr, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem
-- 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
have :
  ∀ (π : R)
    (hπ :
      Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))),
    ∃ (π : R),
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (↑π : K) :
          WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑π : K) :
        WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
have ⟨π, hπ⟩ := intValuation_exists_uniformizer v
-- 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
π : R
hπ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑π : K) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑π : K) :
        WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
use π
-- 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
π : R
hπ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑π : K) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
grind [valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap
-- 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
obtain :
  ∀ (r : R)
    (hr :
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (↑r : K) :
          WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))),
    ∃ (π : K),
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
          WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ∃ (π : K),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
        WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨r, hr⟩ := 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
r : R
hr :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑r : K) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
w : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) r) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ ∃ (π : K),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
        WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
use (algebraMap _ _ r)

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
π : K
hπ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ Ne (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ∧
    Ne (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
aesop