awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
hp : Nat.Prime p
⊢ ¬p = 0 ∧ ¬p = 1

Tactic:
⟨hp.ne_zero, hp.ne_one⟩

Premises used: Nat.Prime.ne_one, Nat.Prime.ne_zero, And.intro
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
hp : Nat.Prime p
⊢ ¬p = 0 ∧ ¬p = 1

Tactic:
exact ⟨hp.ne_zero, hp.ne_one⟩
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ UniformContinuousConstSMul ℚ_[p] (PadicAlgCl p)

Tactic:
uniformContinuousConstSMul_of_continuousConstSMul ℚ_[p] (PadicAlgCl p)

Premises used: uniformContinuousConstSMul_of_continuousConstSMul, Padic, PadicAlgCl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
choose : ∀ (x : ℚ_[p]) (hx : 1 < ‖x‖), ∃ (x : PadicAlgCl p), 1 < ‖x‖
⊢ ∃ (x : PadicAlgCl p), 1 < ‖x‖

Tactic:
choose x hx using NontriviallyNormedField.non_trivial (α := ℚ_[p])

Premises used: NontriviallyNormedField.non_trivial
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
h : 1 < Norm.norm (E := PadicAlgCl p) ((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x : PadicAlgCl p)
⊢ ∃ (x : PadicAlgCl p), 1 < ‖x‖

Tactic:
use x
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
h : 1 < ‖x‖
⊢ 1 < Norm.norm (E := PadicAlgCl p) ((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x : PadicAlgCl p)

Tactic:
rw [PadicAlgCl.norm_extends]

Premises used: PadicAlgCl.norm_extends
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ 1 < ‖x‖

Tactic:
hx
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ 1 < ‖x‖

Tactic:
exact hx
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ CharZero (PadicAlgCl p)

Tactic:
(RingHom.charZero_iff (algebraMap ℚ_[p] (PadicAlgCl p)).injective).mp inferInstance

Premises used: Algebra.algebraMap, inferInstance, RingHom.charZero_iff, RingHom.injective, Iff.mp, Padic, PadicAlgCl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ Eq (α := ℝ≥0)
    ((Valued.v : (a : UniformSpace.Completion (PadicAlgCl p)) → ℝ≥0) (↑x : UniformSpace.Completion (PadicAlgCl p)) :
      ℝ≥0)
    ((Valued.v : (a : PadicAlgCl p) → ℝ≥0) x : ℝ≥0)

Tactic:
Valued.extensionValuation_apply_coe _

Premises used: Valued.extensionValuation_apply_coe
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ Eq (α := UniformSpace.Completion (PadicAlgCl p)) (↑x : UniformSpace.Completion (PadicAlgCl p))
    ((algebraMap (PadicAlgCl p) ℂ_[p] : (a : PadicAlgCl p) → ℂ_[p]) x)

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := UniformSpace.Completion (PadicAlgCl p)) (↑0 : UniformSpace.Completion (PadicAlgCl p)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsScalarTower ℚ_[p] (PadicAlgCl p) ℂ_[p]

Tactic:
IsScalarTower.of_algebraMap_eq (congrFun rfl)

Premises used: congrFun, IsScalarTower.of_algebraMap_eq, rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
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))
rw₁ 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))
⊢ Eq (α := UniformSpace.Completion (PadicAlgCl p)) (↑(↑n : PadicAlgCl p) : UniformSpace.Completion (PadicAlgCl p))
    (↑n : ℂ_[p])

Tactic:
rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]) n, coe_eq]

Premises used: PadicComplex, PadicComplex.coe_eq, Algebra.algebraMap, map_natCast, PadicAlgCl
-- Module: Mathlib.NumberTheory.Padics.Complex
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)
rw₃ rw₄ : HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)
⊢ (Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p]) = HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)

Tactic:
rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]), ← coe_eq, valuation_extends,
    PadicAlgCl.valuation_p]

Premises used: PadicComplex, PadicComplex.valuation_extends, PadicComplex.coe_eq, Algebra.algebraMap, PadicAlgCl.valuation_p, map_natCast, PadicAlgCl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h :
  Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 0 ∧
    Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 1
⊢ ∃ (x : ℂ_[p]),
    Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ∧
      Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)

