awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  Eq (α := UniformSpace.Completion (PadicAlgCl p)) (↑(↑n : PadicAlgCl p) : UniformSpace.Completion (PadicAlgCl p))
    ((algebraMap (PadicAlgCl p) ℂ_[p] : (a : PadicAlgCl p) → ℂ_[p]) (↑n : PadicAlgCl p))
⊢ Eq (α := UniformSpace.Completion (PadicAlgCl p)) (↑(↑n : PadicAlgCl p) : UniformSpace.Completion (PadicAlgCl p))
    (↑n : ℂ_[p])
have rw₁ : Eq (α := UniformSpace.Completion (PadicAlgCl p))
  ((algebraMap (PadicAlgCl p) ℂ_[p] : (a : PadicAlgCl p) → ℂ_[p]) (↑n : PadicAlgCl p))
  ((algebraMap (PadicAlgCl p) ℂ_[p] : (a : PadicAlgCl p) → ℂ_[p]) (↑n : PadicAlgCl p))
Tactic: rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]) n, coe_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p]) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
have rw : (Valued.v : (a : ℂ_[p]) → ℝ≥0) ((algebraMap (PadicAlgCl p) ℂ_[p] : (a : PadicAlgCl p) → ℂ_[p]) (↑p : PadicAlgCl p)) =
  HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
Tactic: rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]), ← coe_eq, valuation_extends,
    PadicAlgCl.valuation_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw :
  (Valued.v : (a : ℂ_[p]) → ℝ≥0) ((algebraMap (PadicAlgCl p) ℂ_[p] : (a : PadicAlgCl p) → ℂ_[p]) (↑p : PadicAlgCl p)) =
    HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
⊢ (Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p]) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
have rw₁ : (Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑(↑p : PadicAlgCl p) : UniformSpace.Completion (PadicAlgCl p)) =
  HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
Tactic: rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]), ← coe_eq, valuation_extends,
    PadicAlgCl.valuation_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw :
  (Valued.v : (a : ℂ_[p]) → ℝ≥0) ((algebraMap (PadicAlgCl p) ℂ_[p] : (a : PadicAlgCl p) → ℂ_[p]) (↑p : PadicAlgCl p)) =
    HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
rw₁ :
  (Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑(↑p : PadicAlgCl p) : UniformSpace.Completion (PadicAlgCl p)) =
    HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
⊢ (Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p]) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
have rw₂ : (Valued.v : (a : PadicAlgCl p) → ℝ≥0) (↑p : PadicAlgCl p) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
Tactic: rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]), ← coe_eq, valuation_extends,
    PadicAlgCl.valuation_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw :
  (Valued.v : (a : ℂ_[p]) → ℝ≥0) ((algebraMap (PadicAlgCl p) ℂ_[p] : (a : PadicAlgCl p) → ℂ_[p]) (↑p : PadicAlgCl p)) =
    HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
rw₁ :
  (Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑(↑p : PadicAlgCl p) : UniformSpace.Completion (PadicAlgCl p)) =
    HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
rw₂ : (Valued.v : (a : PadicAlgCl p) → ℝ≥0) (↑p : PadicAlgCl p) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
⊢ (Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p]) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
have rw₃ : HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
Tactic: rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]), ← coe_eq, valuation_extends,
    PadicAlgCl.valuation_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ (x : ℂ_[p]),
    Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ∧
      Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
have h : Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 0 ∧
  Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 1
Tactic: use p
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 0 ∧
    Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 1
have hp₁ : Nat.Prime p
Tactic: have hp : Nat.Prime p := hp.1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
hp : Nat.Prime p
⊢ Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 0 ∧
    Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 1
have h : ¬p = 0 ∧ ¬p = 1
Tactic: simp only [valuation_p, one_div, ne_eq, inv_eq_zero, Nat.cast_eq_zero, inv_eq_one,
      Nat.cast_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℂ_[p] → ℝ) (fun (x : ℂ_[p]) ↦ ‖x‖) (Valuation.norm Valued.v)
have hf : UniformContinuous (α := PadicAlgCl p) Norm.norm
Tactic: apply UniformSpace.Completion.extension_unique (f := @norm (PadicAlgCl p) _) (g := Valued.v.norm)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hf : UniformContinuous (α := PadicAlgCl p) Norm.norm
⊢ Eq (α := ℂ_[p] → ℝ) (fun (x : ℂ_[p]) ↦ ‖x‖) (Valuation.norm Valued.v)
have hg : UniformContinuous (α := UniformSpace.Completion (PadicAlgCl p)) (Valuation.norm Valued.v)
Tactic: apply UniformSpace.Completion.extension_unique (f := @norm (PadicAlgCl p) _) (g := Valued.v.norm)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hf : UniformContinuous (α := PadicAlgCl p) Norm.norm
hg : UniformContinuous (α := UniformSpace.Completion (PadicAlgCl p)) (Valuation.norm Valued.v)
⊢ Eq (α := ℂ_[p] → ℝ) (fun (x : ℂ_[p]) ↦ ‖x‖) (Valuation.norm Valued.v)
have h : ∀ (a : PadicAlgCl p),
  ‖a‖ =
    Valuation.norm (L := UniformSpace.Completion (PadicAlgCl p)) Valued.v (↑a : UniformSpace.Completion (PadicAlgCl p))
