awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  (HeightOneSpectrum.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)) :
      ℝ)
⊢ 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₁ : (↑((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)) :
    ℝ) =
  (↑((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]
-- 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 : R
⊢ norm.{u_1} (E := adicCompletion K v)
      ((embedding v : (a : K) → adicCompletion K v) ((algebraMap R K : (a : R) → K) x) : adicCompletion K v) ≤
    1
have rw : LE.le (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ)
Tactic: rw [norm_embedding]
-- 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 : R
⊢ norm.{u_1} (E := adicCompletion K v)
        ((embedding v : (a : K) → adicCompletion K v) ((algebraMap R K : (a : R) → K) x) : adicCompletion K v) =
      1 ↔
    x ∉ v.asIdeal
have rw : Eq (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ) ↔
  x ∉ v.asIdeal
Tactic: rw [norm_embedding]
-- 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 : R
⊢ norm.{u_1} (E := adicCompletion K v)
        ((embedding v : (a : K) → adicCompletion K v) ((algebraMap R K : (a : R) → K) x) : adicCompletion K v) <
      1 ↔
    x ∈ v.asIdeal
have rw : LT.lt (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ) ↔
  x ∈ v.asIdeal
Tactic: rw [norm_embedding]
-- 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 : R
h_x_nezero : x ≠ 0
⊢ norm.{u_1} (E := adicCompletion K v)
        ((embedding v : (a : K) → adicCompletion K v) ((algebraMap R K : (a : R) → K) x) : adicCompletion K v) *
      (↑((absNorm : (a : Ideal R) → ℕ) (v.maxPowDividing (span {x}))) : ℝ) =
    1
have rw : (↑(HPow.hPow (α := ℝ≥0) (β := ℤ) (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0)
          ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
              (unzero (x :=
                ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
                  ((algebraMap R K : (a : R) → K) x))
                sorry) :
            ℤ)) :
      ℝ) *
    HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ)
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) =
  1
Tactic: rw [maxPowDividing, map_pow, Nat.cast_pow, norm_embedding, adicAbv_def,
    WithZeroMulInt.toNNReal_neg_apply _ ((v.valuation K).ne_zero_iff.mpr
      ((FaithfulSMul.algebraMap_eq_zero_iff R K).not.2 h_x_nezero))]
-- 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 : R
h_x_nezero : x ≠ 0
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ)
        ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
            (unzero (x :=
              ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
                ((algebraMap R K : (a : R) → K) x))
              ⋯) :
          ℤ) *
      HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ)
        (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) =
    1
have rw : HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ)
    (HAdd.hAdd (α := ℤ) (β := ℤ)
      ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
          (unzero (x :=
            ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
              ((algebraMap R K : (a : R) → K) x))
            sorry) :
        ℤ)
      ((↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) : ℤ) : ℤ)) =
  1
Tactic: rw [← zpow_natCast, ← zpow_add₀ <| mod_cast (zero_lt_one.trans (one_lt_absNorm_nnreal v)).ne']
-- 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 : R
h_x_nezero : x ≠ 0
⊢ HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ)
      (HAdd.hAdd (α := ℤ) (β := ℤ)
        ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
            (unzero (x :=
              ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
                ((algebraMap R K : (a : R) → K) x))
              ⋯) :
          ℤ)
        ((↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) : ℤ) : ℤ)) =
    1
have rw : HAdd.hAdd (α := ℤ) (β := ℤ)
    ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
        (unzero (x :=
          ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            ((algebraMap R K : (a : R) → K) x))
          sorry) :
      ℤ)
    ((↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) : ℤ) : ℤ) =
  0
Tactic: rw [zpow_eq_one_iff_right₀ (Nat.cast_nonneg' _) (mod_cast (one_lt_absNorm_nnreal v).ne')]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : FinitePlace K
x : K
| (w : (a : K) → ℝ) x
have rw : norm (E := adicCompletion K w.maximalIdeal)
  ((embedding w.maximalIdeal : (a : K) → adicCompletion K w.maximalIdeal) x : adicCompletion K w.maximalIdeal)
