awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) <
    2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
rw : Submodule.IsPrincipal.{u_1, u_1} (R := 𝓞 K) («M» := 𝓞 K) ⊤
⊢ Submodule.IsPrincipal (↑I : Ideal (𝓞 K))

Tactic:
rw [absNorm_eq_one_iff.mp <| le_antisymm (Nat.lt_succ_iff.mp (cast_lt.mp
    (lt_of_le_of_lt hI h))) <| one_le_iff_ne_zero.mpr (absNorm_ne_zero_of_nonZeroDivisors I)]

Premises used: Iff.mpr, lt_of_le_of_lt, le_antisymm, Nat.lt_succ_iff, Ideal.absNorm_eq_one_iff, Iff.mp, Nat.one_le_iff_ne_zero, Nat.cast_lt, Ideal.absNorm_ne_zero_of_nonZeroDivisors
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) <
    2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
⊢ Submodule.IsPrincipal.{u_1, u_1} (R := 𝓞 K) («M» := 𝓞 K) ⊤

Tactic:
top_isPrincipal

Premises used: top_isPrincipal
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) <
    2
this : 0 < finrank ℚ K
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
⊢ Submodule.IsPrincipal.{u_1, u_1} (R := 𝓞 K) («M» := 𝓞 K) ⊤

Tactic:
exact top_isPrincipal

Premises used: top_isPrincipal
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
⊢ classNumber ℚ = 1

Tactic:
classNumber_eq_one_iff.mpr <| IsPrincipalIdealRing.of_surjective
    Rat.ringOfIntegersEquiv.symm Rat.ringOfIntegersEquiv.symm.surjective

Premises used: Iff.mpr, RingEquiv.surjective, IsPrincipalIdealRing.of_surjective, Rat.ringOfIntegersEquiv, NumberField.classNumber_eq_one_iff, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
rw :
  ¬Set.Subsingleton (α := WithZero (Multiplicative ℤ))
      (Set.range (ι := K) (⇑(valuation K v) : (a : K) → WithZero (Multiplicative ℤ)))
⊢ IsPrincipalIdealRing.{u_2} ↥(Valuation.integer (valuation K v))

Tactic:
rw [(Valuation.integer.integers (v.valuation K)).isPrincipalIdealRing_iff_not_denselyOrdered,
    WithZero.denselyOrdered_set_iff_subsingleton]

Premises used: Valuation.integer.integers, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered, WithZero.denselyOrdered_set_iff_subsingleton, IsDedekindDomain.HeightOneSpectrum.valuation
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
⊢ ¬Set.Subsingleton (α := WithZero (Multiplicative ℤ))
      (Set.range (ι := K) (⇑(valuation K v) : (a : K) → WithZero (Multiplicative ℤ)))

Tactic:
simpa using (v.valuation K).toMonoidWithZeroHom.range_nontrivial

Premises used: MonoidWithZeroHom.range_nontrivial, Valuation.toMonoidWithZeroHom, IsDedekindDomain.HeightOneSpectrum.valuation
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
⊢ IsDiscreteValuationRing.{u_2} ↥(Valuation.integer (valuation K v))

Tactic:
(v.valuation K).valuationSubring_isDiscreteValuationRing

Premises used: Set.Mem, Valuation.valuationSubring_isDiscreteValuationRing, IsDedekindDomain.HeightOneSpectrum.valuation, Valuation.integer, Valuation.valuationSubring
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
rw :
  ¬Set.Subsingleton (α := WithZero (Multiplicative ℤ))
      (Set.range.{0, u_2 + 1} (ι := adicCompletion K v)
        (⇑Valued.v : (a : adicCompletion K v) → WithZero (Multiplicative ℤ)))
⊢ IsPrincipalIdealRing.{u_2} ↥(Valuation.valuationSubring Valued.v)

Tactic:
rw [(Valuation.valuationSubring.integers (Valued.v)).isPrincipalIdealRing_iff_not_denselyOrdered,
    WithZero.denselyOrdered_set_iff_subsingleton]

Premises used: Valued.v, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered, WithZero.denselyOrdered_set_iff_subsingleton, Valuation.valuationSubring.integers
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
⊢ ¬Set.Subsingleton (α := WithZero (Multiplicative ℤ))
      (Set.range.{0, u_2 + 1} (ι := adicCompletion K v)
        (⇑Valued.v : (a : adicCompletion K v) → WithZero (Multiplicative ℤ)))