Tactic: apply UniformSpace.Completion.extension_unique (f := @norm (PadicAlgCl p) _) (g := Valued.v.norm)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℂ_[p]
⊢ ‖x‖ = Valuation.norm Valued.v x
have h : Eq (α := ℂ_[p] → ℝ) Norm.norm (Valuation.norm Valued.v)
Tactic: congr!
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ nnnorm (E := UniformSpace.Completion (PadicAlgCl p)) (↑x : UniformSpace.Completion (PadicAlgCl p)) = ‖x‖₊
have a : (↑(nnnorm (E := UniformSpace.Completion (PadicAlgCl p)) (↑x : UniformSpace.Completion (PadicAlgCl p))) : ℝ) =
  (↑‖x‖₊ : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ nnnorm (E := UniformSpace.Completion (PadicAlgCl p))
      ((↑((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x) : UniformSpace.Completion (PadicAlgCl p)) :
        UniformSpace.Completion (PadicAlgCl p)) =
    ‖x‖₊
have a : (↑(nnnorm (E := UniformSpace.Completion (PadicAlgCl p))
        ((↑((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x) :
            UniformSpace.Completion (PadicAlgCl p)) :
          UniformSpace.Completion (PadicAlgCl p))) :
    ℝ) =
  (↑‖x‖₊ : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ (x : ℂ_[p]), 1 < ‖x‖
have choose : ∀ (x : ℚ_[p]) (hx : 1 < ‖x‖), ∃ (x : ℂ_[p]), 1 < ‖x‖
Tactic: choose x hx using NontriviallyNormedField.non_trivial (α := ℚ_[p])
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Complex (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ ∃ (x : ℂ_[p]), 1 < ‖x‖
have h : 1 <
  Norm.norm (E := ℂ_[p])
    ((↑((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x) : UniformSpace.Completion (PadicAlgCl p)) :
      UniformSpace.Completion (PadicAlgCl p))
Tactic: use x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsFractionRing R ℚ
x : R
⊢ ∃ (a : ℤ), (algebraMap ℤ R : (a : ℤ) → R) a = x
have obtain : ∀ (y : ℤ) (hy : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) y : ℚ) ((algebraMap R ℚ : (a : R) → ℚ) x : ℚ)),
  ∃ (a : ℤ), (algebraMap ℤ R : (a : ℤ) → R) a = x
Tactic: obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.1 <|
    IsIntegral.algebraMap (B := ℚ) (IsIntegralClosure.isIntegral ℤ ℚ x)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
n : ℕ
⊢ natGenerator v ∣ n ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.map (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) v.asIdeal) (↑n : ℤ)
have rw : natGenerator v ∣ n ↔ Dvd.dvd (α := ℤ) (↑(natGenerator v) : ℤ) (↑n : ℤ)
Tactic: rw [← span_natGenerator, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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
⊢ (fun (p : Nat.Primes) ↦
        have h :
          Prime (M := Ideal R)
            (Ideal.map (R := ℤ) (F := ℤ ≃+* R) (RingEquiv.symm (IsIntegralClosure.intEquiv R))
              (Ideal.span {(↑(↑p : ℕ) : ℤ)})) :=
          ⋯;
        HeightOneSpectrum.ofPrime h)
      ((fun (v : HeightOneSpectrum R) ↦ Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (natGenerator v) ⋯) v) =
    v
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [Ideal.map_symm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e_p : Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}) = v.asIdeal
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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
⊢ Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}) = v.asIdeal
have e_p : Eq (α := Ideal R) (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}))
  (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R)
    (Ideal.map (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) v.asIdeal))
Tactic: rw [← v.asIdeal.comap_map_of_bijective _ (IsIntegralClosure.intEquiv R).bijective,
      ← span_natGenerator]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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
e_p :
  Eq (α := Ideal R) (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}))
    (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R)
      (Ideal.map (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) v.asIdeal))
⊢ Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}) = v.asIdeal
have e_p₁ : Eq (α := Ideal R) (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}))
  (Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}))
Tactic: rw [← v.asIdeal.comap_map_of_bijective _ (IsIntegralClosure.intEquiv R).bijective,
      ← span_natGenerator]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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
⊢ (fun (v : HeightOneSpectrum R) ↦ Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (natGenerator v) ⋯)
      ((fun (p : Nat.Primes) ↦
          have h :
            Prime (M := Ideal R)
              (Ideal.map (R := ℤ) (F := ℤ ≃+* R) (RingEquiv.symm (IsIntegralClosure.intEquiv R))
                (Ideal.span {(↑(↑p : ℕ) : ℤ)})) :=
            ⋯;
          HeightOneSpectrum.ofPrime h)
        p) =
    p
have simp : 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 : ℕ) : ℤ)})))))
    sorry =
  p
Tactic: simp only [Ideal.map_symm, natGenerator, HeightOneSpectrum.ofPrime_asIdeal]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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
⊢ 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
have 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 : ℕ)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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) : ℕ)])
have 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) : ℕ)])
Tactic: refine ⟨fun x hx ↦ ?_, (padicEquiv v).injective.injOn, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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) : ℕ)])
⊢ 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) : ℕ)])
have 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
Tactic: refine ⟨fun x hx ↦ ?_, (padicEquiv v).injective.injOn, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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))
⊢ 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) : ℕ)])
have 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) : ℕ)])
Tactic: rw [← adicCompletionIntegers.coe_padicIntEquiv_apply v ⟨x, hx⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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) : ℕ)])
⊢ 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
have 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
Tactic: obtain ⟨x, hx⟩ := (adicCompletionIntegers.padicIntEquiv v).surjective ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
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) : ℕ)])
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
⊢ (padicEquiv v :
        (a : HeightOneSpectrum.adicCompletion ℚ v) →
          ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      (↑x : HeightOneSpectrum.adicCompletion ℚ v) =
    y
have rw : (↑((adicCompletionIntegers.padicIntEquiv v :
          (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
            ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
        x) :
    ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) =
  y
Tactic: rw [← adicCompletionIntegers.coe_padicIntEquiv_apply, hx]