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
a : adicCompletion K v
ha :
  LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
ϖ : R
hϖ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) ϖ : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
this :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) ϖ) :
      WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
hϖ0 : ϖ ≠ 0
neg :
  Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (a *
      (↑(ϖ ^
            Int.natAbs
              (log
                (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                    (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                  a))) :
        adicCompletion K v))
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))

Tactic:
refine ⟨ϖ^(log (Valued.v a)).natAbs, pow_mem (mem_nonZeroDivisors_of_ne_zero hϖ0) _, ?_⟩
-- 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 : adicCompletion K v
ha :
  LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
ϖ : R
hϖ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) ϖ : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
this :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) ϖ) :
      WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
hϖ0 : ϖ ≠ 0
neg :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (exp
          |log
              (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                a)|)⁻¹ ≤
    1
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (a *
      (↑(ϖ ^
            Int.natAbs
              (log
                (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                    (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                  a))) :
        adicCompletion K v))

Tactic:
simp only [map_pow, mem_adicCompletionIntegers, map_mul, this, inv_pow, ← exp_nsmul, nsmul_one,
      Int.natCast_natAbs]

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, map_pow, inv_pow, WithZero.exp_nsmul, map_mul, nsmul_one, Int.natCast_natAbs
-- 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 : adicCompletion K v
ha :
  LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
ϖ : R
hϖ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) ϖ : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
this :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) ϖ) :
      WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
hϖ0 : ϖ ≠ 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (exp
      (log
        (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          a)))
    (exp
      |log
          (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            a)|)

Tactic:
simp [le_abs_self]

Premises used: le_abs_self
-- 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 : adicCompletion K v
ha :
  LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
ϖ : R
hϖ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) ϖ : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
this :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) ϖ) :
      WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
hϖ0 : ϖ ≠ 0
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (exp
          |log
              (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                a)|)⁻¹ ≤
    1

Tactic:
exact mul_inv_le_one_of_le₀ (le_exp_log.trans (by simp [le_abs_self])) zero_le

Premises used: zero_le, mul_inv_le_one_of_le₀
-- 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
⊢ FaithfulSMul.{u_2, u_2} (↥(adicCompletionIntegers K v)) (adicCompletion K v)

Tactic:
Subsemiring.faithfulSMul _

Premises used: Set.Mem, Valuation.valuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Subsemiring.faithfulSMul
-- 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 : ↥(adicCompletionIntegers K v)),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v) :
              (a : ↥(adicCompletionIntegers K v)) → adicCompletion K v)
            x) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [mem_adicCompletionIntegers]

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers
-- 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 : adicCompletion K v⦄,
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            r :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∃ (x : ↥(adicCompletionIntegers K v)),
        (algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v) :
              (a : ↥(adicCompletionIntegers K v)) → adicCompletion K v)
            x =
          r

Tactic:
simp [mem_adicCompletionIntegers]

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers
-- 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 : ↥(adicCompletionIntegers K v)
⊢ IsUnit a ↔
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          (↑a : adicCompletion K v) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [Valuation.Integers.isUnit_iff_valuation_eq_one (integers K v)]

Premises used: IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Valuation.Integers.isUnit_iff_valuation_eq_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 : (adicCompletion K v)ˣ
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        (↑a : adicCompletion K v) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ a ∈
    (↑(Submonoid.comap (F := (adicCompletion K v)ˣ →* adicCompletion K v) (Units.coeHom (adicCompletion K v))
            (Subsemiring.toSubmonoid
              (Subring.toSubsemiring (ValuationSubring.toSubring (adicCompletionIntegers K v)))))⁻¹ :
      Set (adicCompletion K v)ˣ)

Tactic:
simp [mem_adicCompletionIntegers, inv_le_one_iff₀, h.symm.le]

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, inv_le_one_iff₀, Eq.le, Eq.symm
-- 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 : (adicCompletion K v)ˣ
refine :
  ∀
    (h :
      Membership.mem (γ := Subgroup (adicCompletion K v)ˣ)
        (Submonoid.units
          (Subsemiring.toSubmonoid (Subring.toSubsemiring (ValuationSubring.toSubring (adicCompletionIntegers K v)))))
        a),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          (↑a : adicCompletion K v) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := Subgroup (adicCompletion K v)ˣ)
      (Submonoid.units
        (Subsemiring.toSubmonoid (Subring.toSubsemiring (ValuationSubring.toSubring (adicCompletionIntegers K v)))))
      a ↔
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          (↑a : adicCompletion K v) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦
     ⟨h.le, by simp [mem_adicCompletionIntegers, inv_le_one_iff₀, h.symm.le]⟩⟩
