awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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'
-- 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₂
have :
  ∀ (x : 𝓞 K) (hx1 : x ∈ v₁.asIdeal) (hx2 : x ∉ v₂.asIdeal),
    ∃ (a : K), Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) a : ℝ) ((mk v₂ : (a : K) → ℝ) a : ℝ)
⊢ ∃ (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
-- 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₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
h₁ : Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) (↑x : K) : ℝ) ((mk v₂ : (a : K) → ℝ) (↑x : K) : ℝ)
⊢ ∃ (a : K), Ne (α := ℝ) ((mk v₁ : (a : K) → ℝ) a : ℝ) ((mk v₂ : (a : K) → ℝ) a : ℝ)

Tactic:
use x
-- 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₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ 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

Premises used: NumberField.FinitePlace.norm_lt_one_iff_mem
-- 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₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
hx1₁ :
  norm (E := adicCompletion K v₁)
      ((embedding v₁ : (a : K) → adicCompletion K v₁) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : adicCompletion K v₁) <
    1
⊢ x ∉ v₂.asIdeal

Tactic:
rw [← norm_lt_one_iff_mem K] at hx1

Premises used: NumberField.FinitePlace.norm_lt_one_iff_mem
-- 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₂
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₂) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x) : adicCompletion K v₂) =
    1

Tactic:
rw [← norm_eq_one_iff_notMem K] at hx2

Premises used: NumberField.FinitePlace.norm_eq_one_iff_notMem
-- 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₂
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
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
⊢ 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₂)

Tactic:
linarith
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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)
rw₁ rw₂ : Eq (α := FinitePlace K) (mk v) (mk v)
⊢ maximalIdeal (mk v) = v

Tactic:
rw [← mk_eq_iff, mk_maximalIdeal]

Premises used: NumberField.FinitePlace.mk_maximalIdeal, NumberField.FinitePlace.mk_eq_iff
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Function.Injective (β := HeightOneSpectrum (𝓞 K)) fun (w : FinitePlace K) ↦ w.maximalIdeal

Tactic:
equivHeightOneSpectrum.injective

Premises used: NumberField.FinitePlace.maximalIdeal, NumberField.FinitePlace.equivHeightOneSpectrum, Classical.choose, Equiv.injective
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ w₂ : FinitePlace K
⊢ w₁.maximalIdeal = w₂.maximalIdeal ↔ w₁ = w₂

Tactic:
equivHeightOneSpectrum.injective.eq_iff

Premises used: Function.Injective.eq_iff, NumberField.FinitePlace.maximalIdeal, NumberField.FinitePlace.equivHeightOneSpectrum, Classical.choose, Equiv.injective
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ ∀ (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
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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 : ℝ)
simp_rw : Set.Finite.{u_1} (α := FinitePlace K) {x_1 : FinitePlace K | x_1.maximalIdeal.asIdeal ∣ span {x}}
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦ (w : (a : K) → ℝ) (↑x : K)

Tactic:
simp_rw [Function.HasFiniteMulSupport, Function.mulSupport, this, ← norm_embedding_eq,
    norm_lt_one_iff_mem, ← Ideal.dvd_span_singleton]

Premises used: NumberField.FinitePlace.norm_embedding_eq, NumberField.FinitePlace.norm_lt_one_iff_mem, Function.mulSupport, Function.HasFiniteMulSupport, Ideal.dvd_span_singleton
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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 : ℝ)
hI : Ne (α := Ideal (𝓞 K)) (span {x}) 0
⊢ Set.Finite.{u_1} (α := HeightOneSpectrum (𝓞 K)) {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}

Tactic:
apply Ideal.finite_factors

Premises used: Ideal.finite_factors
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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 : ℝ)
⊢ Ne (α := Ideal (𝓞 K)) (span {x}) 0

Tactic:
simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true]

Premises used: Ideal.span_singleton_eq_bot, ne_eq, Submodule.zero_eq_bot, not_false_eq_true
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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}}

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]
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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.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
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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}}

Tactic:
(h.subset ?_).of_finite_image h_inj

Premises used: Set.Finite.subset, Set.Finite.of_finite_image
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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}}
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}}
⊢ Set.Finite.{u_1} (α := FinitePlace K) {x_1 : FinitePlace K | x_1.maximalIdeal.asIdeal ∣ span {x}}