Tactic: rw [← mk_maximalIdeal w, mk_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : FinitePlace K
x : K
⊢ norm (E := adicCompletion K w.maximalIdeal)
      ((embedding w.maximalIdeal : (a : K) → adicCompletion K w.maximalIdeal) x : adicCompletion K w.maximalIdeal) =
    (w : (a : K) → ℝ) x
have conv_rhs : norm (E := adicCompletion K w.maximalIdeal)
    ((embedding w.maximalIdeal : (a : K) → adicCompletion K w.maximalIdeal) x : adicCompletion K w.maximalIdeal) =
  (w : (a : K) → ℝ) x
Tactic: conv_rhs => rw [← mk_maximalIdeal w, mk_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : FinitePlace K
x : K
conv_rhs :
  norm (E := adicCompletion K w.maximalIdeal)
      ((embedding w.maximalIdeal : (a : K) → adicCompletion K w.maximalIdeal) x : adicCompletion K w.maximalIdeal) =
    (w : (a : K) → ℝ) x
⊢ norm (E := adicCompletion K w.maximalIdeal)
      ((embedding w.maximalIdeal : (a : K) → adicCompletion K w.maximalIdeal) x : adicCompletion K w.maximalIdeal) =
    (w : (a : K) → ℝ) x
have conv_rhs₁ : norm (E := adicCompletion K w.maximalIdeal)
    ((embedding w.maximalIdeal : (a : K) → adicCompletion K w.maximalIdeal) x : adicCompletion K w.maximalIdeal) =
  norm (E := adicCompletion K w.maximalIdeal)
    ((embedding w.maximalIdeal : (a : K) → adicCompletion K w.maximalIdeal) x : adicCompletion K w.maximalIdeal)
Tactic: conv_rhs => rw [← mk_maximalIdeal w, mk_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
a : v₁ = v₂
⊢ Eq (α := FinitePlace K) (mk v₁) (mk v₂)
have rw : Eq (α := FinitePlace K) (mk v₂) (mk v₂)
Tactic: rw [a]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ Eq (α := FinitePlace K) (mk v₁) (mk v₂) ↔ v₁ = v₂
have refine : Eq (α := FinitePlace K) (mk v₁) (mk v₂) → v₁ = v₂
Tactic: refine ⟨?_, fun a ↦ by rw [a]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ Eq (α := FinitePlace K) (mk v₁) (mk v₂) → v₁ = v₂
have contrapose! : v₁ ≠ v₂ → Ne (α := FinitePlace K) (mk v₁) (mk v₂)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ Ne (α := FinitePlace K) (mk v₁) (mk v₂)
have rw : ∃ (a : K), Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) a : ℝ) ((mk v₂ : (a : K) → ℝ) a : ℝ)
Tactic: rw [DFunLike.ne_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ x ∈ v₁.asIdeal, x ∉ v₂.asIdeal
have by_contra! : ∀ (H : ∀ (x : 𝓞 K) (_ : x ∈ v₁.asIdeal), x ∈ v₂.asIdeal), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ (a : K), Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) a : ℝ) ((mk v₂ : (a : K) → ℝ) a : ℝ)
have have : ∀ (x : 𝓞 K) (hx1 : x ∈ v₁.asIdeal) (hx2 : x ∉ v₂.asIdeal),
  ∃ (a : K), Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) a : ℝ) ((mk v₂ : (a : K) → ℝ) a : ℝ)
Tactic: have ⟨x, hx1, hx2⟩ : ∃ x : 𝓞 K, x ∈ v₁.asIdeal ∧ x ∉ v₂.asIdeal := by
    by_contra! H
    exact h <| HeightOneSpectrum.ext_iff.mpr <| IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ ∃ (a : K), Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) a : ℝ) ((mk v₂ : (a : K) → ℝ) a : ℝ)
have h₁ : Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) (↑x : K) : ℝ) ((mk v₂ : (a : K) → ℝ) (↑x : K) : ℝ)
Tactic: use x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ norm (E := adicCompletion K v₁) ((embedding v₁ : (a : K) → adicCompletion K v₁) (↑x : K) : adicCompletion K v₁) ≠
    norm (E := adicCompletion K v₂) ((embedding v₂ : (a : K) → adicCompletion K v₂) (↑x : K) : adicCompletion K v₂)
have hx1₁ : norm (E := adicCompletion K v₁)
    ((embedding v₁ : (a : K) → adicCompletion K v₁) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : adicCompletion K v₁) <
  1
