awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : Algebra R_1 ℚ
inst_2 : IsIntegralClosure R_1 ℤ ℚ
R : Type u_2
inst_3 : CommRing R
inst_4 : Algebra R ℚ
inst_5 : IsIntegralClosure R ℤ ℚ
inst_6 : IsDedekindDomain R
inst_7 : IsFractionRing R ℚ
p : Nat.Primes
e_val :
  Int.natAbs
      (Submodule.IsPrincipal.generator
        (Ideal.map (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R)
          (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(↑p : ℕ) : ℤ)})))) =
    (↑p : ℕ)
⊢ Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p)
      (Int.natAbs
        (Submodule.IsPrincipal.generator
          (Ideal.map (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R)
            (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(↑p : ℕ) : ℤ)})))))
      ⋯ =
    p

Tactic:
congr
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : Algebra R_1 ℚ
inst_2 : IsIntegralClosure R_1 ℤ ℚ
R : Type u_2
inst_3 : CommRing R
inst_4 : Algebra R ℚ
inst_5 : IsIntegralClosure R ℤ ℚ
inst_6 : IsDedekindDomain R
inst_7 : IsFractionRing R ℚ
p : Nat.Primes
⊢ Int.natAbs
      (Submodule.IsPrincipal.generator
        (Ideal.map (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R)
          (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(↑p : ℕ) : ℤ)})))) =
    (↑p : ℕ)

Tactic:
simp [Ideal.map_comap_of_surjective _ (IsIntegralClosure.intEquiv R).surjective,
      Int.associated_iff_natAbs.1 (Submodule.IsPrincipal.associated_generator_span_self _)]

Premises used: Rat.IsIntegralClosure.intEquiv, RingEquiv.surjective, Int.associated_iff_natAbs, Iff.mp, Submodule.IsPrincipal.associated_generator_span_self, Ideal.map_comap_of_surjective
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ Valuation.IsEquiv (HeightOneSpectrum.valuation ℚ v)
    (padicValuation
      (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ))

Tactic:
simp [primesEquiv, Valuation.isEquiv_iff_val_le_one, valuation_le_one_iff_den,
    padicValuation_le_one_iff, natGenerator_dvd_iff,
    map_natCast (IsIntegralClosure.intEquiv R) _ ▸ Ideal.apply_mem_of_equiv_iff]

Premises used: Rat.HeightOneSpectrum.primesEquiv, Valuation.isEquiv_iff_val_le_one, Rat.valuation_le_one_iff_den, Rat.HeightOneSpectrum.natGenerator_dvd_iff, Rat.padicValuation_le_one_iff
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : Algebra R_1 ℚ
inst_2 : IsIntegralClosure R_1 ℤ ℚ
R : Type u_2
inst_3 : CommRing R
inst_4 : Algebra R ℚ
inst_5 : IsIntegralClosure R ℤ ℚ
inst_6 : IsDedekindDomain R
inst_7 : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ ∀ (r : ℚ),
    Equiv.toFun (α := UniformSpace.Completion (WithVal (HeightOneSpectrum.valuation ℚ v)))
        (RingEquiv.toEquiv
          (RingEquiv.trans
            (mapRingEquiv
              (WithVal.congr (HeightOneSpectrum.valuation ℚ v)
                (padicValuation
                  (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
                    ℕ))
                (RingEquiv.refl ℚ))
              ⋯ ⋯)
            Padic.withValRingEquiv))
        ((algebraMap ℚ (HeightOneSpectrum.adicCompletion ℚ v) : (a : ℚ) → HeightOneSpectrum.adicCompletion ℚ v) r) =
      (algebraMap ℚ
            ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)] :
          (a : ℚ) → ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
        r

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : Algebra R_1 ℚ
inst_2 : IsIntegralClosure R_1 ℤ ℚ
R : Type u_2
inst_3 : CommRing R
inst_4 : Algebra R ℚ
inst_5 : IsIntegralClosure R ℤ ℚ
inst_6 : IsDedekindDomain R
inst_7 : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : UniformSpace.Completion (WithVal (HeightOneSpectrum.valuation ℚ v))
⊢ Membership.mem (γ := ValuationSubring (HeightOneSpectrum.adicCompletion ℚ v))
      (HeightOneSpectrum.adicCompletionIntegers ℚ v) x ↔
    Membership.mem (α :=
      UniformSpace.Completion
        (WithVal
          (padicValuation
            (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ))))
      (γ :=
      Subring
        (padicValuation
            (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
              ℕ)).Completion)
      (Valued.integer
        (padicValuation
            (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
              ℕ)).Completion)
      ((mapRingEquiv
              (WithVal.congr (HeightOneSpectrum.valuation ℚ v)
                (padicValuation
                  (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
                    ℕ))
                (RingEquiv.refl ℚ))
              ⋯ ⋯ :
            (a : UniformSpace.Completion (WithVal (HeightOneSpectrum.valuation ℚ v))) →
              UniformSpace.Completion
                (WithVal (padicValuation (↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ))))
          x :
        UniformSpace.Completion
          (WithVal
            (padicValuation
              (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ))))

