awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h_1 :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∃ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P ∧
          (⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
            Submodule.IsPrincipal P)
p : ℕ
hpmem :
  p ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
h_2 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
h :
  ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
    p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P
⊢ Submodule.IsPrincipal P
have linarith : -1 +
      (HPow.hPow (α := ℤ) (↑p : ℤ) (inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) -
        (↑⌊(4 / π) ^ nrComplexPlaces K *
                ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                  √|(↑(discr K) : ℝ)|)⌋₊ :
          ℤ)) +
    (HAdd.hAdd (α := ℤ)
        (↑⌊(4 / π) ^ nrComplexPlaces K *
                ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                  √|(↑(discr K) : ℝ)|)⌋₊ :
          ℤ)
        1 -
      HPow.hPow (α := ℤ) (↑p : ℤ) (inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P)) =
  0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h_1 :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∃ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P ∧
          (⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
            Submodule.IsPrincipal P)
p : ℕ
hpmem :
  p ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
h_2 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
h :
  ¬⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P
⊢ Submodule.IsPrincipal P
have H₁ : ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
    p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
  Submodule.IsPrincipal Q
Tactic: rw [inertiaDeg_eq_of_isGaloisGroup _ Q P (K ≃ₐ[ℚ] K)] at H
Cleared hypotheses: H, hQ1, hQ2, this, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h_1 :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∃ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P ∧
          (⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
            Submodule.IsPrincipal P)
p : ℕ
hpmem :
  p ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
h_2 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
h :
  ¬⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P
⊢ Submodule.IsPrincipal P
have neg : ∀ (σ : Gal(K/ℚ)),
  Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) (σ • Q) →
    ∀
      (hple :
        p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q) ≤
          ⌊(4 / π) ^ nrComplexPlaces K *
              ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊)
      (hP1 : (σ • Q).IsPrime) (hP2 : (σ • Q).LiesOver (A := ℤ) (span {(↑p : ℤ)}))
      (H :
        ⌊(4 / π) ^ nrComplexPlaces K *
                ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                  √|(↑(discr K) : ℝ)|)⌋₊ <
            p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q) ∨
          Submodule.IsPrincipal Q)
      (h :
        ¬⌊(4 / π) ^ nrComplexPlaces K *
                ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                  √|(↑(discr K) : ℝ)|)⌋₊ <
            p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q)),
      Submodule.IsPrincipal (σ • Q)
Tactic: obtain ⟨σ, rfl⟩ := exists_smul_eq_of_isGaloisGroup (span ({↑p} : Set ℤ)) Q P (K ≃ₐ[ℚ] K)
Cleared hypotheses: P, h_2, hple, hP1, hP2, H, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (↑|discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ)))
      2
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)
have this : 0 < finrank ℚ K
Tactic: have : 0 < finrank ℚ K := finrank_pos
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (↑|discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ)))
      2
this : 0 < finrank ℚ K
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)
have h₁ : (4 / π) ^ nrComplexPlaces K *
    ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) <
  2
Tactic: rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff₀' (by positivity),
    mul_inv, ← inv_pow, inv_div, inv_div, mul_assoc, Int.cast_abs] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)
have refine : ∀ (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 (↑I : Ideal (𝓞 K))
Tactic: refine isPrincipalIdealRing_of_isPrincipal_of_norm_le (fun I hI ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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 (↑I : Ideal (𝓞 K))
have rw : Submodule.IsPrincipal.{u_1, u_1} (R := 𝓞 K) («M» := 𝓞 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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)
⊢ IsPrincipalIdealRing.{u_2} ↥(Valuation.integer (valuation K v))
have rw : ¬Set.Subsingleton (α := WithZero (Multiplicative ℤ))
    (Set.range (ι := K) (⇑(valuation K v) : (a : K) → WithZero (Multiplicative ℤ)))
Tactic: rw [(Valuation.integer.integers (v.valuation K)).isPrincipalIdealRing_iff_not_denselyOrdered,
    WithZero.denselyOrdered_set_iff_subsingleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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)
⊢ IsPrincipalIdealRing.{u_2} ↥(Valuation.valuationSubring Valued.v)
have rw : ¬Set.Subsingleton (α := WithZero (Multiplicative ℤ))
    (Set.range.{0, u_2 + 1} (ι := adicCompletion K v)
      (⇑Valued.v : (a : adicCompletion K v) → WithZero (Multiplicative ℤ)))
Tactic: rw [(Valuation.valuationSubring.integers (Valued.v)).isPrincipalIdealRing_iff_not_denselyOrdered,
    WithZero.denselyOrdered_set_iff_subsingleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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)
⊢ Ne.{u_2 + 1} (α := Ideal ↥(Valuation.valuationSubring Valued.v))
    (IsLocalRing.maximalIdeal ↥(Valuation.valuationSubring Valued.v)) ⊥
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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 ℤ))
⊢ ∃ (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)
have 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))
Tactic: use (WithVal.equiv (v.valuation K)).symm π
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
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
⊢ ∃ (γ : (WithZero (Multiplicative ℤ))ˣ),
    Subgroup.zpowers γ =
        MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v ∧
      γ < 1
have h : Valuation.IsRankOneDiscrete (valuation K v)
Tactic: have h : (v.valuation K).IsRankOneDiscrete := Valuation.IsRankOneDiscrete.mk' (valuation K v)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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)
⊢ Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator (valuation K v)) =
    MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v
have rw : MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v) =
  MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v
Tactic: rw [h.generator_zpowers_eq_valueGroup, adicCompletion_valueGroup_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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
⊢ Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator (valuation K v)) =
    MonoidWithZeroHom.valueGroup (F := Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) Valued.v
have rw₁ : MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v) =
  MonoidWithZeroHom.valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K v)
Tactic: rw [h.generator_zpowers_eq_valueGroup, adicCompletion_valueGroup_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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 (α := ℕ) (1 : ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ)
have by_contra! : ∀ (h : LE.le (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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 : ℕ)
⊢ False
have apply : v.asIdeal = ⊤
Tactic: apply IsPrime.ne_top v.isPrime
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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 : ℕ)
⊢ v.asIdeal = ⊤
have rw : Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
Tactic: rw [← absNorm_eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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 : ℕ)
have rw : Finite.{u_2 + 1} (R ⧸ v.asIdeal)
Tactic: rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
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 : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) v.asIdeal : ℕ) (1 : ℕ)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
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
⊢ norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) x : adicCompletion K v) =
    (↑((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)) :
      ℝ)
have rw : (HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) x =
  (↑((toNNReal (e := (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0)) sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x)) :
    ℝ)
Tactic: rw [norm_embedding, adicAbv_def]