awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
n : (WithZero (Multiplicative ℤ))ˣ
h :
  ∃ (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 ℤ))
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) b :
        WithZero (Multiplicative ℤ))
      (↑n : WithZero (Multiplicative ℤ)) =
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y

Tactic:
simp [hb, hy, hx]
-- 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
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
⊢ ∃ (a : K),
    ¬a = 0 ∧
      ∃ (x : K),
        HMul.hMul (α := WithZero (Multiplicative ℤ))
            (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) a :
              WithZero (Multiplicative ℤ))
            (↑n : WithZero (Multiplicative ℤ)) =
          ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x

Tactic:
refine ⟨b, ?_, y, by simp [hb, hy, hx]⟩
-- 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
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 ℤ))
h₃ h₄ h₅ h₆ : a ≠ 0
⊢ ¬b = 0

Tactic:
rwa [← ne_eq, ← (valuation K v).ne_zero_iff, hb, Valuation.ne_zero_iff]

Premises used: ne_eq, Valuation.ne_zero_iff, IsDedekindDomain.HeightOneSpectrum.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
x : adicCompletion K v
⊢ Membership.mem (γ := ValuationSubring (adicCompletion K v)) (adicCompletionIntegers K v) x ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          x :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : adicCompletion K v
⊢ ¬LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) ↔
    LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          x :
        WithZero (Multiplicative ℤ))

Tactic:
not_le

Premises used: not_le
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : adicCompletion K v
⊢ ¬LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) ↔
    LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          x :
        WithZero (Multiplicative ℤ))

Tactic:
exact not_le

Premises used: not_le
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
⊢ UniformContinuousConstSMul.{u_1, u_2} R (WithVal (valuation K v))

Tactic:
uniformContinuousConstSMul_of_continuousConstSMul R (WithVal <| v.valuation K)

Premises used: uniformContinuousConstSMul_of_continuousConstSMul, WithVal, IsDedekindDomain.HeightOneSpectrum.valuation
-- 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
⊢ UniformContinuousConstSMul.{u_3, u_2} S (WithVal (valuation K v))

Tactic:
⟨fun l ↦ ?_⟩

Premises used: UniformContinuousConstSMul.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
inst_6 : Algebra S K
refine : ∀ (l : S), UniformContinuous (β := WithVal (valuation K v)) fun (x : WithVal (valuation K v)) ↦ l • x
⊢ UniformContinuousConstSMul.{u_3, u_2} S (WithVal (valuation K v))

Tactic:
refine ⟨fun l ↦ ?_⟩
-- 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
l : S
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)
⊢ UniformContinuous (β := WithVal (valuation K v)) fun (x : WithVal (valuation K v)) ↦ l • x

Tactic:
simp_rw [WithVal.smul_right_def, Algebra.smul_def]

Premises used: WithVal.smul_right_def, 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
inst_6 : Algebra S K
l : S
⊢ 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:
(Ring.uniformContinuousConstSMul (WithVal <| v.valuation K)).uniformContinuous_const_smul _

Premises used: UniformContinuousConstSMul.uniformContinuous_const_smul
-- 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
l : S
⊢ 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:
exact (Ring.uniformContinuousConstSMul (WithVal <| v.valuation K)).uniformContinuous_const_smul _

Premises used: UniformContinuousConstSMul.uniformContinuous_const_smul
-- 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
r : S
⊢ 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:
isClosed_eq (continuous_const_mul _) (continuous_mul_const _)

Premises used: continuous_const_mul, isClosed_eq, continuous_mul_const
-- 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
r : S
⊢ 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:
exact isClosed_eq (continuous_const_mul _) (continuous_mul_const _)

Premises used: continuous_const_mul, isClosed_eq, continuous_mul_const
-- 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
r : S
x : WithVal (valuation K v)
ih 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)
⊢ 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:
rw [mul_comm]

Premises used: mul_comm
-- 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
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)}
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)
⊢ 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)

Tactic:
induction x using Completion.induction_on with
    | hp =>
      exact isClosed_eq (continuous_const_mul _) (continuous_mul_const _)
    | ih x => rw [mul_comm]

Premises used: continuous_const_mul, isClosed_eq, mul_comm, continuous_mul_const
-- 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
r : S
⊢ 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:
isClosed_eq (continuous_const_smul _) (continuous_const_mul _)

Premises used: ContinuousConstSMul.continuous_const_smul, continuous_const_mul, isClosed_eq
-- 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
r : S
⊢ 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:
exact isClosed_eq (continuous_const_smul _) (continuous_const_mul _)

Premises used: ContinuousConstSMul.continuous_const_smul, continuous_const_mul, isClosed_eq
-- 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
r : S
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:
simp [Algebra.smul_def, Completion.algebraMap_def, WithVal.algebraMap_right_apply,
        Completion.coeRingHom]

Premises used: UniformSpace.Completion.coeRingHom, UniformSpace.Completion.algebraMap_def, Algebra.smul_def, WithVal.algebraMap_right_apply
-- 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
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}
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)))
⊢ 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

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]

Premises used: ContinuousConstSMul.continuous_const_smul, UniformSpace.Completion.coeRingHom, continuous_const_mul, UniformSpace.Completion.algebraMap_def, isClosed_eq, Algebra.smul_def, WithVal.algebraMap_right_apply
-- 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
r : S
x : WithVal (valuation K v)
⊢ (↑(r • x) : UniformSpace.Completion (WithVal (valuation K v))) =
    HSMul.hSMul (β := UniformSpace.Completion (WithVal (valuation K v))) r
      (↑x : UniformSpace.Completion (WithVal (valuation K v)))

Tactic:
UniformSpace.Completion.coe_smul r x

Premises used: Set.Mem, setOf, UniformSpace.Completion.coe_smul