Tactic:
simpa using Valued.v.range_nontrivial

Premises used: Valued.v, MonoidWithZeroHom.range_nontrivial, Valuation.toMonoidWithZeroHom
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
simp :
  ∃ (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 ℤ))
            (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                x :
              WithZero (Multiplicative ℤ))
            (1 : WithZero (Multiplicative ℤ)) ↔
          x = 0)
⊢ Ne.{u_2 + 1} (α := Ideal ↥(Valuation.valuationSubring Valued.v))
    (IsLocalRing.maximalIdeal ↥(Valuation.valuationSubring Valued.v)) ⊥

Tactic:
simp only [ne_eq, Ideal.ext_iff, Valuation.mem_maximalIdeal_iff, Ideal.mem_bot, Subtype.ext_iff,
      ZeroMemClass.coe_zero, Subtype.forall, Valuation.mem_valuationSubring_iff, not_forall,
      exists_prop]

Premises used: Ideal.mem_bot, Valuation.mem_maximalIdeal_iff, Valuation.mem_valuationSubring_iff, Subtype.forall, exists_prop, ne_eq, Subtype.ext_iff, ZeroMemClass.coe_zero, Ideal.ext_iff, Classical.not_forall
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
obtain :
  ∀ (π : K)
    (hπ :
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
          WithZero (Multiplicative ℤ))
        (exp (-1) : WithZero (Multiplicative ℤ))),
    ∃ (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 ℤ))
              (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                    (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                  x :
                WithZero (Multiplicative ℤ))
              (1 : WithZero (Multiplicative ℤ)) ↔
            x = 0)
⊢ ∃ (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 ℤ))
            (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                x :
              WithZero (Multiplicative ℤ))
            (1 : WithZero (Multiplicative ℤ)) ↔
          x = 0)

Tactic:
obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
π : K
hπ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
h :
  LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) π) :
            UniformSpace.Completion (WithVal (valuation K v))) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ∧
    ¬(LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
              (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) π) :
                UniformSpace.Completion (WithVal (valuation K v))) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ↔
        Eq (α := adicCompletion K v)
          ((↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) π) :
              UniformSpace.Completion (WithVal (valuation K v))) :
            UniformSpace.Completion (WithVal (valuation K v)))
          (0 : adicCompletion K v))
⊢ ∃ (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 ℤ))
            (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                x :
              WithZero (Multiplicative ℤ))
            (1 : WithZero (Multiplicative ℤ)) ↔
          x = 0)

Tactic:
use (WithVal.equiv (v.valuation K)).symm π

Premises used: WithVal.equiv, IsDedekindDomain.HeightOneSpectrum.valuation, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
K : Type u_2
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite.{u_1 + 1} (A ⧸ v.asIdeal)
π : K
hπ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) π :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) π) :
            UniformSpace.Completion (WithVal (valuation K v))) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ∧
    ¬(LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
              (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) π) :
                UniformSpace.Completion (WithVal (valuation K v))) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ↔
        Eq (α := adicCompletion K v)
          ((↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) π) :
              UniformSpace.Completion (WithVal (valuation K v))) :
            UniformSpace.Completion (WithVal (valuation K v)))
          (0 : adicCompletion K v))

Tactic:
simp [hπ, ← exp_zero, -exp_neg,
      ← (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰).map_eq_zero_iff]

Premises used: MonoidWithZeroHom.map_eq_zero_iff, WithZero.exp_zero, WithZero.exp_neg
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
⊢ Eq (α := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) x : adicCompletion K v)
    ((↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) x) :
        UniformSpace.Completion (WithVal (valuation K v))) :
      UniformSpace.Completion (WithVal (valuation K v)))

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Valuation.IsRankOneDiscrete (valuation K v)

Tactic:
have h : (v.valuation K).IsRankOneDiscrete := Valuation.IsRankOneDiscrete.mk' (valuation K v)
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
h : Valuation.IsRankOneDiscrete (valuation K v)
rw :
  MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v) =
    MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v
rw₁ rw₂ :
  MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v) =
    MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v)
⊢ Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator (valuation K v)) =
    MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v

Tactic:
rw [h.generator_zpowers_eq_valueGroup, adicCompletion_valueGroup_eq]

Premises used: Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
h : Valuation.IsRankOneDiscrete (valuation K v)
⊢ ∃ (γ : (WithZero (Multiplicative ℤ))ˣ),
    Subgroup.zpowers γ =
        MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v ∧
      γ < 1