Tactic:
refine (h.subset ?_).of_finite_image h_inj

Premises used: Set.Finite.subset, Set.Finite.of_finite_image
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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}}
⊢ 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:
simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_setOf_eq, subset_refl]

Premises used: subset_refl, Set.preimage_setOf_eq, Set.image_subset_iff, Ideal.dvd_span_singleton
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h_x_nezero : x ≠ 0
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))
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦ (w : (a : K) → ℝ) x

Tactic:
rcases IsFractionRing.div_surjective (𝓞 K) x with ⟨a, b, hb, rfl⟩

Premises used: IsFractionRing.div_surjective, NumberField.RingOfIntegers, rfl
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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
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) : ℝ)
⊢ 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:
simp_all only [ne_eq, div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or, map_div₀]

Premises used: ne_eq, not_or, map_div₀, div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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
⊢ ¬a = 0

Tactic:
obtain ⟨ha, hb⟩ := h_x_nezero
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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
⊢ ¬b = 0

Tactic:
obtain ⟨ha, hb⟩ := h_x_nezero
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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
simp_rw :
  Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) ((w : (a : K) → ℝ) (↑b : K) : ℝ)
⊢ 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_rw [← RingOfIntegers.coe_eq_algebraMap]

Premises used: NumberField.RingOfIntegers.coe_eq_algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
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
funProp : a ≠ 0
funProp₁ : b ≠ 0
⊢ Function.HasFiniteMulSupport (M := ℝ) fun (w : FinitePlace K) ↦
    HDiv.hDiv (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) ((w : (a : K) → ℝ) (↑b : K) : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_3
inst_2 : CommMonoid M
I : Ideal (𝓞 K)
hI : I ≠ ⊥
f : Ideal (𝓞 K) → M
⊢ Function.HasFiniteMulSupport.{u_1, u_3} (M := M) fun (v : FinitePlace K) ↦
    f v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I

Tactic:
UniqueFactorizationMonoid.hasFiniteMulSupport_fun_pow_multiplicity _
    (asIdeal_injective.comp maximalIdeal_injective) (fun v ↦ v.maximalIdeal.irreducible) hI

Premises used: UniqueFactorizationMonoid.hasFiniteMulSupport_fun_pow_multiplicity, IsDedekindDomain.HeightOneSpectrum.irreducible, NumberField.FinitePlace.maximalIdeal_injective, NumberField.FinitePlace.maximalIdeal, Function.Injective.comp, IsDedekindDomain.HeightOneSpectrum.asIdeal_injective
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x y : K
obtain :
  ∀ (w : HeightOneSpectrum (𝓞 K)) (hw : place (A := adicCompletion K w) (embedding w) = (↑v : AbsoluteValue K ℝ)),
    LE.le (α := ℝ) ((v : (a : K) → ℝ) (x + y) : ℝ) (max ((v : (a : K) → ℝ) x) ((v : (a : K) → ℝ) y) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x + y) : ℝ) (max ((v : (a : K) → ℝ) x) ((v : (a : K) → ℝ) y) : ℝ)

Tactic:
obtain ⟨w, hw⟩ := v.prop

Premises used: Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x_1 y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (A := adicCompletion K w) (embedding w) = (↑v : AbsoluteValue K ℝ)
x : K
⊢ Eq (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x : ℝ) ((HeightOneSpectrum.adicAbv K w : (a : K) → ℝ) x : ℝ)

Tactic:
grind only [place_apply, norm_embedding]

Premises used: NumberField.FinitePlace.norm_embedding, NumberField.place_apply
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (A := adicCompletion K w) (embedding w) = (↑v : AbsoluteValue K ℝ)
⊢ ∀ (x : K), Eq (α := ℝ) ((v : (a : K) → ℝ) x : ℝ) ((HeightOneSpectrum.adicAbv K w : (a : K) → ℝ) x : ℝ)