Tactic: rw [← norm_lt_one_iff_mem K] at hx1
Cleared hypotheses: hx1, hx2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 :
  norm (E := adicCompletion K v₁)
      ((embedding v₁ : (a : K) → adicCompletion K v₁) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : adicCompletion K v₁) <
    1
hx2 : x ∉ v₂.asIdeal
⊢ norm (E := adicCompletion K v₁) ((embedding v₁ : (a : K) → adicCompletion K v₁) (↑x : K) : adicCompletion K v₁) ≠
    norm (E := adicCompletion K v₂) ((embedding v₂ : (a : K) → adicCompletion K v₂) (↑x : K) : adicCompletion K v₂)
have hx2₁ : norm (E := adicCompletion K v₂)
    ((embedding v₂ : (a : K) → adicCompletion K v₂) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : adicCompletion K v₂) =
  1
Tactic: rw [← norm_eq_one_iff_notMem K] at hx2
Cleared hypotheses: hx2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 :
  norm (E := adicCompletion K v₁)
      ((embedding v₁ : (a : K) → adicCompletion K v₁) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : adicCompletion K v₁) <
    1
hx2 :
  norm (E := adicCompletion K v₂)
      ((embedding v₂ : (a : K) → adicCompletion K v₂) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : adicCompletion K v₂) =
    1
⊢ norm (E := adicCompletion K v₁) ((embedding v₁ : (a : K) → adicCompletion K v₁) (↑x : K) : adicCompletion K v₁) ≠
    norm (E := adicCompletion K v₂) ((embedding v₂ : (a : K) → adicCompletion K v₂) (↑x : K) : adicCompletion K v₂)
