awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
⊢ t₂.Finite

Tactic:
h_fin₀.subset ?_

Premises used: Set.Finite.subset
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
refine : t₂ ⊆ t₀
⊢ t₂.Finite

Tactic:
refine h_fin₀.subset ?_

Premises used: Set.Finite.subset
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
simp :
  ∀ (x_1 : HeightOneSpectrum (𝓞 K)),
    Ne (α := ℝ)
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
              (x_1.asIdeal ^
                Associates.count (Associates.mk x_1.asIdeal) (Associates.factors (Associates.mk (span {x}))))) :
          ℝ)
        1 →
      x_1.asIdeal ∣ span {x}
⊢ t₂ ⊆ t₀

Tactic:
simp only [mulSupport_subset_iff, Set.mem_setOf_eq, t₂, t₀,
      maxPowDividing, ← dvd_span_singleton]

Premises used: Function.mulSupport_subset_iff, Set.mem_setOf_eq, IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Ideal.dvd_span_singleton
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
hv :
  Ne (α := ℝ)
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x}))))) :
      ℝ)
    1
⊢ HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ)
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) ≠
    HPow.hPow (α := ℝ) (β := ℕ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ) 0

Tactic:
simp only [map_pow, Nat.cast_pow, ← pow_zero (absNorm v.asIdeal : ℝ)] at hv

Premises used: Ideal.absNorm, IsDedekindDomain.HeightOneSpectrum.asIdeal, map_pow, Nat.cast, pow_zero, Nat.cast_pow, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
hv :
  HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ)
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) ≠
    HPow.hPow (α := ℝ) (β := ℕ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ) 0
⊢ v.asIdeal ∣ span {x}

Tactic:
(Associates.count_ne_zero_iff_dvd h_span_nezero (irreducible v)).1 <| fun h ↦ hv ?_

Premises used: Set.Mem, IsDedekindDomain.HeightOneSpectrum.irreducible, Iff.mp, Associates.count_ne_zero_iff_dvd
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
hv :
  HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ)
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) ≠
    HPow.hPow (α := ℝ) (β := ℕ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ) 0
refine :
  ∀ (h : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x}))) = 0),
    HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ)
        (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) =
      HPow.hPow (α := ℝ) (β := ℕ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ) 0
⊢ v.asIdeal ∣ span {x}

Tactic:
refine (Associates.count_ne_zero_iff_dvd h_span_nezero (irreducible v)).1 <| fun h ↦ hv ?_

Premises used: IsDedekindDomain.HeightOneSpectrum.irreducible, Iff.mp, Associates.count_ne_zero_iff_dvd
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
hv :
  HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ)
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) ≠
    HPow.hPow (α := ℝ) (β := ℕ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ) 0
h : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x}))) = 0
⊢ HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ)
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) =
    HPow.hPow (α := ℝ) (β := ℕ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ) 0

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
hv :
  HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ)
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) ≠
    HPow.hPow (α := ℝ) (β := ℕ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ) 0
refine :
  ∀ (h : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x}))) = 0),
    HPow.hPow (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ)
        (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (span {x})))) =
      HPow.hPow (α := ℝ) (β := ℕ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) v.asIdeal) : ℝ) 0
⊢ v.asIdeal ∣ span {x}

Tactic:
classical
    refine (Associates.count_ne_zero_iff_dvd h_span_nezero (irreducible v)).1 <| fun h ↦ hv ?_
    congr

Premises used: IsDedekindDomain.HeightOneSpectrum.irreducible, Iff.mp, Associates.count_ne_zero_iff_dvd
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
⊢ t₂.Finite

Tactic:
have h_fin₂ : t₂.Finite := by
    refine h_fin₀.subset ?_
    simp only [mulSupport_subset_iff, Set.mem_setOf_eq, t₂, t₀,
      maxPowDividing, ← dvd_span_singleton]
    intro v hv
    simp only [map_pow, Nat.cast_pow, ← pow_zero (absNorm v.asIdeal : ℝ)] at hv
    classical
    refine (Associates.count_ne_zero_iff_dvd h_span_nezero (irreducible v)).1 <| fun h ↦ hv ?_
    congr
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
⊢ ∀ (x : Ideal (𝓞 K)),
    Eq (α := ℝ)
        ((MonoidHom.comp (↑(Nat.castRingHom ℝ) : ℕ →* ℝ) (↑absNorm : Ideal (𝓞 K) →* ℕ) : (a : Ideal (𝓞 K)) → ℝ) x : ℝ)
        (1 : ℝ) →
      x = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
