awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 y : K
⊢ LE.le (α := ℝ) ((adicAbv K v : (a : K) → ℝ) (x + y) : ℝ)
    (max ((adicAbv K v : (a : K) → ℝ) x) ((adicAbv K v : (a : K) → ℝ) y) : ℝ)

Tactic:
isNonarchimedean_adicAbv K v x y

Premises used: NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv
-- 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
n : ℕ
⊢ LE.le (α := ℝ) ((adicAbv K v : (a : K) → ℝ) (↑n : K) : ℝ) (1 : ℝ)

Tactic:
(isNonarchimedean_adicAbv K v).apply_natCast_le_one

Premises used: NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv, IsNonarchimedean.apply_natCast_le_one
-- 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
n : ℤ
⊢ LE.le (α := ℝ) ((adicAbv K v : (a : K) → ℝ) (↑n : K) : ℝ) (1 : ℝ)

Tactic:
(isNonarchimedean_adicAbv K v).apply_intCast_le_one

Premises used: NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv, IsNonarchimedean.apply_intCast_le_one
-- 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 : adicCompletion K v
⊢ ‖x‖ =
    (↑((toNNReal (e := (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0)) ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            x)) :
      ℝ)

Tactic:
simp [Valued.toNormedField.norm_def, Valuation.RankOne.hom, HeightOneSpectrum.rankOne_hom'_def,
    valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective
      (valuedAdicCompletion_surjective K v)]

Premises used: Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, NumberField.HeightOneSpectrum.rankOne_hom'_def, Valuation.RankOne.hom, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Valued.toNormedField.norm_def
-- 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
⊢ norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) x : adicCompletion K v) =
    (HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) x

Tactic:
simp [norm_def, embedding_apply, adicAbv_def]

Premises used: NumberField.FinitePlace.embedding_apply, NumberField.HeightOneSpectrum.adicAbv_def, NumberField.FinitePlace.norm_def
-- 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
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)) :
      ℝ)
rw₁ rw₂ :
  (↑((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)) :
      ℝ) =
    (↑((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)) :
      ℝ)

Tactic:
rw [norm_embedding, adicAbv_def]

Premises used: NumberField.FinitePlace.norm_embedding, NumberField.HeightOneSpectrum.adicAbv_def
-- 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 : 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) =
    (↑((toNNReal (e := (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ≥0)) ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x)) :
      ℝ)

Tactic:
simp [norm_embedding, adicAbv_def, valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, NumberField.FinitePlace.norm_embedding, NumberField.HeightOneSpectrum.adicAbv_def
-- 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 : R
rw : LE.le (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ)
⊢ 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

Tactic:
rw [norm_embedding]

Premises used: NumberField.FinitePlace.norm_embedding
-- 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 : R
⊢ LE.le (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ)

Tactic:
v.adicAbv_coe_le_one (one_lt_absNorm_nnreal v) x

Premises used: IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one, 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 : R
⊢ LE.le (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ)

Tactic:
exact v.adicAbv_coe_le_one (one_lt_absNorm_nnreal v) x

Premises used: IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one, 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 : R
rw :
  Eq (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ) ↔
    x ∉ v.asIdeal
⊢ 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

Tactic:
rw [norm_embedding]

Premises used: NumberField.FinitePlace.norm_embedding
-- 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 : R
⊢ Eq (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ) ↔
    x ∉ v.asIdeal

Tactic:
v.adicAbv_coe_eq_one_iff (one_lt_absNorm_nnreal v) x

Premises used: NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff
-- 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 : R
⊢ Eq (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ) ↔
    x ∉ v.asIdeal

Tactic:
exact v.adicAbv_coe_eq_one_iff (one_lt_absNorm_nnreal v) x

Premises used: NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff
-- 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 : R
rw :
  LT.lt (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ) ↔
    x ∈ v.asIdeal
⊢ 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

Tactic:
rw [norm_embedding]

Premises used: NumberField.FinitePlace.norm_embedding
-- 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 : R
⊢ LT.lt (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ) ↔
    x ∈ v.asIdeal

Tactic:
v.adicAbv_coe_lt_one_iff (one_lt_absNorm_nnreal v) x

Premises used: NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff
-- 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 : R
⊢ LT.lt (α := ℝ) ((HeightOneSpectrum.adicAbv K v : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) x : K) : ℝ) (1 : ℝ) ↔
    x ∈ v.asIdeal

Tactic:
exact v.adicAbv_coe_lt_one_iff (one_lt_absNorm_nnreal v) x

Premises used: NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff
-- 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 : R
h_x_nezero : x ≠ 0
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))
                  ⋯) :
              ℤ)) :
        ℝ) *
      HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal R) → ℕ) v.asIdeal) : ℝ)
        (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) =
    1
⊢ 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

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))]

Premises used: Iff.mpr, NumberField.FinitePlace.norm_embedding, NumberField.HeightOneSpectrum.adicAbv_def, WithZeroMulInt.toNNReal_neg_apply, Iff.not, map_pow, Valuation.ne_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuation, Nat.cast_pow, IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FaithfulSMul.algebraMap_eq_zero_iff
-- 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 : R
h_x_nezero : x ≠ 0
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))
              ⋯) :
          ℤ)
        ((↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) : ℤ) : ℤ)) =
    1
⊢ 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