Tactic:
have H x : v x = NumberField.HeightOneSpectrum.adicAbv K w x := by
    rw [show v x = v.val x from rfl]
    grind only [place_apply, norm_embedding]
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (A := adicCompletion K w) (embedding w) = (↑v : AbsoluteValue K ℝ)
H : ∀ (x : K), Eq (α := ℝ) ((v : (a : K) → ℝ) x : ℝ) ((HeightOneSpectrum.adicAbv K w : (a : K) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (x + y) : ℝ) (max ((v : (a : K) → ℝ) x) ((v : (a : K) → ℝ) y) : ℝ)

Tactic:
simpa only [H] using adicAbv_add_le_max K w x y

Premises used: NumberField.HeightOneSpectrum.adicAbv_add_le_max
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : K
⊢ (((Equiv.symm equivHeightOneSpectrum : (a : HeightOneSpectrum (𝓞 K)) → FinitePlace K) v : FinitePlace K) :
        (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
I : Ideal (𝓞 K)
hI : I ≠ ⊥
rw : ∏ᶠ (p : HeightOneSpectrum (𝓞 K)), p.asIdeal ^ multiplicity p.asIdeal I
| I

Tactic:
rw [← finprod_heightOneSpectrum_pow_multiplicity hI]

Premises used: Ideal.finprod_heightOneSpectrum_pow_multiplicity
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
conv_rhs :
  Eq.{u_1 + 1} (α := Ideal (𝓞 K))
    (∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I)
    (∏ᶠ (p : HeightOneSpectrum (𝓞 K)), p.asIdeal ^ multiplicity p.asIdeal I)
⊢ ∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I = I

Tactic:
conv_rhs => rw [← finprod_heightOneSpectrum_pow_multiplicity hI]

Premises used: Ideal.finprod_heightOneSpectrum_pow_multiplicity
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
⊢ Eq.{u_1 + 1} (α := Ideal (𝓞 K))
    (∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I)
    (∏ᶠ (p : HeightOneSpectrum (𝓞 K)), p.asIdeal ^ multiplicity p.asIdeal I)

Tactic:
simp only [← finprod_comp_equiv (equivHeightOneSpectrum (K := K)), equivHeightOneSpectrum_apply]

Premises used: NumberField.FinitePlace.equivHeightOneSpectrum_apply, NumberField.FinitePlace.equivHeightOneSpectrum, finprod_comp_equiv
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
⊢ Ne (α := Ideal (𝓞 K)) (span {x}) ⊥

Tactic:
have hnz : span {x} ≠ ⊥ := mt Submodule.span_singleton_eq_bot.mp hx
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : Ne (α := Ideal (𝓞 K)) (span {x}) ⊥
rw :
  norm (E := adicCompletion K v.maximalIdeal)
        ((embedding v.maximalIdeal : (a : K) → adicCompletion K v.maximalIdeal) (↑x : K) :
          adicCompletion K v.maximalIdeal) *
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maximalIdeal.maxPowDividing (span {x}))) : ℝ) =
    1
⊢ HMul.hMul (α := ℝ) ((v : (a : K) → ℝ) (↑x : K) : ℝ)
      (HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.maximalIdeal.asIdeal) : ℝ)
        (multiplicity v.maximalIdeal.asIdeal (span {x}))) =
    1

Tactic:
rw [← norm_embedding_eq v x, ← Nat.cast_pow, ← map_pow, ← maxPowDividing_eq_pow_multiplicity hnz]

Premises used: NumberField.FinitePlace.norm_embedding_eq, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiplicity, NumberField.RingOfIntegers.val, map_pow, Nat.cast_pow
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : Ne (α := Ideal (𝓞 K)) (span {x}) ⊥
⊢ norm (E := adicCompletion K v.maximalIdeal)
        ((embedding v.maximalIdeal : (a : K) → adicCompletion K v.maximalIdeal) (↑x : K) :
          adicCompletion K v.maximalIdeal) *
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maximalIdeal.maxPowDividing (span {x}))) : ℝ) =
    1

Tactic:
HeightOneSpectrum.embedding_mul_absNorm K v.maximalIdeal hx

Premises used: NumberField.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.maximalIdeal
-- Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : Ne (α := Ideal (𝓞 K)) (span {x}) ⊥
⊢ norm (E := adicCompletion K v.maximalIdeal)
        ((embedding v.maximalIdeal : (a : K) → adicCompletion K v.maximalIdeal) (↑x : K) :
          adicCompletion K v.maximalIdeal) *
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maximalIdeal.maxPowDividing (span {x}))) : ℝ) =
    1

Tactic:
exact HeightOneSpectrum.embedding_mul_absNorm K v.maximalIdeal hx

Premises used: NumberField.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.maximalIdeal