⊢ Eq (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) : ℝ)
    (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ))

Tactic:
have h_prod : (absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x})) : ℝ) =
      ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), (absNorm (v.maxPowDividing (span {x})) : ℝ) :=
    ((Nat.castRingHom ℝ).toMonoidHom.comp absNorm.toMonoidHom).map_finprod_of_preimage_one
      (by simp) _
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
h_prod :
  Eq (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) : ℝ)
    (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ))
rw :
  Eq (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i) *
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (i.maxPowDividing (span {x}))) : ℝ))
    1
⊢ HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) : ℝ) =
    1

Tactic:
rw [h_prod, ← finprod_mul_distrib h_fin₁ h_fin₂]

Premises used: finprod_mul_distrib
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
h_prod :
  Eq (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) : ℝ)
    (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ))
⊢ Eq (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i) *
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (i.maxPowDividing (span {x}))) : ℝ))
    1

Tactic:
finprod_eq_one_of_forall_eq_one fun v ↦ embedding_mul_absNorm _ v h_x_nezero

Premises used: NumberField.HeightOneSpectrum.embedding_mul_absNorm, finprod_eq_one_of_forall_eq_one
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
h_prod :
  Eq (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) : ℝ)
    (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ))
⊢ Eq (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i) *
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (i.maxPowDividing (span {x}))) : ℝ))
    1

Tactic:
exact finprod_eq_one_of_forall_eq_one fun v ↦ embedding_mul_absNorm _ v h_x_nezero

Premises used: NumberField.HeightOneSpectrum.embedding_mul_absNorm, finprod_eq_one_of_forall_eq_one
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
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),
    Eq (α := ℝ)
      (∏ᶠ (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)))
      (↑|(Algebra.norm ℚ : (a : K) → ℚ)
                (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))|⁻¹ :
        ℝ)
⊢ Eq (α := ℝ) (∏ᶠ (w : FinitePlace K), (w : (a : K) → ℝ) x) (↑|(Algebra.norm ℚ : (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.ProductFormula
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
⊢ b ≠ 0

Tactic:
apply nonZeroDivisors.ne_zero at hb

Premises used: nonZeroDivisors.ne_zero
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : 𝓞 K
hb : b ≠ 0
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
⊢ False

Tactic:
simp at h_x_nezero
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
⊢ a ≠ 0

Tactic:
have ha : a ≠ 0 := by
    rintro rfl
    simp at h_x_nezero
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
simp_rw :
  HDiv.hDiv (α := ℝ) |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ)|⁻¹ |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ)|⁻¹ =
    |(↑((Algebra.norm ℚ : (a : K) → ℚ)
              (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
          ℝ)|⁻¹
⊢ Eq (α := ℝ)
    (∏ᶠ (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)))
    (↑|(Algebra.norm ℚ : (a : K) → ℚ)
              (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))|⁻¹ :
      ℝ)

Tactic:
simp_rw [map_div₀, Rat.cast_inv, Rat.cast_abs,
    finprod_div_distrib (hasFiniteMulSupport_int ha) (hasFiniteMulSupport_int hb),
    prod_eq_inv_abs_norm_int ha, prod_eq_inv_abs_norm_int hb]

Premises used: NumberField.FinitePlace.hasFiniteMulSupport_int, NumberField.FinitePlace.prod_eq_inv_abs_norm_int, Rat.cast_inv, map_div₀, Rat.cast_abs, finprod_div_distrib
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
rw :
  |HDiv.hDiv (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ)| =
    |(↑((Algebra.norm ℚ : (a : K) → ℚ)
            (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
        ℝ)|
⊢ HDiv.hDiv (α := ℝ) |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ)|⁻¹ |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ)|⁻¹ =
    |(↑((Algebra.norm ℚ : (a : K) → ℚ)
              (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
          ℝ)|⁻¹

Tactic:
rw [← inv_eq_iff_eq_inv, inv_inv_div_inv, ← abs_div]

Premises used: inv_inv_div_inv, abs_div, inv_eq_iff_eq_inv
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
e_a :
  HDiv.hDiv (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) =
    (↑((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
      ℝ)
⊢ |HDiv.hDiv (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ)| =
    |(↑((Algebra.norm ℚ : (a : K) → ℚ)
            (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
        ℝ)|

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
⊢ Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0

Tactic:
simp [hb]
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
⊢ Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0

Tactic:
have hb₀ : ((Algebra.norm ℤ) b : ℝ) ≠ 0 := by simp [hb]