Tactic:
rw [← zpow_natCast, ← zpow_add₀ <| mod_cast (zero_lt_one.trans (one_lt_absNorm_nnreal v)).ne']

Premises used: zpow_natCast, LT.lt.ne', zero_lt_one, zpow_add₀, LT.lt.trans, 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 : R
h_x_nezero : x ≠ 0
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))
            ⋯) :
        ℤ)
      ((↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {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

Tactic:
rw [zpow_eq_one_iff_right₀ (Nat.cast_nonneg' _) (mod_cast (one_lt_absNorm_nnreal v).ne')]

Premises used: zpow_eq_one_iff_right₀
-- 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 : R
h_x_nezero : x ≠ 0
⊢ 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})))) : ℤ) : ℤ) =
    0

Tactic:
simp [valuation_of_algebraMap, intValuation_if_neg, h_x_nezero]

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
⊢ IsFinitePlace (↑v : AbsoluteValue K ℝ)

Tactic:
simp [IsFinitePlace, v.prop]

Premises used: NumberField.IsFinitePlace, Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : AbsoluteValue K ℝ
⊢ IsFinitePlace v ↔ ∃ (w : FinitePlace K), (↑w : AbsoluteValue K ℝ) = v

Tactic:
⟨fun H ↦ ⟨⟨v, H⟩, rfl⟩, fun ⟨w, hw⟩ ↦ hw ▸ w.isFinitePlace⟩

Premises used: NumberField.IsFinitePlace, Eq.rec, Subtype.mk, _private.0.NumberField.isFinitePlace_iff.match_1, Iff.intro, Exists.intro, NumberField.FinitePlace.isFinitePlace, rfl
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : K
⊢ (mk v : (a : K) → ℝ) x =
    norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) x : adicCompletion K v)

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', Valuation.norm, SeparationQuotient.mk, NNReal.toReal, rfl
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x : K
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) x : ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: 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_1 : HeightOneSpectrum R
inst_5 : NumberField K
v : FinitePlace K
x y : K
⊢ (v : (a : K) → ℝ) (x + y) ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((v : (a : K) → ℝ) x : ℝ) ((v : (a : K) → ℝ) y : ℝ)

Tactic:
simpa [coe_apply] using IsAbsoluteValue.abv_add' x y

Premises used: IsAbsoluteValue.abv_add', NumberField.FinitePlace.coe_apply
-- 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_1 : HeightOneSpectrum R
inst_5 : NumberField K
v : FinitePlace K
x : K
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) (-x) : ℝ) ((v : (a : K) → ℝ) x : ℝ)

Tactic:
simp [coe_apply]

Premises used: NumberField.FinitePlace.coe_apply
-- 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_1 : HeightOneSpectrum R
inst_5 : NumberField K
v : FinitePlace K
⊢ ∀ {a : K}, Eq (α := ℝ) ((v : (a : K) → ℝ) a : ℝ) (0 : ℝ) → a = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : FinitePlace K
⊢ mk w.maximalIdeal = w

Tactic:
Subtype.ext w.2.choose_spec

Premises used: Exists.choose_spec, Subtype.property, Subtype.ext, NumberField.FinitePlace
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : FinitePlace K
x : K
rw :
  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:
rw [← mk_maximalIdeal w, mk_apply]

Premises used: NumberField.FinitePlace.mk_apply, NumberField.FinitePlace.mk_maximalIdeal
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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
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)
⊢ 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]

Premises used: NumberField.FinitePlace.mk_apply, NumberField.FinitePlace.mk_maximalIdeal
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : FinitePlace K
x : K
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) x : ℝ) ↔ x ≠ 0

Tactic:
w.1.pos_iff

Premises used: AbsoluteValue.pos_iff, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
a : v₁ = v₂
rw rw₁ : Eq (α := FinitePlace K) (mk v₂) (mk v₂)
⊢ Eq (α := FinitePlace K) (mk v₁) (mk v₂)

Tactic:
rw [a]
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
refine : Eq (α := FinitePlace K) (mk v₁) (mk v₂) → v₁ = v₂
⊢ Eq (α := FinitePlace K) (mk v₁) (mk v₂) ↔ v₁ = v₂

Tactic:
refine ⟨?_, fun a ↦ by rw [a]⟩
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
contrapose! : v₁ ≠ v₂ → Ne (α := FinitePlace K) (mk v₁) (mk v₂)
⊢ Eq (α := FinitePlace K) (mk v₁) (mk v₂) → v₁ = v₂

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
rw : ∃ (a : K), Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) a : ℝ) ((mk v₂ : (a : K) → ℝ) a : ℝ)
⊢ Ne (α := FinitePlace K) (mk v₁) (mk v₂)

Tactic:
rw [DFunLike.ne_iff]

Premises used: DFunLike.ne_iff
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
by_contra! : ∀ (H : ∀ (x : 𝓞 K) (_ : x ∈ v₁.asIdeal), x ∈ v₂.asIdeal), False
⊢ ∃ x ∈ v₁.asIdeal, x ∉ v₂.asIdeal

Tactic:
by_contra! H
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
H : ∀ (x : 𝓞 K) (_ : x ∈ v₁.asIdeal), x ∈ v₂.asIdeal
⊢ False

Tactic:
h <| HeightOneSpectrum.ext_iff.mpr <| IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H

Premises used: Iff.mpr, IsDedekindDomain.HeightOneSpectrum.isMaximal, IsDedekindDomain.HeightOneSpectrum.ext_iff, Ideal.IsMaximal.eq_of_le, Ideal.IsPrime.ne_top'