Tactic:
use p
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
hp : Nat.Prime p
h : ¬p = 0 ∧ ¬p = 1
⊢ Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[p])) 0 ∧
    Ne (α := ℝ≥0) ((Valued.v : (a : ℂ_[p]) → ℝ≥0) (↑p : ℂ_[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]

Premises used: inv_eq_zero, inv_eq_one, PadicComplex.valuation_p, ne_eq, Nat.cast_eq_zero, Nat.cast_eq_one, one_div
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := MonoidWithZeroHom.ValueGroup₀ (F := Valuation ℂ_[p] ℝ≥0) Valued.v →*₀ ℝ≥0) (RankOne.hom Valued.v) embedding

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℂ_[p] → ℝ) (fun (x : ℂ_[p]) ↦ ‖x‖) Norm.norm

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℂ_[p] → ℝ) (fun (x : ℂ_[p]) ↦ ‖x‖) Norm.norm

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ Norm.norm (E := UniformSpace.Completion (PadicAlgCl p)) (↑x : UniformSpace.Completion (PadicAlgCl p)) = ‖x‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ Norm.norm (E := UniformSpace.Completion (PadicAlgCl p))
      ((↑((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x) : UniformSpace.Completion (PadicAlgCl p)) :
        UniformSpace.Completion (PadicAlgCl p)) =
    ‖x‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsUltrametricDist ℂ_[p]

Tactic:
IsUltrametricDist.of_normedAlgebra ℚ_[p]

Premises used: IsUltrametricDist.of_normedAlgebra, Padic
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsNonarchimedean (α := ℂ_[p]) Norm.norm

Tactic:
IsUltrametricDist.norm_add_le_max

Premises used: IsUltrametricDist.norm_add_le_max, IsNonarchimedean
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hf : UniformContinuous (α := PadicAlgCl p) Norm.norm
hg : UniformContinuous (α := UniformSpace.Completion (PadicAlgCl p)) (Valuation.norm Valued.v)
h :
  ∀ (a : PadicAlgCl p),
    ‖a‖ =
      Valuation.norm (L := UniformSpace.Completion (PadicAlgCl p)) Valued.v
        (↑a : UniformSpace.Completion (PadicAlgCl p))
⊢ Eq (α := ℂ_[p] → ℝ) (fun (x : ℂ_[p]) ↦ ‖x‖) (Valuation.norm Valued.v)

Tactic:
apply UniformSpace.Completion.extension_unique (f := @norm (PadicAlgCl p) _) (g := Valued.v.norm)

Premises used: UniformSpace.Completion.extension_unique
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ UniformContinuous (α := PadicAlgCl p) Norm.norm

Tactic:
uniformContinuous_norm

Premises used: uniformContinuous_norm
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ UniformContinuous (α := PadicAlgCl p) Norm.norm

Tactic:
exact uniformContinuous_norm

Premises used: uniformContinuous_norm
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
S : SeminormedRing ℂ_[p] := NormedRing.toSeminormedRing
this : SeminormedAddGroup ℂ_[p] := SeminormedAddCommGroup.toSeminormedAddGroup
⊢ UniformContinuous (α := UniformSpace.Completion (PadicAlgCl p)) (Valuation.norm Valued.v)

Tactic:
@uniformContinuous_norm ℂ_[p] this

Premises used: uniformContinuous_norm
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
S : SeminormedRing ℂ_[p] := NormedRing.toSeminormedRing
this : SeminormedAddGroup ℂ_[p] := SeminormedAddCommGroup.toSeminormedAddGroup
⊢ UniformContinuous (α := UniformSpace.Completion (PadicAlgCl p)) (Valuation.norm Valued.v)

Tactic:
exact @uniformContinuous_norm ℂ_[p] this

Premises used: uniformContinuous_norm
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ ‖x‖ =
    Valuation.norm (L := UniformSpace.Completion (PadicAlgCl p)) Valued.v (↑x : UniformSpace.Completion (PadicAlgCl p))

Tactic:
simp [Valued.v.norm_def, restrict_def]

Premises used: Valued.v, Valuation.restrict_def, Valuation.norm_def
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℂ_[p]
h : Eq (α := ℂ_[p] → ℝ) Norm.norm (Valuation.norm Valued.v)
⊢ ‖x‖ = Valuation.norm Valued.v x

Tactic:
congr!
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℂ_[p]
⊢ Eq (α := ℂ_[p] → ℝ) Norm.norm (Valuation.norm Valued.v)

Tactic:
norm_eq_norm' p

Premises used: PadicComplex.norm_eq_norm'
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℂ_[p]
⊢ Eq (α := ℂ_[p] → ℝ) Norm.norm (Valuation.norm Valued.v)

Tactic:
exact norm_eq_norm' p

Premises used: PadicComplex.norm_eq_norm'
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
a :
  (↑(nnnorm (E := UniformSpace.Completion (PadicAlgCl p)) (↑x : UniformSpace.Completion (PadicAlgCl p))) : ℝ) =
    (↑‖x‖₊ : ℝ)
⊢ nnnorm (E := UniformSpace.Completion (PadicAlgCl p)) (↑x : UniformSpace.Completion (PadicAlgCl p)) = ‖x‖₊

Tactic:
ext
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ (↑(nnnorm (E := UniformSpace.Completion (PadicAlgCl p)) (↑x : UniformSpace.Completion (PadicAlgCl p))) : ℝ) =
    (↑‖x‖₊ : ℝ)

Tactic:
norm_extends p x

Premises used: PadicComplex.norm_extends, NNReal.toReal
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ (↑(nnnorm (E := UniformSpace.Completion (PadicAlgCl p)) (↑x : UniformSpace.Completion (PadicAlgCl p))) : ℝ) =
    (↑‖x‖₊ : ℝ)

Tactic:
exact norm_extends p x

Premises used: PadicComplex.norm_extends
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
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‖₊ : ℝ)
⊢ 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
-- Module: Mathlib.NumberTheory.Padics.Complex
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‖₊ : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
choose : ∀ (x : ℚ_[p]) (hx : 1 < ‖x‖), ∃ (x : ℂ_[p]), 1 < ‖x‖
⊢ ∃ (x : ℂ_[p]), 1 < ‖x‖