Tactic:
exact ⟨h.generator, by rw [h.generator_zpowers_eq_valueGroup, adicCompletion_valueGroup_eq],
      h.generator_lt_one⟩
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
by_contra! : ∀ (h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)), False
⊢ LT.lt (α := ℕ) (1 : ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ)

Tactic:
by_contra! h
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
apply : v.asIdeal = ⊤
⊢ False

Tactic:
apply IsPrime.ne_top v.isPrime

Premises used: IsDedekindDomain.HeightOneSpectrum.isPrime, Ideal.IsPrime.ne_top
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
rw : Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
⊢ v.asIdeal = ⊤

Tactic:
rw [← absNorm_eq_one_iff]

Premises used: Ideal.absNorm_eq_one_iff
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
rw : Finite.{u_2 + 1} (R ⧸ v.asIdeal)
⊢ LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ)

Tactic:
rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff]

Premises used: Nat.pos_iff_ne_zero, Ideal.absNorm_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
⊢ Finite.{u_2 + 1} (R ⧸ v.asIdeal)

Tactic:
v.asIdeal.finiteQuotientOfFreeOfNeBot v.ne_bot

Premises used: IsDedekindDomain.HeightOneSpectrum.asIdeal, IsDedekindDomain.HeightOneSpectrum.ne_bot, Ideal.finiteQuotientOfFreeOfNeBot
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
⊢ Finite.{u_2 + 1} (R ⧸ v.asIdeal)

Tactic:
exact v.asIdeal.finiteQuotientOfFreeOfNeBot v.ne_bot

Premises used: IsDedekindDomain.HeightOneSpectrum.asIdeal, IsDedekindDomain.HeightOneSpectrum.ne_bot, Ideal.finiteQuotientOfFreeOfNeBot
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
⊢ LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ)

Tactic:
have : 0 < absNorm v.asIdeal := by
    rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff]
    exact v.asIdeal.finiteQuotientOfFreeOfNeBot v.ne_bot
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
this : LT.lt (α := ℕ) (0 : ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)

Tactic:
lia
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
⊢ LT.lt (α := ℝ≥0) 1 (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0)

Tactic:
mod_cast one_lt_absNorm v

Premises used: Ideal.absNorm, congrArg, Nat.cast_lt._simp_1, cast, IsDedekindDomain.HeightOneSpectrum.asIdeal, Nat.cast, LT.lt, congrFun', NumberField.HeightOneSpectrum.one_lt_absNorm, Eq.symm, Nat.cast_one, DFunLike.coe, Eq.trans
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
inst_2 : Module.Finite ℤ R
inst_3 : Module.Free ℤ R
⊢ Ne (α := ℝ≥0) (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0) 0

Tactic:
ne_zero_of_lt (one_lt_absNorm_nnreal v)

Premises used: ne_zero_of_lt, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
inst_5 : Module.Finite ℤ R
inst_6 : Module.Free ℤ R
x : K
⊢ (adicAbv K v : (a : K) → ℝ) x =
    (↑((toNNReal (e := (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0)) ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x)) :
      ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
inst_5 : Module.Finite ℤ R
inst_6 : Module.Free ℤ R
⊢ IsNonarchimedean (R := ℝ) (α := K) (⇑(adicAbv K v) : (a : K) → ℝ)

Tactic:
v.isNonarchimedean_adicAbv <| one_lt_absNorm_nnreal v

Premises used: IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
inst_5 : Module.Finite ℤ R
inst_6 : Module.Free ℤ R
⊢ Eq (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v →*₀ ℝ≥0)
    (Valuation.RankLeOne.hom' Valued.v)
    ((toNNReal (e := (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0)) ⋯).comp
      (MulEquiv.toMonoidWithZeroHom (valueGroup₀_equiv_withZeroMulInt Valued.v)))

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl, MulEquiv.toMonoidWithZeroHom
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R K
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
inst_5 : Module.Finite ℤ R
inst_6 : Module.Free ℤ R
x : WithVal (valuation K v)
⊢ (↑((toNNReal (e := (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0)) ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((Valued.v : Valuation (WithVal (valuation K v)) (WithZero (Multiplicative ℤ))) :
              (a : WithVal (valuation K v)) → WithZero (Multiplicative ℤ))
            x)) :
      ℝ) =
    (adicAbv K v : (a : K) → ℝ) ((WithVal.equiv (valuation K v) : (a : WithVal (valuation K v)) → K) x : K)

Tactic:
rfl

Premises used: NNReal.toReal, rfl