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
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ r • x =
    HMul.hMul (α := ↥(adicCompletionIntegers K v))
      (({
              toFun := fun (r : R) ↦
                Subtype.mk (p := fun (x : adicCompletion K v) ↦
                  Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x)
                  (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
                        ((algebraMap R K : (a : R) → K) r)) :
                    UniformSpace.Completion (WithVal (valuation K v)))
                  ⋯,
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : R) → ↥(adicCompletionIntegers K v))
          r :
        ↥(adicCompletionIntegers K v))
      x
have a : (↑(r • x) : adicCompletion K v) =
  (↑(HMul.hMul (α := ↥(adicCompletionIntegers K v))
        (({
                toFun := fun (r : R) ↦
                  Subtype.mk (p := fun (x : adicCompletion K v) ↦
                    Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x)
                    (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
                          ((algebraMap R K : (a : R) → K) r)) :
                      UniformSpace.Completion (WithVal (valuation K v)))
                    sorry,
                map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
                RingHom.{u_1, u_2} R ↥(adicCompletionIntegers K v) } :
              (a : R) → ↥(adicCompletionIntegers K v))
            r :
          ↥(adicCompletionIntegers K v))
        x) :
    adicCompletion K v)
Tactic: ext
-- 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
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ (↑(r • x) : adicCompletion K v) =
    (↑(HMul.hMul (α := ↥(adicCompletionIntegers K v))
          (({
                  toFun := fun (r : R) ↦
                    Subtype.mk (p := fun (x : adicCompletion K v) ↦
                      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x)
                      (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
                            ((algebraMap R K : (a : R) → K) r)) :
                        UniformSpace.Completion (WithVal (valuation K v)))
                      ⋯,
                  map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  RingHom.{u_1, u_2} R ↥(adicCompletionIntegers K v) } :
                (a : R) → ↥(adicCompletionIntegers K v))
              r :
            ↥(adicCompletionIntegers K v))
          x) :
      adicCompletion K v)
have a : (↑(r • x) : adicCompletion K v) =
  (↑(HMul.hMul (α := ↥(adicCompletionIntegers K v))
        (({
                toFun := fun (r : R) ↦
                  Subtype.mk (p := fun (x : adicCompletion K v) ↦
                    Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x)
                    (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
                          ((algebraMap R K : (a : R) → K) r)) :
                      UniformSpace.Completion (WithVal (valuation K v)))
                    sorry,
                map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
                RingHom.{u_1, u_2} R ↥(adicCompletionIntegers K v) } :
              (a : R) → ↥(adicCompletionIntegers K v))
            r :
          ↥(adicCompletionIntegers K v))
        x) :
    adicCompletion K v)
Tactic: simp +instances only [Algebra.smul_def]
-- 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
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
inst_6 : FaithfulSMul R K
⊢ FaithfulSMul.{u_1, u_2} R ↥(adicCompletionIntegers K v)
have rw : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := ↥(adicCompletionIntegers K v))
  (⇑(algebraMap R ↥(adicCompletionIntegers K v)) : (a : R) → ↥(adicCompletionIntegers K v))
Tactic: rw [faithfulSMul_iff_algebraMap_injective]
-- 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
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
inst_6 : FaithfulSMul R K
x y : R
⊢ Eq.{u_2 + 1} (α := ↥(adicCompletionIntegers K v))
      ((algebraMap R ↥(adicCompletionIntegers K v) : (a : R) → ↥(adicCompletionIntegers K v)) x :
        ↥(adicCompletionIntegers K v))
      ((algebraMap R ↥(adicCompletionIntegers K v) : (a : R) → ↥(adicCompletionIntegers K v)) y :
        ↥(adicCompletionIntegers K v)) →
    x = y
have rw : Eq.{u_2 + 1} (α := adicCompletion K v)
    (↑((algebraMap R ↥(adicCompletionIntegers K v) : (a : R) → ↥(adicCompletionIntegers K v)) x) : adicCompletion K v)
    (↑((algebraMap R ↥(adicCompletionIntegers K v) : (a : R) → ↥(adicCompletionIntegers K v)) y) : adicCompletion K v) →
  x = y