Tactic:
choose x hx using NontriviallyNormedField.non_trivial (α := ℚ_[p])

Premises used: NontriviallyNormedField.non_trivial
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
h :
  1 <
    Norm.norm (E := ℂ_[p])
      ((↑((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x) : UniformSpace.Completion (PadicAlgCl p)) :
        UniformSpace.Completion (PadicAlgCl p))
⊢ ∃ (x : ℂ_[p]), 1 < ‖x‖

Tactic:
use x
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ 1 <
    Norm.norm (E := ℂ_[p])
      ((↑((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x) : UniformSpace.Completion (PadicAlgCl p)) :
        UniformSpace.Completion (PadicAlgCl p))

Tactic:
simpa only [norm_extends']

Premises used: PadicComplex.norm_extends'
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ CharZero ℂ_[p]

Tactic:
(RingHom.charZero_iff (algebraMap ℚ_[p] ℂ_[p]).injective).mp inferInstance

Premises used: PadicComplex, Algebra.algebraMap, inferInstance, RingHom.charZero_iff, RingHom.injective, Iff.mp, Padic
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsAlgClosed ℂ_[p]

Tactic:
IsAlgClosed.of_denseRange UniformSpace.Completion.denseRange_coe

Premises used: IsAlgClosed.of_denseRange, UniformSpace.Completion.denseRange_coe
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Integers (R := ℂ_[p]) Valued.v ↥𝓞_ℂ_[p]

Tactic:
Valuation.integer.integers _

Premises used: Set.Mem, Subsemiring.ofClass, setOf, PadicComplexInt, Valuation.integer.integers, Valuation.integer, Valuation.valuationSubring
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
p : Nat.Primes
⊢ Fact (Nat.Prime (↑p : ℕ))

Tactic:
⟨p.2⟩

Premises used: Fact.mk, Subtype.property
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℚ
⊢ Function.Injective (α := ℤ) (β := R) (⇑(algebraMap ℤ R) : (a : ℤ) → R)

Tactic:
.of_comp (IsScalarTower.algebraMap_eq ℤ R ℚ ▸ RingHom.injective_int (algebraMap ℤ ℚ))

Premises used: Function.Injective.of_comp
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsFractionRing R ℚ
x : R
obtain :
  ∀ (y : ℤ) (hy : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) y : ℚ) ((algebraMap R ℚ : (a : R) → ℚ) x : ℚ)),
    ∃ (a : ℤ), (algebraMap ℤ R : (a : ℤ) → R) a = x
⊢ ∃ (a : ℤ), (algebraMap ℤ R : (a : ℤ) → R) a = x

Tactic:
obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.1 <|
    IsIntegral.algebraMap (B := ℚ) (IsIntegralClosure.isIntegral ℤ ℚ x)

Premises used: IsIntegrallyClosed.isIntegral_iff, Rat, IsIntegralClosure.isIntegral, Int, Iff.mp, IsIntegral.algebraMap
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsFractionRing R ℚ
x : R
y : ℤ
hy : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) y : ℚ) ((algebraMap R ℚ : (a : R) → ℚ) x : ℚ)
⊢ Eq (α := ℚ) ((algebraMap R ℚ : (a : R) → ℚ) ((algebraMap ℤ R : (a : ℤ) → R) y : R) : ℚ)
    ((algebraMap R ℚ : (a : R) → ℚ) x : ℚ)

Tactic:
simp only [← IsScalarTower.algebraMap_apply, hy]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsFractionRing R ℚ
x : R
y : ℤ
hy : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) y : ℚ) ((algebraMap R ℚ : (a : R) → ℚ) x : ℚ)
⊢ ∃ (a : ℤ), (algebraMap ℤ R : (a : ℤ) → R) a = x

