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
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)
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)))
                      ⋯,
                  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)
⊢ (↑(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)

Tactic:
simp +instances only [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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
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)

Tactic:
rfl
-- 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
⊢ Eq (α := adicCompletion K v)
    ((↑((algebraMap R ↥(adicCompletionIntegers K v) : (a : R) → ↥(adicCompletionIntegers K v)) r) :
        adicCompletion K v) :
      adicCompletion K v)
    ((↑((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))) :
      UniformSpace.Completion (WithVal (valuation K v)))

Tactic:
rfl
-- 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
inst_6 : FaithfulSMul R K
rw :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := ↥(adicCompletionIntegers K v))
    (⇑(algebraMap R ↥(adicCompletionIntegers K v)) : (a : R) → ↥(adicCompletionIntegers K v))
⊢ FaithfulSMul.{u_1, u_2} R ↥(adicCompletionIntegers K v)

Tactic:
rw [faithfulSMul_iff_algebraMap_injective]

Premises used: faithfulSMul_iff_algebraMap_injective
-- 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
inst_6 : FaithfulSMul R K
x y : R
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
⊢ 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

Tactic:
rw [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- 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
inst_6 : FaithfulSMul R K
x y : R
⊢ 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:
simp
-- 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
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        (↑r : adicCompletion K v) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑r : K) :
      WithZero (Multiplicative ℤ))

Tactic:
Valued.valuedCompletion_apply _

Premises used: UniformSpace.Completion.coe', Valued.valuedCompletion_apply, SeparationQuotient.mk
-- 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
k : K
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (UniformSpace.Completion (WithVal (valuation K v))) (WithZero (Multiplicative ℤ))) :
          (a : UniformSpace.Completion (WithVal (valuation K v))) → WithZero (Multiplicative ℤ))
        (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) k) :
          UniformSpace.Completion (WithVal (valuation K v))) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) k :
      WithZero (Multiplicative ℤ))

Tactic:
Valued.valuedCompletion_apply _

Premises used: Valued.valuedCompletion_apply
-- 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 ℤ)) (↑r : K) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) (↑r : adicCompletion K v)

Tactic:
rw [mem_adicCompletionIntegers, valuedAdicCompletion_eq_valuation]

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation
-- 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 ℤ)) (↑r : K) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
valuation_le_one v r

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

Tactic:
exact valuation_le_one v r

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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ (↑(r • x) : adicCompletion K v) = r • (↑x : adicCompletion K v)

Tactic:
rfl

Premises used: rfl
-- 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
⊢ ∀ (r : R) (m : ↥(adicCompletionIntegers K v)), r • m = 0 → r = 0 ∨ m = 0

Tactic:
simp
-- 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
x : R
y : ↥(adicCompletionIntegers K v)
z : adicCompletion K v
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)
⊢ (x • y) • z = x • y • z

Tactic:
simp only [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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
x : R
y : ↥(adicCompletionIntegers K v)
z : adicCompletion K v
⊢ 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:
apply mul_assoc

Premises used: mul_assoc
-- 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
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))
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))
⊢ ∃ (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

Premises used: IsDedekindDomain.HeightOneSpectrum.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 : adicCompletion K v
ha : Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) a
h :
  Membership.mem (γ := Submonoid R) R⁰ 1 ∧
    Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
      (a * (↑1 : 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:
use 1
-- 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 : Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) a
⊢ Membership.mem (γ := Submonoid R) R⁰ 1 ∧
    Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
      (a * (↑1 : adicCompletion K v))

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 : adicCompletion K v
ha : a ∉ adicCompletionIntegers K v
⊢ 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

Premises used: IsDedekindDomain.HeightOneSpectrum.notMem_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 : 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 ℤ))
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))
⊢ ∃ (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

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_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
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 ℤ))
⊢ 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:
simp [valuedAdicCompletion_eq_valuation, valuation_of_algebraMap, hϖ, exp]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, WithZero.exp
-- 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 ℤ))
⊢ 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]
-- 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 ℤ))
hϖ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) 0 : 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) 0) :
      WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
⊢ False

Tactic:
simp [exp_ne_zero.symm] at hϖ

Premises used: Ne.symm, WithZero.exp_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 : 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 ℤ))
⊢ ϖ ≠ 0

Tactic:
have hϖ0 : ϖ ≠ 0 := by rintro rfl; simp [exp_ne_zero.symm] at hϖ
-- 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
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
        (a * (↑b : adicCompletion K v))

Tactic:
⟨ϖ^(log (Valued.v a)).natAbs, pow_mem (mem_nonZeroDivisors_of_ne_zero hϖ0) _, ?_⟩

Premises used: Valued.v, WithZero.log, HPow.hPow, And.intro, Int.natAbs, Exists.intro, pow_mem, mem_nonZeroDivisors_of_ne_zero, DFunLike.coe