Tactic: rw [Subtype.ext_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
r : R
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) (↑r : adicCompletion K v)
have rw : LE.le (α := WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑r : K) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [mem_adicCompletionIntegers, valuedAdicCompletion_eq_valuation]
-- 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
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
x : R
y : ↥(adicCompletionIntegers K v)
z : adicCompletion K v
⊢ (x • y) • z = x • y • z
have simp : HMul.hMul (α := adicCompletion K v)
    ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v) :
          (a : ↥(adicCompletionIntegers K v)) → adicCompletion K v)
        (HMul.hMul (α := ↥(adicCompletionIntegers K v))
          ((algebraMap R ↥(adicCompletionIntegers K v) : (a : R) → ↥(adicCompletionIntegers K v)) x :
            ↥(adicCompletionIntegers K v))
          y) :
      adicCompletion K v)
    z =
  HMul.hMul (α := adicCompletion K v)
    ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) x : adicCompletion K v)
    (HMul.hMul (α := adicCompletion K v)
      ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v) :
            (a : ↥(adicCompletionIntegers K v)) → adicCompletion K v)
          y :
        adicCompletion K v)
      z)
Tactic: simp only [Algebra.smul_def]
-- 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
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))
have pos : ∀ (ha : Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) a),
  ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))
Tactic: by_cases ha : a ∈ v.adicCompletionIntegers K
-- 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
a : adicCompletion K v
pos :
  ∀ (ha : Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) a),
    ∃ (b : R),
      Membership.mem (γ := Submonoid R) R⁰ b ∧
        Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
          (a * (↑b : 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))
have neg : ∀ (ha : a ∉ adicCompletionIntegers 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: by_cases ha : a ∈ v.adicCompletionIntegers K
-- 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
a : adicCompletion K v
ha : Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) a
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))
have h : Membership.mem (γ := Submonoid R) R⁰ 1 ∧
  Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (a * (↑1 : adicCompletion K v))
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
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 : a ∉ adicCompletionIntegers K v
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))
have 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 ℤ))
Tactic: rw [notMem_adicCompletionIntegers] at ha
Cleared hypotheses: ha
-- 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
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 ℤ))
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))
have neg : ∀ (ϖ : R)
  (hϖ :
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) ϖ : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))),
  ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))
Tactic: obtain ⟨ϖ, hϖ⟩ := intValuation_exists_uniformizer v
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
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 ℤ))
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))
have 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 ℤ))
Tactic: have : Valued.v (algebraMap R (v.adicCompletion K) ϖ) = (exp (1 : ℤ))⁻¹ := by
      simp [valuedAdicCompletion_eq_valuation, valuation_of_algebraMap, hϖ, exp]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
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 ℤ))
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))
have hϖ0 : ϖ ≠ 0
Tactic: have hϖ0 : ϖ ≠ 0 := by rintro rfl; simp [exp_ne_zero.symm] at 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
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
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))
have 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))
Tactic: refine ⟨ϖ^(log (Valued.v a)).natAbs, pow_mem (mem_nonZeroDivisors_of_ne_zero hϖ0) _, ?_⟩
-- 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
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
⊢ 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))
have 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
Tactic: simp only [map_pow, mem_adicCompletionIntegers, map_mul, this, inv_pow, ← exp_nsmul, nsmul_one,
      Int.natCast_natAbs]
-- 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
a : (adicCompletion K v)ˣ
⊢ 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 ℤ))
have 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 ℤ))
Tactic: refine ⟨fun h ↦ ?_, fun h ↦
     ⟨h.le, by simp [mem_adicCompletionIntegers, inv_le_one_iff₀, h.symm.le]⟩⟩
-- 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
b : ℝ≥0
hb : 1 < b
x y : R
⊢ 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)
have h_mono : Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal sorry) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
Tactic: have h_mono := (toNNReal_strictMono hb).monotone
-- 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
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)
    (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)
have rw : LE.le (α := ℝ≥0)
  ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (x + y)) :
    ℝ≥0)
  ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
      (max ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x)
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) y)) :
    ℝ≥0)
Tactic: rw [← h_mono.map_max]
-- 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
b : ℝ≥0
hb : 1 < b
r : R
⊢ Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∉ v.asIdeal
have contrapose : ¬Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal
Tactic: contrapose
-- 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
b : ℝ≥0
hb : 1 < b
r : R
⊢ ¬Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal
have rw : LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)
Tactic: rw [← v.intAdicAbv_lt_one_iff hb, ne_iff_lt_iff_le]