awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 ↥L) → 𝓞 K) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 K)
have rw : IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
  IsUnit.{u_2} (M := 𝓞 K)
    ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 ↥L) → 𝓞 F) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x)) : 𝓞 K)
Tactic: rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
rw :
  IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K)
      ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 ↥L) → 𝓞 F) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x)) : 𝓞 K)
⊢ IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 ↥L) → 𝓞 K) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 K)
have rw₁ : IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
  IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) (x ^ finrank F ↥L) : 𝓞 K)
Tactic: rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
rw :
  IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K)
      ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 ↥L) → 𝓞 F) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x)) : 𝓞 K)
rw₁ :
  IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) (x ^ finrank F ↥L) : 𝓞 K)
⊢ IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 ↥L) → 𝓞 K) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 K)
have rw₂ : IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
  IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L))
Tactic: rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) ↔ IsUnit x
have IsUnit : IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
  IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 ↥L) → 𝓞 K) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 K)
Tactic: calc
    IsUnit (norm K x) ↔ IsUnit ((norm K) x ^ finrank F L) :=
      (isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)).symm
    _ ↔ IsUnit (norm K (algebraMap (𝓞 F) (𝓞 L) x)) := by
      rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
    _ ↔ IsUnit (algebraMap (𝓞 F) (𝓞 L) x) := isUnit_norm_of_isGalois K
    _ ↔ IsUnit (norm F (algebraMap (𝓞 F) (𝓞 L) x)) := (isUnit_norm_of_isGalois F).symm
    _ ↔ IsUnit (x ^ finrank F L) := (congr_arg IsUnit (norm_algebraMap F _)).to_iff
    _ ↔ IsUnit x := isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ Eq (α := ℝ) (∏ᶠ (w : FinitePlace K), (w : (a : K) → ℝ) (↑x : K)) |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)|⁻¹
have simp : Eq (α := ℝ)
  (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
    Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
  |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)|⁻¹
Tactic: simp only [← finprod_comp_equiv equivHeightOneSpectrum.symm, equivHeightOneSpectrum_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ Eq (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
    |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)|⁻¹
have refine : HMul.hMul (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
    |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)| =
  1
Tactic: refine (inv_eq_of_mul_eq_one_left ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)| =
    1
have norm_cast : HMul.hMul (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
    (↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℝ) =
  1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      (↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℝ) =
    1
have h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
Tactic: have h_span_nezero : span {x} ≠ 0 := by simp [h_x_nezero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
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
⊢ HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      (↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℝ) =
    1
have rw : 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 [Int.abs_eq_natAbs, ← absNorm_span_singleton,
    ← finprod_heightOneSpectrum_factorization h_span_nezero, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (hypothesis)
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}
⊢ 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
have h_fin₀ : t₀.Finite
Tactic: have h_fin₀ : t₀.Finite := by simp only [← dvd_span_singleton, finite_factors h_span_nezero, t₀]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (hypothesis)
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}))) : ℝ)
⊢ 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
have h_fin₁ : t₁.Finite
Tactic: have h_fin₁ : t₁.Finite := h_fin₀.subset <| by simp [norm_eq_one_iff_notMem, t₁, t₀]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
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
have refine : t₂ ⊆ t₀
Tactic: refine h_fin₀.subset ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
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₂ ⊆ t₀
have 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}
Tactic: simp only [mulSupport_subset_iff, Set.mem_setOf_eq, t₂, t₀,
      maxPowDividing, ← dvd_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (hypothesis)
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
⊢ v.asIdeal ∣ span {x}
have 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
Tactic: simp only [map_pow, Nat.cast_pow, ← pow_zero (absNorm v.asIdeal : ℝ)] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
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}
have 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
Tactic: refine (Associates.count_ne_zero_iff_dvd h_span_nezero (irreducible v)).1 <| fun h ↦ hv ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
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}
have 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
Tactic: classical
    refine (Associates.count_ne_zero_iff_dvd h_span_nezero (irreducible v)).1 <| fun h ↦ hv ?_
    congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (hypothesis)
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
⊢ 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
have h_fin₂ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (hypothesis)
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
⊢ 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
have 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}))) : ℝ))
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) _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
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}))) : ℝ))
⊢ 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
have 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
Tactic: rw [h_prod, ← finprod_mul_distrib h_fin₁ h_fin₂]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h_x_nezero : x ≠ 0
⊢ Eq (α := ℝ) (∏ᶠ (w : FinitePlace K), (w : (a : K) → ℝ) x) (↑|(Algebra.norm ℚ : (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),
  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: 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.ProductFormula (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 :
  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))|⁻¹ :
      ℝ)
have hb₁ : b ≠ 0
Tactic: apply nonZeroDivisors.ne_zero at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (hypothesis)
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
⊢ 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))|⁻¹ :
      ℝ)
have ha : a ≠ 0
Tactic: have ha : a ≠ 0 := by
    rintro rfl
    simp at h_x_nezero