-- 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 : (adicCompletion K v)ˣ
h :
  Membership.mem (γ := Subgroup (adicCompletion K v)ˣ)
    (Submonoid.units
      (Subsemiring.toSubmonoid (Subring.toSubsemiring (ValuationSubring.toSubring (adicCompletionIntegers K v)))))
    a
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
        (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
      (↑(↑((Submonoid.unitsEquivIsUnitSubmonoid
                    (Subsemiring.toSubmonoid
                      (Subring.toSubsemiring (ValuationSubring.toSubring (adicCompletionIntegers K v)))) :
                  (a : ↥(adicCompletionIntegers K v).units) →
                    ↥(IsUnit.submonoid ↥(adicCompletionIntegers K v).toSubmonoid))
                (Subtype.mk (p := fun (x : (adicCompletion K v)ˣ) ↦
                  Membership.mem (γ := Subgroup (adicCompletion K v)ˣ)
                    (Submonoid.units
                      (Subsemiring.toSubmonoid
                        (Subring.toSubsemiring (ValuationSubring.toSubring (adicCompletionIntegers K v)))))
                    x)
                  a h)) :
            ↥(adicCompletionIntegers K v).toSubmonoid) :
        adicCompletion K v))
    1

Tactic:
isUnit_iff_valued_eq_one.1 (Submonoid.unitsEquivIsUnitSubmonoid _ ⟨_, h⟩).2

Premises used: Submonoid.unitsEquivIsUnitSubmonoid, Subtype.mk, Iff.mp, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, DFunLike.coe, Subtype.property
-- 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 : (adicCompletion K v)ˣ
h :
  Membership.mem (γ := Subgroup (adicCompletion K v)ˣ)
    (Submonoid.units
      (Subsemiring.toSubmonoid (Subring.toSubsemiring (ValuationSubring.toSubring (adicCompletionIntegers K v)))))
    a
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        (↑a : adicCompletion K v) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
convert! isUnit_iff_valued_eq_one.1 (Submonoid.unitsEquivIsUnitSubmonoid _ ⟨_, h⟩).2

Premises used: Submonoid.unitsEquivIsUnitSubmonoid, Subtype.mk, Iff.mp, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
⊢ Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)

Tactic:
have h_mono := (toNNReal_strictMono hb).monotone
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
h_mono :
  Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
rw :
  LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (x + y)) :
      ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (max ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x)
          ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)
⊢ LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (x + y)) :
      ℝ≥0)
    (max
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x))
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)

Tactic:
rw [← h_mono.map_max]

Premises used: Monotone.map_max
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
h_mono :
  Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
⊢ LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (x + y)) :
      ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (max ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x)
          ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)

Tactic:
h_mono <| v.intValuation.map_add x y

Premises used: Valuation.map_add, IsDedekindDomain.HeightOneSpectrum.intValuation
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
h_mono :
  Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
⊢ LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (x + y)) :
      ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (max ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x)
          ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)

Tactic:
exact h_mono <| v.intValuation.map_add x y

Premises used: Valuation.map_add, IsDedekindDomain.HeightOneSpectrum.intValuation
-- 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
b : ℝ≥0
hb : 1 < b
r : R
x : K
x_1 x_2 : R
⊢ (↑(v.intAdicAbvDef hb (x_1 * x_2)) : ℝ) = (↑(v.intAdicAbvDef hb x_1) : ℝ) * (↑(v.intAdicAbvDef hb x_2) : ℝ)

Tactic:
simp [intAdicAbvDef]

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef
-- 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
b : ℝ≥0
hb : 1 < b
r : R
x : K
x_1 : R
⊢ (↑(v.intAdicAbvDef hb x_1) : ℝ) = 0 ↔ x_1 = 0

Tactic:
simp [intAdicAbvDef, intValuation_def]

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_def, IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
⊢ IsNonarchimedean (R := ℝ) (α := R) (⇑(v.intAdicAbv hb) : (a : R) → ℝ)

Tactic:
isNonarchimedean_intAdicAbvDef v hb

Premises used: IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbvDef, dite, IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef, IsNonarchimedean, NNReal.toReal
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)

Tactic:
simpa [intAdicAbv, intAdicAbvDef, toNNReal_le_one_iff hb] using intValuation_le_one v r

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, WithZeroMulInt.toNNReal_le_one_iff, IsDedekindDomain.HeightOneSpectrum.intAdicAbv, IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal

Tactic:
simpa [intAdicAbv, intAdicAbvDef, toNNReal_lt_one_iff hb] using intValuation_lt_one_iff_mem v r

Premises used: WithZeroMulInt.toNNReal_lt_one_iff, IsDedekindDomain.HeightOneSpectrum.intAdicAbv, IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
contrapose : ¬Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal
⊢ Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∉ v.asIdeal

Tactic:
contrapose
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
rw : LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)
⊢ ¬Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal

Tactic:
rw [← v.intAdicAbv_lt_one_iff hb, ne_iff_lt_iff_le]

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff, ne_iff_lt_iff_le
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)

Tactic:
intAdicAbv_le_one v hb r

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)

Tactic:
exact intAdicAbv_le_one v hb r

Premises used: IsDedekindDomain.HeightOneSpectrum.intAdicAbv_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
b : ℝ≥0
hb : 1 < b
x y : K
⊢ Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)

Tactic:
have h_mono := (toNNReal_strictMono hb).monotone