Tactic:
exact ⟨y, IsFractionRing.injective R ℚ <| by simp only [← IsScalarTower.algebraMap_apply, hy]⟩
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
x : 𝓞 ℚ
⊢ Eq (α := ℤ) ((intEquiv (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) x : ℤ) ((ringOfIntegersEquiv : (a : 𝓞 ℚ) → ℤ) x : ℤ)

Tactic:
simp [intEquiv, RingOfIntegers.equiv, IsIntegralClosure.equiv, IsIntegralClosure.lift,
    IsIntegralClosure.mk']

Premises used: Rat.IsIntegralClosure.intEquiv, IsIntegralClosure.equiv, NumberField.RingOfIntegers.equiv, IsIntegralClosure.mk', IsIntegralClosure.lift
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
⊢ Eq (α := Ideal ℤ) (Ideal.span {(↑(natGenerator v) : ℤ)})
    (Ideal.map (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) v.asIdeal)

Tactic:
simp [natGenerator]

Premises used: Rat.HeightOneSpectrum.natGenerator
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
n : ℕ
rw : natGenerator v ∣ n ↔ Dvd.dvd (α := ℤ) (↑(natGenerator v) : ℤ) (↑n : ℤ)
⊢ natGenerator v ∣ n ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.map (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) v.asIdeal) (↑n : ℤ)

Tactic:
rw [← span_natGenerator, Ideal.mem_span_singleton]

Premises used: Rat.HeightOneSpectrum.span_natGenerator, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
n : ℕ
⊢ natGenerator v ∣ n ↔ Dvd.dvd (α := ℤ) (↑(natGenerator v) : ℤ) (↑n : ℤ)

Tactic:
Int.ofNat_dvd.symm

Premises used: Int.ofNat_dvd, Iff.symm
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
n : ℕ
⊢ natGenerator v ∣ n ↔ Dvd.dvd (α := ℤ) (↑(natGenerator v) : ℤ) (↑n : ℤ)

Tactic:
exact Int.ofNat_dvd.symm

Premises used: Int.ofNat_dvd, Iff.symm
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
⊢ Nat.Prime (natGenerator v)

Tactic:
Int.prime_iff_natAbs_prime.1 <| Submodule.IsPrincipal.prime_generator_of_isPrime _
    ((Ideal.map_eq_bot_iff_of_injective (IsIntegralClosure.intEquiv R).injective).not.2 v.ne_bot)

Premises used: Iff.mpr, Rat.IsIntegralClosure.intEquiv, RingEquiv.injective, Iff.not, Ideal.map_eq_bot_iff_of_injective, IsDedekindDomain.HeightOneSpectrum.ne_bot, Submodule.IsPrincipal.prime_generator_of_isPrime, Rat.HeightOneSpectrum.natGenerator, Iff.mp, Int.prime_iff_natAbs_prime
-- 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
⊢ Prime (M := Ideal ℤ) (Ideal.span {(↑(↑p : ℕ) : ℤ)})

Tactic:
simp [← Nat.prime_iff_prime_int, p.2]

Premises used: Nat.prime_iff_prime_int, Subtype.property
-- 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
⊢ Ne (α := Ideal ℤ) (Ideal.span {(↑(↑p : ℕ) : ℤ)}) ⊥

Tactic:
simp [p.2.ne_zero]

Premises used: Nat.Prime.ne_zero, Subtype.property
-- 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
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (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

Tactic:
simp only [Ideal.map_symm]

Premises used: Ideal.map_symm
-- 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
e_p : Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}) = v.asIdeal
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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 ℚ
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))
e_p₁ 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) : ℤ)}))
⊢ Ideal.comap (F := R ≃+* ℤ) (IsIntegralClosure.intEquiv R) (Ideal.span {(↑(natGenerator v) : ℤ)}) = v.asIdeal

Tactic:
rw [← v.asIdeal.comap_map_of_bijective _ (IsIntegralClosure.intEquiv R).bijective,
      ← span_natGenerator]

Premises used: Rat.IsIntegralClosure.intEquiv, Rat.HeightOneSpectrum.span_natGenerator, Ideal.comap_map_of_bijective, RingEquiv.bijective
-- 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
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 : ℕ) : ℤ)})))))
      ⋯ =
    p
⊢ (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

Tactic:
simp only [Ideal.map_symm, natGenerator, HeightOneSpectrum.ofPrime_asIdeal]

Premises used: IsDedekindDomain.HeightOneSpectrum.ofPrime_asIdeal, Ideal.map_symm, Rat.HeightOneSpectrum.natGenerator