have linarith : norm (E := adicCompletion K v₁) ((embedding v₁ : (a : K) → adicCompletion K v₁) (↑x : K) : adicCompletion K v₁) =
    norm (E := adicCompletion K v₂) ((embedding v₂ : (a : K) → adicCompletion K v₂) (↑x : K) : adicCompletion K v₂) →
  norm (E := adicCompletion K v₁)
            ((embedding v₁ : (a : K) → adicCompletion K v₁) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) :
              adicCompletion K v₁) -
          1 +
        -(norm (E := adicCompletion K v₂)
              ((embedding v₂ : (a : K) → adicCompletion K v₂) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) :
                adicCompletion K v₂) -
            1) +
      -(norm (E := adicCompletion K v₁)
            ((embedding v₁ : (a : K) → adicCompletion K v₁) (↑x : K) : adicCompletion K v₁) -
          norm (E := adicCompletion K v₂)
            ((embedding v₂ : (a : K) → adicCompletion K v₂) (↑x : K) : adicCompletion K v₂)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : HeightOneSpectrum (𝓞 K)
⊢ maximalIdeal (mk v) = v
have rw : Eq (α := FinitePlace K) (mk (maximalIdeal (mk v))) (mk v)
Tactic: rw [← mk_eq_iff, mk_maximalIdeal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : HeightOneSpectrum (𝓞 K)
rw : Eq (α := FinitePlace K) (mk (maximalIdeal (mk v))) (mk v)
⊢ maximalIdeal (mk v) = v
have rw₁ : Eq (α := FinitePlace K) (mk v) (mk v)
Tactic: rw [← mk_eq_iff, mk_maximalIdeal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦ (w : (a : K) → ℝ) (↑x : K)
have this : ∀ (w : FinitePlace K),
  Ne (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
Tactic: have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 :=
    ne_iff_lt_iff_le.mpr <| norm_embedding_eq w x ▸ norm_le_one K w.maximalIdeal x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this :
  ∀ (w : FinitePlace K),
    Ne (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦ (w : (a : K) → ℝ) (↑x : K)
have simp_rw : Set.Finite.{u_1} (α := FinitePlace K) {x_1 : FinitePlace K | x_1.maximalIdeal.asIdeal ∣ span {x}}
Tactic: simp_rw [Function.HasFiniteMulSupport, Function.mulSupport, this, ← norm_embedding_eq,
    norm_lt_one_iff_mem, ← Ideal.dvd_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this :
  ∀ (w : FinitePlace K),
    Ne (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
⊢ Set.Finite.{u_1} (α := HeightOneSpectrum (𝓞 K)) {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}
have hI : Ne (α := Ideal (𝓞 K)) (span {x}) 0
Tactic: apply Ideal.finite_factors
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this :
  ∀ (w : FinitePlace K),
    Ne (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
⊢ Set.Finite.{u_1} (α := FinitePlace K) {x_1 : FinitePlace K | x_1.maximalIdeal.asIdeal ∣ span {x}}
have h : Set.Finite.{u_1} (α := HeightOneSpectrum (𝓞 K)) {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}
Tactic: have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by
    apply Ideal.finite_factors
    simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this :
  ∀ (w : FinitePlace K),
    Ne (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h : Set.Finite.{u_1} (α := HeightOneSpectrum (𝓞 K)) {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}
⊢ Set.Finite.{u_1} (α := FinitePlace K) {x_1 : FinitePlace K | x_1.maximalIdeal.asIdeal ∣ span {x}}
have h_inj : Set.InjOn.{u_1, u_1} (α := FinitePlace K) maximalIdeal {w : FinitePlace K | w.maximalIdeal.asIdeal ∣ span {x}}
Tactic: have h_inj : Set.InjOn FinitePlace.maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}} :=
    Function.Injective.injOn maximalIdeal_injective
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this :
  ∀ (w : FinitePlace K),
    Ne (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h : Set.Finite.{u_1} (α := HeightOneSpectrum (𝓞 K)) {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}
h_inj : Set.InjOn.{u_1, u_1} (α := FinitePlace K) maximalIdeal {w : FinitePlace K | w.maximalIdeal.asIdeal ∣ span {x}}
⊢ Set.Finite.{u_1} (α := FinitePlace K) {x_1 : FinitePlace K | x_1.maximalIdeal.asIdeal ∣ span {x}}
have refine : Subset.{u_1} (α := Set (HeightOneSpectrum (𝓞 K)))
  (Set.image (α := FinitePlace K) maximalIdeal {x_1 : FinitePlace K | x_1.maximalIdeal.asIdeal ∣ span {x}})
  {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}
Tactic: refine (h.subset ?_).of_finite_image h_inj
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h_x_nezero : x ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦ (w : (a : K) → ℝ) x
have rcases : ∀ (a b : 𝓞 K) (hb : Membership.mem (γ := Submonoid (𝓞 K)) (nonZeroDivisors (𝓞 K)) b)
  (h_x_nezero :
    HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
      0),
  Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    (w : (a : K) → ℝ)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))
Tactic: rcases IsFractionRing.div_surjective (𝓞 K) x with ⟨a, b, hb, rfl⟩
Cleared hypotheses: x, h_x_nezero
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
hb : Membership.mem (γ := Submonoid (𝓞 K)) (nonZeroDivisors (𝓞 K)) b
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    (w : (a : K) → ℝ)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))
have simp_all : ∀ (h_x_nezero : ¬a = 0 ∧ ¬b = 0),
  Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) : ℝ)
      ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) : ℝ)
Tactic: simp_all only [ne_eq, div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or, map_div₀]
Cleared hypotheses: h_x_nezero
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
hb : Membership.mem (γ := Submonoid (𝓞 K)) (nonZeroDivisors (𝓞 K)) b
h_x_nezero : ¬a = 0 ∧ ¬b = 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) : ℝ)
      ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) : ℝ)
have ha : ¬a = 0
Tactic: obtain ⟨ha, hb⟩ := h_x_nezero
Cleared hypotheses: h_x_nezero
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
hb : Membership.mem (γ := Submonoid (𝓞 K)) (nonZeroDivisors (𝓞 K)) b
h_x_nezero : ¬a = 0 ∧ ¬b = 0
ha : ¬a = 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) : ℝ)
      ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) : ℝ)
have hb₁ : ¬b = 0
Tactic: obtain ⟨ha, hb⟩ := h_x_nezero
Cleared hypotheses: h_x_nezero
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.FinitePlace (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
hb_1 : Membership.mem (γ := Submonoid (𝓞 K)) (nonZeroDivisors (𝓞 K)) b
ha : ¬a = 0
hb : ¬b = 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) : ℝ)
      ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) : ℝ)
have simp_rw : Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
  HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) ((w : (a : K) → ℝ) (↑b : K) : ℝ)
Tactic: simp_rw [← RingOfIntegers.coe_eq_algebraMap]