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
inst_6 : Algebra S K
⊢ Eq (α := (a : S) → adicCompletion K v) (⇑(algebraMap S (adicCompletion K v)) : (a : S) → adicCompletion K v)
    ((fun (x : K) ↦
        (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) x) :
          UniformSpace.Completion (WithVal (valuation K v)))) ∘
      (⇑(algebraMap S K) : (a : S) → K))

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, 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
⊢ DenseRange (X := adicCompletion K v) (α := K) (⇑(algebraMap K (adicCompletion K v)) : (a : K) → adicCompletion K v)

Tactic:
UniformSpace.Completion.denseRange_coe.comp (WithVal.equiv _).symm.surjective.denseRange
    (UniformSpace.Completion.continuous_coe _)

Premises used: UniformSpace.Completion.coe', RingEquiv.surjective, Function.Surjective.denseRange, UniformSpace.Completion.denseRange_coe, WithVal.equiv, UniformSpace.Completion.continuous_coe, SeparationQuotient.mk, DenseRange.comp, RingEquiv.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
r : R
rw :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (WithVal (valuation K v)) (WithZero (Multiplicative ℤ))) :
          (a : WithVal (valuation K v)) → WithZero (Multiplicative ℤ))
        ((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
          ((algebraMap R K : (a : R) → K) r)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Membership.mem (α := adicCompletion K v) (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers 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:
rw [mem_adicCompletionIntegers, Valued.valuedCompletion_apply]

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, 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
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (WithVal (valuation K v)) (WithZero (Multiplicative ℤ))) :
          (a : WithVal (valuation K v)) → WithZero (Multiplicative ℤ))
        ((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v))
          ((algebraMap R K : (a : R) → K) r)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simpa using v.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
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)
rw :
  Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (HMul.hMul (α := adicCompletion K v)
      ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) r : adicCompletion K v)
      (↑x : adicCompletion K v))
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (r • (↑x : adicCompletion K v))

Tactic:
rw [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)
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (HMul.hMul (α := adicCompletion K v)
      ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) r : adicCompletion K v)
      (↑x : adicCompletion K v))

Tactic:
ValuationSubring.mul_mem _ _ _ ?_ x.2

Premises used: ValuationSubring.mul_mem, Subtype.property
-- 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)
refine :
  Membership.mem (α := adicCompletion K v) (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) r : adicCompletion K v)
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (HMul.hMul (α := adicCompletion K v)
      ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) r : adicCompletion K v)
      (↑x : adicCompletion K v))

Tactic:
refine ValuationSubring.mul_mem _ _ _ ?_ x.2

Premises used: ValuationSubring.mul_mem, Subtype.property
-- 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)
rw :
  Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (((fun (x : K) ↦
          (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) x) :
            UniformSpace.Completion (WithVal (valuation K v)))) ∘
        (⇑(algebraMap R K) : (a : R) → K))
      r)
⊢ Membership.mem (α := adicCompletion K v) (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    ((algebraMap R (adicCompletion K v) : (a : R) → adicCompletion K v) r : adicCompletion K v)

Tactic:
rw [algebraMap_adicCompletion]

Premises used: IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion
-- 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)
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (((fun (x : K) ↦
          (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) x) :
            UniformSpace.Completion (WithVal (valuation K v)))) ∘
        (⇑(algebraMap R K) : (a : R) → K))
      r)

Tactic:
coe_algebraMap_mem _ _ v r

Premises used: UniformSpace.Completion.coe', Set.Mem, setOf, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, SeparationQuotient.mk
-- 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)
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (((fun (x : K) ↦
          (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) x) :
            UniformSpace.Completion (WithVal (valuation K v)))) ∘
        (⇑(algebraMap R K) : (a : R) → K))
      r)

Tactic:
exact coe_algebraMap_mem _ _ v r

Premises used: IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem
-- 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
a :
  Eq (α := adicCompletion K v)
    (↑(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) 1)) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯) :
      adicCompletion K v)
    (↑1 : adicCompletion K v)
⊢ Eq (α := ↥(adicCompletionIntegers K v))
    (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) 1)) :
        UniformSpace.Completion (WithVal (valuation K v)))
      ⋯)
    1

Tactic:
ext
-- 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
⊢ Eq (α := adicCompletion K v)
    (↑(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) 1)) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯) :
      adicCompletion K v)
    (↑1 : adicCompletion K v)

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 y : R
a :
  (↑(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) (x * y))) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯) :
      adicCompletion K v) =
    (↑(HMul.hMul (α := ↥(adicCompletionIntegers K v)) (β := ↥(adicCompletionIntegers K v))
          (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) x)) :
                UniformSpace.Completion (WithVal (valuation K v)))
              ⋯ :
            ↥(adicCompletionIntegers K v))
          (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) y)) :
                UniformSpace.Completion (WithVal (valuation K v)))
              ⋯ :
            ↥(adicCompletionIntegers K v))) :
      adicCompletion K v)
⊢ 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) (x * y))) :
        UniformSpace.Completion (WithVal (valuation K v)))
      ⋯ =
    HMul.hMul (α := ↥(adicCompletionIntegers K v)) (β := ↥(adicCompletionIntegers K v))
      (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) x)) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯ :
        ↥(adicCompletionIntegers K v))
      (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) y)) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯ :
        ↥(adicCompletionIntegers K v))

Tactic:
ext
-- 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 y : 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) (x * y))) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯) :
      adicCompletion K v) =
    (↑(HMul.hMul (α := ↥(adicCompletionIntegers K v)) (β := ↥(adicCompletionIntegers K v))
          (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) x)) :
                UniformSpace.Completion (WithVal (valuation K v)))
              ⋯ :
            ↥(adicCompletionIntegers K v))
          (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) y)) :
                UniformSpace.Completion (WithVal (valuation K v)))
              ⋯ :
            ↥(adicCompletionIntegers K v))) :
      adicCompletion K v)

Tactic:
simp only [map_mul, UniformSpace.Completion.coe_mul, MulMemClass.mk_mul_mk]

Premises used: map_mul, UniformSpace.Completion.coe_mul, MulMemClass.mk_mul_mk
-- 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
a :
  Eq (α := adicCompletion K v)
    (↑(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) 0)) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯) :
      adicCompletion K v)
    (↑0 : adicCompletion K v)
⊢ Eq (α := ↥(adicCompletionIntegers K v))
    (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) 0)) :
        UniformSpace.Completion (WithVal (valuation K v)))
      ⋯)
    0

Tactic:
ext
-- 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
⊢ Eq (α := adicCompletion K v)
    (↑(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) 0)) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯) :
      adicCompletion K v)
    (↑0 : adicCompletion K v)

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 y : R
a :
  (↑(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) (x + y))) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯) :
      adicCompletion K v) =
    (↑(HAdd.hAdd (α := ↥(adicCompletionIntegers K v)) (β := ↥(adicCompletionIntegers K v))
          (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) x)) :
                UniformSpace.Completion (WithVal (valuation K v)))
              ⋯ :
            ↥(adicCompletionIntegers K v))
          (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) y)) :
                UniformSpace.Completion (WithVal (valuation K v)))
              ⋯ :
            ↥(adicCompletionIntegers K v))) :
      adicCompletion K v)
⊢ 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) (x + y))) :
        UniformSpace.Completion (WithVal (valuation K v)))
      ⋯ =
    HAdd.hAdd (α := ↥(adicCompletionIntegers K v)) (β := ↥(adicCompletionIntegers K v))
      (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) x)) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯ :
        ↥(adicCompletionIntegers K v))
      (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) y)) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯ :
        ↥(adicCompletionIntegers K v))

Tactic:
ext
-- 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 y : 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) (x + y))) :
            UniformSpace.Completion (WithVal (valuation K v)))
          ⋯) :
      adicCompletion K v) =
    (↑(HAdd.hAdd (α := ↥(adicCompletionIntegers K v)) (β := ↥(adicCompletionIntegers K v))
          (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) x)) :
                UniformSpace.Completion (WithVal (valuation K v)))
              ⋯ :
            ↥(adicCompletionIntegers K v))
          (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) y)) :
                UniformSpace.Completion (WithVal (valuation K v)))
              ⋯ :
            ↥(adicCompletionIntegers K v))) :
      adicCompletion K v)

Tactic:
simp only [map_add, UniformSpace.Completion.coe_add, AddMemClass.mk_add_mk]

Premises used: map_add, AddMemClass.mk_add_mk, UniformSpace.Completion.coe_add
-- 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 =
    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

Tactic:
ext