Tactic:
simpa using (valuation_equiv_padicValuation v).valuedCompletion_le_one_iff

Premises used: Valuation.IsEquiv.valuedCompletion_le_one_iff, Rat.HeightOneSpectrum.valuation_equiv_padicValuation
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : Algebra R_1 ℚ
inst_2 : IsIntegralClosure R_1 ℤ ℚ
R : Type u_2
inst_3 : CommRing R
inst_4 : Algebra R ℚ
inst_5 : IsIntegralClosure R ℤ ℚ
inst_6 : IsDedekindDomain R
inst_7 : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : UniformSpace.Completion (WithVal (HeightOneSpectrum.valuation ℚ v))
⊢ Membership.mem (γ := ValuationSubring (HeightOneSpectrum.adicCompletion ℚ v))
      (HeightOneSpectrum.adicCompletionIntegers ℚ v) x ↔
    Membership.mem (α :=
      (padicValuation
          (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
            ℕ)).Completion)
      (γ :=
      Subring
        (padicValuation
            (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
              ℕ)).Completion)
      (Valued.integer
        (padicValuation
            (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
              ℕ)).Completion)
      ((mapEquiv (withValEquiv v) :
            (a : UniformSpace.Completion (WithVal (HeightOneSpectrum.valuation ℚ v))) →
              UniformSpace.Completion
                (WithVal (padicValuation (↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ))))
          x :
        UniformSpace.Completion
          (WithVal
            (padicValuation
              (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ))))

Tactic:
simpa using (valuation_equiv_padicValuation v).valuedCompletion_le_one_iff

Premises used: Valuation.IsEquiv.valuedCompletion_le_one_iff, Rat.HeightOneSpectrum.valuation_equiv_padicValuation
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : Algebra R_1 ℚ
inst_2 : IsIntegralClosure R_1 ℤ ℚ
R : Type u_2
inst_3 : CommRing R
inst_4 : Algebra R ℚ
inst_5 : IsIntegralClosure R ℤ ℚ
inst_6 : IsDedekindDomain R
inst_7 : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ ∀ (r : ℤ),
    Eq (α := ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      (Equiv.toFun (α := ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v))
          (RingEquiv.toEquiv
              (let e :
                ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v) ≃+*
                  ↥(Valued.integer
                      (padicValuation
                          (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                                v) :
                            ℕ)).Completion) :=
                RingEquiv.restrict
                  (mapRingEquiv
                    (WithVal.congr (HeightOneSpectrum.valuation ℚ v)
                      (padicValuation
                        (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                              v) :
                          ℕ))
                      (RingEquiv.refl ℚ))
                    ⋯ ⋯)
                  (HeightOneSpectrum.adicCompletionIntegers ℚ v)
                  (Valued.integer
                    (padicValuation
                        (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                              v) :
                          ℕ)).Completion)
                  ⋯;
              e.trans withValIntegersRingEquiv) :
            ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v) ≃
              ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
                  ℕ)])
          ((algebraMap ℤ ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v) :
                (a : ℤ) → ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v))
              r :
            ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) :
        ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      ((algebraMap ℤ
              ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
                  ℕ)] :
            (a : ℤ) → ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
          r :
        ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
⊢ Eq (α := ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    ((↑((padicIntEquiv v :
              (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
                ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
            x) :
        ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) :
      ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    ((adicCompletion.padicEquiv v :
          (a : HeightOneSpectrum.adicCompletion ℚ v) →
            ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
        (↑x : HeightOneSpectrum.adicCompletion ℚ v) :
      ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])

Tactic:
rfl

Premises used: UniformSpace.Completion.extension, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]
⊢ Eq (α := HeightOneSpectrum.adicCompletion ℚ v)
    ((↑((ContinuousAlgEquiv.symm (padicIntEquiv v) :
              (a : ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) →
                ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v))
            x) :
        HeightOneSpectrum.adicCompletion ℚ v) :
      HeightOneSpectrum.adicCompletion ℚ v)
    ((ContinuousAlgEquiv.symm (adicCompletion.padicEquiv v) :
          (a : ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) →
            HeightOneSpectrum.adicCompletion ℚ v)
        (↑x : ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) :
      HeightOneSpectrum.adicCompletion ℚ v)

Tactic:
rfl

Premises used: Classical.epsilon, Set.Mem, Filter.lim, Filter.limUnder, IsDenseInducing.extend, rfl
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ Set.BijOn
    (⇑(padicEquiv v) :
      (a : HeightOneSpectrum.adicCompletion ℚ v) →
        ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v))
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])

