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
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
n : (WithZero (Multiplicative ℤ))ˣ
h_1 :
  ∃ (a : adicCompletion K v),
    ¬a = 0 ∧
      ∃ (x : adicCompletion K v),
        HMul.hMul (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                a :
              WithZero (Multiplicative ℤ))
            (↑n : WithZero (Multiplicative ℤ)) =
          ((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            x
a : adicCompletion K v
ha0 : ¬a = 0
x : adicCompletion K v
hx :
  HMul.hMul (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (↑n : WithZero (Multiplicative ℤ)) =
    ((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
        (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
      x
b : K
hb :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) b :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
y : K
hy :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
h : b ≠ 0
h₁ :
  Ne (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) b :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
h₂ :
  Ne (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ ¬b = 0
have h₃ : a ≠ 0
Tactic: rwa [← ne_eq, ← (valuation K v).ne_zero_iff, hb, Valuation.ne_zero_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
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
⊢ UniformContinuousConstSMul.{u_3, u_2} S (WithVal (valuation K v))
have refine : ∀ (l : S), UniformContinuous (β := WithVal (valuation K v)) fun (x : WithVal (valuation K v)) ↦ l • x
Tactic: refine ⟨fun l ↦ ?_⟩
-- 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 : Algebra S K
l : S
⊢ UniformContinuous (β := WithVal (valuation K v)) fun (x : WithVal (valuation K v)) ↦ l • x
have simp_rw : UniformContinuous (β := WithVal (valuation K v)) fun (x : WithVal (valuation K v)) ↦
  WithVal.toVal (valuation K v) (HMul.hMul (α := K) ((algebraMap S K : (a : S) → K) l : K) x.ofVal)
Tactic: simp_rw [WithVal.smul_right_def, 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 : Algebra S K
r : S
x : WithVal (valuation K v)
⊢ HMul.hMul (α := adicCompletion K v) (β := adicCompletion K v)
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
      (↑x : Completion (WithVal (valuation K v))) =
    HMul.hMul (α := adicCompletion K v) (β := adicCompletion K v) (↑x : Completion (WithVal (valuation K v)))
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
have ih : HMul.hMul (α := adicCompletion K v) (β := adicCompletion K v) (↑x : Completion (WithVal (valuation K v)))
    ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
      adicCompletion K v) =
  HMul.hMul (α := adicCompletion K v) (β := adicCompletion K v) (↑x : Completion (WithVal (valuation K v)))
    ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
      adicCompletion K v)
Tactic: rw [mul_comm]
-- 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 : Algebra S K
r : S
x : adicCompletion K v
⊢ HMul.hMul (α := adicCompletion K v)
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
      x =
    HMul.hMul (β := adicCompletion K v) x
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
have hp : IsClosed.{u_2} (X := Completion (WithVal (valuation K v)))
  {a : Completion (WithVal (valuation K v)) |
    HMul.hMul (α := adicCompletion K v)
        ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v)
            r :
          adicCompletion K v)
        a =
      HMul.hMul (β := adicCompletion K v) a
        ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v)
            r :
          adicCompletion K v)}
Tactic: induction x using Completion.induction_on with
    | hp =>
      exact isClosed_eq (continuous_const_mul _) (continuous_mul_const _)
    | ih x => rw [mul_comm]
Cleared hypotheses: x
-- 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 : Algebra S K
r : S
x : adicCompletion K v
hp :
  IsClosed.{u_2} (X := Completion (WithVal (valuation K v)))
    {a : Completion (WithVal (valuation K v)) |
      HMul.hMul (α := adicCompletion K v)
          ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v)
              r :
            adicCompletion K v)
          a =
        HMul.hMul (β := adicCompletion K v) a
          ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v)
              r :
            adicCompletion K v)}
⊢ HMul.hMul (α := adicCompletion K v)
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
      x =
    HMul.hMul (β := adicCompletion K v) x
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
have ih : ∀ (x : WithVal (valuation K v)),
  HMul.hMul (α := adicCompletion K v) (β := adicCompletion K v)
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
      (↑x : Completion (WithVal (valuation K v))) =
    HMul.hMul (α := adicCompletion K v) (β := adicCompletion K v) (↑x : Completion (WithVal (valuation K v)))
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
Tactic: induction x using Completion.induction_on with
    | hp =>
      exact isClosed_eq (continuous_const_mul _) (continuous_mul_const _)
    | ih x => rw [mul_comm]
Cleared hypotheses: x
-- 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 : Algebra S K
r : S
x : adicCompletion K v
⊢ r • x =
    HMul.hMul (α := adicCompletion K v)
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
      x
have hp : IsClosed.{u_2} (X := Completion (WithVal (valuation K v)))
  {a : Completion (WithVal (valuation K v)) |
    r • a =
      HMul.hMul (α := adicCompletion K v)
        ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v)
            r :
          adicCompletion K v)
        a}
Tactic: induction x using Completion.induction_on with
    | hp =>
      exact isClosed_eq (continuous_const_smul _) (continuous_const_mul _)
    | ih x =>
      simp [Algebra.smul_def, Completion.algebraMap_def, WithVal.algebraMap_right_apply,
        Completion.coeRingHom]
Cleared hypotheses: x
-- 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 : Algebra S K
r : S
x : adicCompletion K v
hp :
  IsClosed.{u_2} (X := Completion (WithVal (valuation K v)))
    {a : Completion (WithVal (valuation K v)) |
      r • a =
        HMul.hMul (α := adicCompletion K v)
          ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v)
              r :
            adicCompletion K v)
          a}
⊢ r • x =
    HMul.hMul (α := adicCompletion K v)
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
      x
have ih : ∀ (x : WithVal (valuation K v)),
  HSMul.hSMul (β := adicCompletion K v) r (↑x : Completion (WithVal (valuation K v))) =
    HMul.hMul (α := adicCompletion K v) (β := adicCompletion K v)
      ((RingHom.comp Completion.coeRingHom (algebraMap S (WithVal (valuation K v))) : (a : S) → adicCompletion K v) r :
        adicCompletion K v)
      (↑x : Completion (WithVal (valuation K v)))
Tactic: induction x using Completion.induction_on with
    | hp =>
      exact isClosed_eq (continuous_const_smul _) (continuous_const_mul _)
    | ih x =>
      simp [Algebra.smul_def, Completion.algebraMap_def, WithVal.algebraMap_right_apply,
        Completion.coeRingHom]
Cleared hypotheses: x
-- 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 (α := 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)))
have 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 ℤ))
Tactic: rw [mem_adicCompletionIntegers, Valued.valuedCompletion_apply]
-- 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)
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v)
    (r • (↑x : adicCompletion K v))
have 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))
Tactic: rw [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
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))
have 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)
Tactic: refine ValuationSubring.mul_mem _ _ _ ?_ x.2
-- 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)
⊢ 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)
have 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)
Tactic: rw [algebraMap_adicCompletion]
-- 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
⊢ 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
have 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)))
        sorry) :
    adicCompletion K v)
  (↑1 : 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
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)))
      ⋯ =
    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))
have 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)))
        sorry) :
    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)))
            sorry :
          ↥(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)))
            sorry :
          ↥(adicCompletionIntegers K v))) :
    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
⊢ 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
have 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)))
        sorry) :
    adicCompletion K v)
  (↑0 : 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
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)))
      ⋯ =
    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))
have 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)))
        sorry) :
    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)))
            sorry :
          ↥(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)))
            sorry :
          ↥(adicCompletionIntegers K v))) :
    adicCompletion K v)
Tactic: ext