Tactic:
⟨fun x hx ↦ ?_, (padicEquiv v).injective.injOn, fun y hy ↦ ?_⟩

Premises used: Function.Injective.injOn, And.intro, Set.BijOn, AlgEquiv.injective, Rat.HeightOneSpectrum.adicCompletion.padicEquiv, ContinuousAlgEquiv.toAlgEquiv
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
refine_1 :
  ∀ (x : HeightOneSpectrum.adicCompletion ℚ v)
    (hx : x ∈ (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v))),
    Membership.mem (α :=
      ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      (↑(subring
            (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
        Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      ((padicEquiv v :
            (a : HeightOneSpectrum.adicCompletion ℚ v) →
              ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
          x :
        ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
refine_2 :
  ∀ (y : ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    (hy :
      y ∈
        (↑(subring
              (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
          Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])),
    Membership.mem (γ :=
      Set ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      ((⇑(padicEquiv v) :
          (a : HeightOneSpectrum.adicCompletion ℚ v) →
            ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ''
        (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v)))
      y
⊢ Set.BijOn
    (⇑(padicEquiv v) :
      (a : HeightOneSpectrum.adicCompletion ℚ v) →
        ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v))
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])

Tactic:
refine ⟨fun x hx ↦ ?_, (padicEquiv v).injective.injOn, fun y hy ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : HeightOneSpectrum.adicCompletion ℚ v
hx : x ∈ (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v))
refine_1 :
  (↑((adicCompletionIntegers.padicIntEquiv v :
            (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
              ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
          (Subtype.mk (p := fun (x : HeightOneSpectrum.adicCompletion ℚ v) ↦
            Membership.mem (γ := ValuationSubring (HeightOneSpectrum.adicCompletion ℚ v))
              (HeightOneSpectrum.adicCompletionIntegers ℚ v) x)
            x hx)) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ∈
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
⊢ Membership.mem (α :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    ((padicEquiv v :
          (a : HeightOneSpectrum.adicCompletion ℚ v) →
            ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
        x :
      ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])

Tactic:
rw [← adicCompletionIntegers.coe_padicIntEquiv_apply v ⟨x, hx⟩]

Premises used: Subtype.mk, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : HeightOneSpectrum.adicCompletion ℚ v
hx : x ∈ (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v))
⊢ (↑((adicCompletionIntegers.padicIntEquiv v :
            (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
              ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
          (Subtype.mk (p := fun (x : HeightOneSpectrum.adicCompletion ℚ v) ↦
            Membership.mem (γ := ValuationSubring (HeightOneSpectrum.adicCompletion ℚ v))
              (HeightOneSpectrum.adicCompletionIntegers ℚ v) x)
            x hx)) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ∈
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])

Tactic:
norm_le_one ((adicCompletionIntegers.padicIntEquiv v) ⟨x, hx⟩)

Premises used: Set.Mem, setOf, Subtype.mk, Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv, PadicInt.norm_le_one, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : HeightOneSpectrum.adicCompletion ℚ v
hx : x ∈ (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v))
⊢ (↑((adicCompletionIntegers.padicIntEquiv v :
            (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
              ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
          (Subtype.mk (p := fun (x : HeightOneSpectrum.adicCompletion ℚ v) ↦
            Membership.mem (γ := ValuationSubring (HeightOneSpectrum.adicCompletion ℚ v))
              (HeightOneSpectrum.adicCompletionIntegers ℚ v) x)
            x hx)) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ∈
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])

Tactic:
exact norm_le_one ((adicCompletionIntegers.padicIntEquiv v) ⟨x, hx⟩)

Premises used: Subtype.mk, Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv, PadicInt.norm_le_one, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]
hy :
  y ∈
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
refine_2 :
  ∀ (x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v))
    (hx :
      (adicCompletionIntegers.padicIntEquiv v :
            (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
              ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
          x =
        Subtype.mk (p :=
          fun
            (x :
              ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
                  ℕ)]) ↦
          ‖x‖ ≤ 1) y hy),
    Membership.mem (γ :=
      Set ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      ((⇑(padicEquiv v) :
          (a : HeightOneSpectrum.adicCompletion ℚ v) →
            ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ''
        (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v)))
      y
⊢ Membership.mem (γ :=
    Set ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    ((⇑(padicEquiv v) :
        (a : HeightOneSpectrum.adicCompletion ℚ v) →
          ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ''
      (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v)))
    y

Tactic:
obtain ⟨x, hx⟩ := (adicCompletionIntegers.padicIntEquiv v).surjective ⟨y, hy⟩

Premises used: Subtype.mk, ContinuousAlgEquiv.surjective, Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv