From 873b88795c7fe2bfadad964c353167ff6b8bf996 Mon Sep 17 00:00:00 2001
From: tb65536 <thomas.l.browning@gmail.com>
Date: Fri, 10 Jul 2026 18:37:32 +0100
Subject: [PATCH 1/8] almost sorry free

---
 Mathlib/NumberTheory/Height/NumberField.lean | 209 +++++++++++++++++++
 1 file changed, 209 insertions(+)

diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean
index 852c8132ed30e9..ac1abd2b636428 100644
--- a/Mathlib/NumberTheory/Height/NumberField.lean
+++ b/Mathlib/NumberTheory/Height/NumberField.lean
@@ -8,6 +8,8 @@ module
 public import Mathlib.NumberTheory.Height.Basic
 public import Mathlib.NumberTheory.Height.Northcott
 public import Mathlib.NumberTheory.NumberField.ProductFormula
+public import Mathlib.NumberTheory.NumberField.Completion.Ramification
+public import Mathlib.NumberTheory.RamificationInertia.Valuation
 
 import Mathlib.Algebra.FiniteSupport.Basic
 import Mathlib.Algebra.Order.Hom.Lattice
@@ -128,6 +130,213 @@ lemma mulHeight_eq {ι : Type*} {x : ι → K} (hx : x ≠ 0) :
   simp only [FinitePlace.coe_apply, InfinitePlace.coe_apply, Height.mulHeight_eq hx,
     prod_archAbsVal_eq, prod_nonarchAbsVal_eq fun v ↦ ⨆ i, v (x i)]
 
+section extension
+
+variable (L : Type*) [Field L] [NumberField L] [Algebra K L]
+
+attribute [mk_iff] AbsoluteValue.LiesOver
+
+theorem _root_.NumberField.InfinitePlace.liesOver_iff_comap_eq {K L : Type*} [Field K] [Field L]
+    [NumberField K] [NumberField L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} :
+    w.1.LiesOver v.1 ↔ w.comap (algebraMap K L) = v := by
+  rw [AbsoluteValue.liesOver_iff, AbsoluteValue.ext_iff, InfinitePlace.ext_iff]
+  rfl
+
+@[to_additive]
+theorem finprod_fiberwise {ι κ M : Type*} [CommMonoid M]
+    (s : Set ι) (g : ι → κ) (f : ι → M) (hf : f.HasFiniteMulSupport) :
+    ∏ᶠ j, ∏ᶠ i ∈ {i ∈ s | g i = j}, f i = ∏ᶠ i ∈ s, f i := by
+  classical
+  let t := hf.toFinset
+  have : ∀ i, f i ≠ 1 → i ∈ t := by simp [t]
+  have : ∀ i ∈ (hf.toFinset.filter (· ∈ s)), g i ∈ t.image g := by grind
+  rw [finprod_mem_eq_prod_filter f s hf, ← Finset.prod_fiberwise_of_maps_to this,
+    finprod_eq_prod_of_mulSupport_subset]
+  · apply Finset.prod_congr rfl
+    intro k hk
+    apply finprod_mem_eq_prod_of_subset
+    · grind [Function.mem_mulSupport]
+    · grind
+  · rw [Function.mulSupport_subset_iff]
+    intro x
+    contrapose!
+    intro h
+    apply finprod_mem_eq_one_of_forall_eq_one
+    grind
+
+@[to_additive]
+theorem finprod_fiberwise_univ {ι κ M : Type*} [CommMonoid M]
+    (g : ι → κ) (f : ι → M) (hf : f.HasFiniteMulSupport) :
+    ∏ᶠ j, ∏ᶠ i ∈ {i | g i = j}, f i = ∏ᶠ i, f i := by
+  simpa using finprod_fiberwise Set.univ g f hf
+
+theorem finprod_mem_pow_eq_pow_finsum {ι M : Type*} [CommMonoid M] (s : Set ι) (f : ι → ℕ)
+    (hf : (s ∩ f.support).Finite) (a : M) :
+    ∏ᶠ i ∈ s, a ^ f i = a ^ ∑ᶠ i ∈ s, f i := by
+  classical
+  rw [finprod_mem_eq_prod_of_subset (t := hf.toFinset.filter (· ∈ s)), Finset.prod_pow_eq_pow_sum,
+    finsum_mem_eq_sum_of_subset (t := hf.toFinset.filter (· ∈ s))]
+  · simp [Function.support]
+    grind
+  · simp
+    grind
+  · simp [Function.mulSupport]
+    intro x ⟨hx1, hx2⟩
+    refine ⟨?_, hx1⟩
+    contrapose! hx2
+    simp [hx2]
+    rw [hx2 hx1, pow_zero]
+  · simp
+    grind
+
+open IsDedekindDomain in
+theorem foo {f : Ideal (𝓞 L) → ℝ} (v : HeightOneSpectrum (𝓞 K)) :
+    ∏ᶠ (w : HeightOneSpectrum (𝓞 L)) (_ : w.under (𝓞 K) = v), f w.1 =
+      ∏ w ∈ IsDedekindDomain.primesOverFinset v.1 (𝓞 L), f w := by
+  sorry
+
+open scoped NumberField.LiesOver
+
+theorem mult_mul_finrank (v : InfinitePlace K) (w : InfinitePlace L) [hh : w.1.LiesOver v.1] :
+    v.mult * Module.finrank v.Completion w.Completion = w.mult := by
+  have : v = w.comap (algebraMap K L) := by
+    have h1 := hh.comp_eq.symm
+    rw [InfinitePlace.ext_iff]
+    rwa [AbsoluteValue.ext_iff] at h1
+  by_cases h : w.IsUnramified K
+  · rw [NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified v h, mul_one]
+    convert NumberField.InfinitePlace.IsUnramified.eq h
+  · rw [NumberField.InfinitePlace.Completion.finrank_eq_two_of_isRamified v h]
+    have := InfinitePlace.isRamified_iff.mp h
+    rw [InfinitePlace.mult, if_pos, InfinitePlace.mult, if_neg, one_mul]
+    simpa using this.1
+    convert this.2
+
+open IsDedekindDomain in
+theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
+    (x : ι → K) (hx : ∀ i, x i ≠ 0) : -- is nonempty required?
+    mulHeight x ^ Module.finrank K L = mulHeight (algebraMap K L ∘ x) := by
+  classical
+  by_cases hx' : x = 0
+  · simp [hx']
+  rw [mulHeight_eq hx', mulHeight_eq (by simpa [funext_iff] using hx'), mul_pow]
+  simp only [Function.comp_apply]
+  congr
+  · rw [← Finset.prod_pow]
+    let g : InfinitePlace L → InfinitePlace K := fun v ↦ v.comap (algebraMap K L)
+    rw [← Finset.univ.prod_fiberwise g]
+    apply Finset.prod_congr rfl fun v _ ↦ ?_
+    simp_rw [← InfinitePlace.comap_apply]
+    have key : ∏ w with g w = v, (⨆ i, w.comap (algebraMap K L) (x i)) ^ w.mult =
+        ∏ w with g w = v, (⨆ i, v (x i)) ^ w.mult := by
+      apply Finset.prod_congr rfl fun w hw ↦ ?_
+      rw [Finset.mem_filter_univ, ← InfinitePlace.liesOver_iff_comap_eq] at hw
+      rw [NumberField.InfinitePlace.LiesOver.comap_eq w v]
+    rw [key, Finset.prod_pow_eq_pow_sum, ← pow_mul]
+    congr
+    rw [← v.sum_inertiaDeg_eq_finrank K L, Finset.mul_sum]
+    have : (InfinitePlace.placesOver L v).toFinset =
+        ({w | g w = v} : Finset (InfinitePlace L)) := by
+      ext w
+      simp [InfinitePlace.placesOver, g, InfinitePlace.liesOver_iff_comap_eq]
+    apply Finset.sum_congr this
+    intro w hw
+    rw [Finset.mem_filter_univ, ← InfinitePlace.liesOver_iff_comap_eq] at hw
+    rw [InfinitePlace.inertiaDeg_eq_finrank]
+    apply mult_mul_finrank
+  · simp_rw [← finprod_comp_equiv NumberField.FinitePlace.equivHeightOneSpectrum.symm]
+    let g : HeightOneSpectrum (𝓞 L) → HeightOneSpectrum (𝓞 K) := fun v ↦ v.under (𝓞 K)
+    rw [← finprod_fiberwise_univ g, finprod_pow]
+    · apply finprod_congr
+      intro v
+      simp_rw [NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply]
+      have key : ∀ (w : HeightOneSpectrum (𝓞 L)) (hw : w ∈ ({w | g w = v})) (i : ι),
+        ‖FinitePlace.embedding w (algebraMap K L (x i))‖ = ‖FinitePlace.embedding v (x i)‖ ^
+          (w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
+        intro w hw i
+        rw [← hw]
+        simp_rw [FinitePlace.norm_embedding, HeightOneSpectrum.adicAbv_def]
+        have : w.1.LiesOver v.1 := by
+          rw [Set.mem_setOf_eq, HeightOneSpectrum.ext_iff] at hw
+          exact ⟨hw.symm⟩
+        rw [hw, ← IsDedekindDomain.HeightOneSpectrum.valuation_liesOver L v w (x i),
+          map_pow, Ideal.ramificationIdx'_eq_ramificationIdx v.1 w.1 v.ne_bot]
+        simp [WithZeroMulInt.toNNReal, MonoidWithZeroHom.coe_mk]
+        split_ifs
+        · simp
+          symm
+          rw [zero_pow, zero_pow]
+          exact (w.asIdeal.ramificationIdx_pos (𝓞 K)).ne'
+          exact (mul_pos (w.asIdeal.ramificationIdx_pos (𝓞 K))
+            (w.asIdeal.inertiaDeg_pos (𝓞 K))).ne'
+        · rw [← Ideal.absNorm_pow_inertiaDeg v.1 w.1]
+          simp
+          push_cast
+          simp_rw [← zpow_natCast, ← zpow_mul]
+          grind
+      simp +contextual only [key]
+      simp [g]
+      let f : Ideal (𝓞 L) → ℝ :=
+        fun w ↦ ⨆ i : ι, ‖(FinitePlace.embedding v) (x i)‖ ^ (w.ramificationIdx (𝓞 K) * w.inertiaDeg (𝓞 K))
+      rw [foo L v (f := f)]
+
+      have key : ∀ i : ι, 0 ≤ ‖(FinitePlace.embedding v) (x i)‖ := by
+        intro i
+        positivity
+      simp_rw [f]
+      simp_rw [← Real.iSup_pow key]
+      rw [Finset.prod_pow_eq_pow_sum]
+      congr
+      rw [Algebra.IsAlgebraic.finrank_of_isFractionRing (𝓞 K) K (𝓞 L) L]
+      rw [← Ideal.sum_ramification_inertia_eq_finrank v.1 (𝓞 L)]
+      symm
+      apply Finset.sum_subtype
+      intro I
+      rw [IsDedekindDomain.mem_primesOverFinset_iff]
+      exact v.ne_bot
+    · apply Function.HasFiniteMulSupport.comp_of_injective
+        FinitePlace.equivHeightOneSpectrum.symm.injective
+          (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport (hx i))
+    · apply Function.HasFiniteMulSupport.comp_of_injective
+        FinitePlace.equivHeightOneSpectrum.symm.injective
+          (f := fun v ↦ ⨆ i, v (algebraMap K L (x i)))
+      exact (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport
+        ((map_ne_zero _).mpr (hx i)))
+
+open IsDedekindDomain in
+theorem mulHeight_pow_finrank {ι : Type*} (x : ι → K) [Finite ι] :
+    mulHeight x ^ Module.finrank K L = mulHeight (algebraMap K L ∘ x) := by
+  classical
+  by_cases hx : x = 0
+  · simp [hx]
+  rw [mulHeight_eq_mulHeight_restrict_support]
+  conv_rhs => rw [mulHeight_eq_mulHeight_restrict_support]
+  have : Function.support (algebraMap K L ∘ x) = Function.support x := by
+    ext
+    simp
+  rw [this]
+  have : Nonempty (Function.support x) := by
+    rwa [Set.nonempty_coe_sort, Function.support_nonempty_iff]
+  apply mulHeight_pow_finrank_aux
+  simp
+
+#exit
+
+theorem mulHeight₁_pow_finrank (x : K) :
+    mulHeight₁ x ^ Module.finrank K L = mulHeight₁ (algebraMap K L x) := by
+  rw [mulHeight₁_eq_mulHeight, mulHeight₁_eq_mulHeight, mulHeight_pow_finrank]
+  congr; ext i; fin_cases i <;> simp
+
+theorem finrank_nsmul_logHeight {ι : Type*} (x : ι → K) :
+    Module.finrank K L • logHeight x = logHeight (algebraMap K L ∘ x) := by
+  simp [logHeight_eq_log_mulHeight, ← mulHeight_pow_finrank]
+
+theorem finrank_nsmul_logHeight₁ (x : K) :
+    Module.finrank K L • logHeight₁ x = logHeight₁ (algebraMap K L x) := by
+  simp [logHeight₁_eq_log_mulHeight₁, ← mulHeight₁_pow_finrank]
+
+end extension
+
 variable (K) in
 lemma totalWeight_eq_sum_mult : totalWeight K = ∑ v : InfinitePlace K, v.mult := by
   simp only [totalWeight]

From 0f6ea66e5c3cd7e92ce3622ebd2275e8fc8fd282 Mon Sep 17 00:00:00 2001
From: tb65536 <thomas.l.browning@gmail.com>
Date: Fri, 10 Jul 2026 20:17:17 +0100
Subject: [PATCH 2/8] tmp

---
 Mathlib/NumberTheory/Height/NumberField.lean | 72 +++++++++-----------
 1 file changed, 34 insertions(+), 38 deletions(-)

diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean
index ac1abd2b636428..57f64db3807330 100644
--- a/Mathlib/NumberTheory/Height/NumberField.lean
+++ b/Mathlib/NumberTheory/Height/NumberField.lean
@@ -170,47 +170,48 @@ theorem finprod_fiberwise_univ {ι κ M : Type*} [CommMonoid M]
     ∏ᶠ j, ∏ᶠ i ∈ {i | g i = j}, f i = ∏ᶠ i, f i := by
   simpa using finprod_fiberwise Set.univ g f hf
 
-theorem finprod_mem_pow_eq_pow_finsum {ι M : Type*} [CommMonoid M] (s : Set ι) (f : ι → ℕ)
-    (hf : (s ∩ f.support).Finite) (a : M) :
-    ∏ᶠ i ∈ s, a ^ f i = a ^ ∑ᶠ i ∈ s, f i := by
-  classical
-  rw [finprod_mem_eq_prod_of_subset (t := hf.toFinset.filter (· ∈ s)), Finset.prod_pow_eq_pow_sum,
-    finsum_mem_eq_sum_of_subset (t := hf.toFinset.filter (· ∈ s))]
-  · simp [Function.support]
-    grind
-  · simp
-    grind
-  · simp [Function.mulSupport]
-    intro x ⟨hx1, hx2⟩
-    refine ⟨?_, hx1⟩
-    contrapose! hx2
-    simp [hx2]
-    rw [hx2 hx1, pow_zero]
-  · simp
-    grind
-
 open IsDedekindDomain in
 theorem foo {f : Ideal (𝓞 L) → ℝ} (v : HeightOneSpectrum (𝓞 K)) :
     ∏ᶠ (w : HeightOneSpectrum (𝓞 L)) (_ : w.under (𝓞 K) = v), f w.1 =
-      ∏ w ∈ IsDedekindDomain.primesOverFinset v.1 (𝓞 L), f w := by
-  sorry
+      ∏ w : v.1.primesOver (𝓞 L), f w := by
+  let s : Set (HeightOneSpectrum (𝓞 L)) := {w | w.under (𝓞 K) = v}
+  change ∏ᶠ w ∈ s, f w.1 = ∏ w : v.1.primesOver (𝓞 L), f w
+  have h1 : s.Finite := by
+    sorry
+  let ι : HeightOneSpectrum (𝓞 L) ↪ Ideal (𝓞 L) :=
+    ⟨HeightOneSpectrum.asIdeal, HeightOneSpectrum.asIdeal_injective⟩
+  have h2 : h1.toFinset.map ι = IsDedekindDomain.primesOverFinset v.1 (𝓞 L) := by
+    sorry
+  rw [finprod_mem_eq_finite_toFinset_prod _ h1]
+  transitivity ∏ i ∈ h2, f i
+
+  apply Finset.prod_of_injOn _ HeightOneSpectrum.asIdeal_injective.injOn
+  · intro p hp
+    rw [SetLike.mem_coe, IsDedekindDomain.mem_primesOverFinset_iff]
+    rw [Ideal.primesOver]
+    simp [s, HeightOneSpectrum.ext_iff] at hp
+    refine ⟨p.isPrime, ?_⟩
+    exact ⟨hp.symm⟩
+    exact v.ne_bot
+  · intro i hi h
+    contrapose! h
+    rw [IsDedekindDomain.mem_primesOverFinset_iff] at hi
+    sorry
+  · intro i hi
+    rfl
 
 open scoped NumberField.LiesOver
 
 theorem mult_mul_finrank (v : InfinitePlace K) (w : InfinitePlace L) [hh : w.1.LiesOver v.1] :
     v.mult * Module.finrank v.Completion w.Completion = w.mult := by
-  have : v = w.comap (algebraMap K L) := by
-    have h1 := hh.comp_eq.symm
-    rw [InfinitePlace.ext_iff]
-    rwa [AbsoluteValue.ext_iff] at h1
-  by_cases h : w.IsUnramified K
-  · rw [NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified v h, mul_one]
-    convert NumberField.InfinitePlace.IsUnramified.eq h
-  · rw [NumberField.InfinitePlace.Completion.finrank_eq_two_of_isRamified v h]
-    have := InfinitePlace.isRamified_iff.mp h
-    rw [InfinitePlace.mult, if_pos, InfinitePlace.mult, if_neg, one_mul]
-    simpa using this.1
-    convert this.2
+  have : v = w.comap (algebraMap K L) := Subtype.ext hh.comp_eq.symm
+  by_cases h : w.IsUnramified K -- add IsUnramified or IsRamified (for dot notation)
+  · rw [NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified v h, mul_one,
+      this, h.eq]
+  · rw [NumberField.InfinitePlace.Completion.finrank_eq_two_of_isRamified v h, this,
+      InfinitePlace.mult, if_pos (InfinitePlace.IsRamified.isReal h), InfinitePlace.mult, if_neg] -- add mult_isReal and mult_isComplex
+    rw [InfinitePlace.not_isReal_iff_isComplex]
+    exact InfinitePlace.IsRamified.isComplex h
 
 open IsDedekindDomain in
 theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
@@ -289,11 +290,6 @@ theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
       congr
       rw [Algebra.IsAlgebraic.finrank_of_isFractionRing (𝓞 K) K (𝓞 L) L]
       rw [← Ideal.sum_ramification_inertia_eq_finrank v.1 (𝓞 L)]
-      symm
-      apply Finset.sum_subtype
-      intro I
-      rw [IsDedekindDomain.mem_primesOverFinset_iff]
-      exact v.ne_bot
     · apply Function.HasFiniteMulSupport.comp_of_injective
         FinitePlace.equivHeightOneSpectrum.symm.injective
           (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport (hx i))

From 1391c86b607564abc9e3ffd9586e717e61e4be01 Mon Sep 17 00:00:00 2001
From: tb65536 <thomas.l.browning@gmail.com>
Date: Fri, 10 Jul 2026 20:57:54 +0100
Subject: [PATCH 3/8] clean

---
 Mathlib/NumberTheory/Height/NumberField.lean | 47 +++++++++-----------
 1 file changed, 20 insertions(+), 27 deletions(-)

diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean
index 57f64db3807330..978f0cfe739bcd 100644
--- a/Mathlib/NumberTheory/Height/NumberField.lean
+++ b/Mathlib/NumberTheory/Height/NumberField.lean
@@ -202,6 +202,7 @@ theorem foo {f : Ideal (𝓞 L) → ℝ} (v : HeightOneSpectrum (𝓞 K)) :
 
 open scoped NumberField.LiesOver
 
+-- PRed
 theorem mult_mul_finrank (v : InfinitePlace K) (w : InfinitePlace L) [hh : w.1.LiesOver v.1] :
     v.mult * Module.finrank v.Completion w.Completion = w.mult := by
   have : v = w.comap (algebraMap K L) := Subtype.ext hh.comp_eq.symm
@@ -213,39 +214,32 @@ theorem mult_mul_finrank (v : InfinitePlace K) (w : InfinitePlace L) [hh : w.1.L
     rw [InfinitePlace.not_isReal_iff_isComplex]
     exact InfinitePlace.IsRamified.isComplex h
 
-open IsDedekindDomain in
-theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
-    (x : ι → K) (hx : ∀ i, x i ≠ 0) : -- is nonempty required?
+open IsDedekindDomain InfinitePlace in
+private theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
+    (x : ι → K) (hx : ∀ i, x i ≠ 0) :
     mulHeight x ^ Module.finrank K L = mulHeight (algebraMap K L ∘ x) := by
   classical
   by_cases hx' : x = 0
   · simp [hx']
   rw [mulHeight_eq hx', mulHeight_eq (by simpa [funext_iff] using hx'), mul_pow]
-  simp only [Function.comp_apply]
   congr
-  · rw [← Finset.prod_pow]
-    let g : InfinitePlace L → InfinitePlace K := fun v ↦ v.comap (algebraMap K L)
-    rw [← Finset.univ.prod_fiberwise g]
+  · simp_rw [← Finset.prod_pow, ← pow_mul, Function.comp_apply, ← comap_apply,
+      ← Finset.univ.prod_fiberwise fun v : InfinitePlace L ↦ v.comap (algebraMap K L)]
     apply Finset.prod_congr rfl fun v _ ↦ ?_
-    simp_rw [← InfinitePlace.comap_apply]
-    have key : ∏ w with g w = v, (⨆ i, w.comap (algebraMap K L) (x i)) ^ w.mult =
-        ∏ w with g w = v, (⨆ i, v (x i)) ^ w.mult := by
-      apply Finset.prod_congr rfl fun w hw ↦ ?_
-      rw [Finset.mem_filter_univ, ← InfinitePlace.liesOver_iff_comap_eq] at hw
-      rw [NumberField.InfinitePlace.LiesOver.comap_eq w v]
-    rw [key, Finset.prod_pow_eq_pow_sum, ← pow_mul]
-    congr
-    rw [← v.sum_inertiaDeg_eq_finrank K L, Finset.mul_sum]
-    have : (InfinitePlace.placesOver L v).toFinset =
-        ({w | g w = v} : Finset (InfinitePlace L)) := by
-      ext w
-      simp [InfinitePlace.placesOver, g, InfinitePlace.liesOver_iff_comap_eq]
-    apply Finset.sum_congr this
-    intro w hw
-    rw [Finset.mem_filter_univ, ← InfinitePlace.liesOver_iff_comap_eq] at hw
-    rw [InfinitePlace.inertiaDeg_eq_finrank]
-    apply mult_mul_finrank
-  · simp_rw [← finprod_comp_equiv NumberField.FinitePlace.equivHeightOneSpectrum.symm]
+    set s : Finset (InfinitePlace L) := {w | w.comap (algebraMap K L) = v}
+    have key1 (w : InfinitePlace L) (hw : w ∈ s) (i : ι) :
+        w.comap (algebraMap K L) (x i) = v (x i) := by
+      rw [Finset.mem_filter_univ, ← liesOver_iff_comap_eq] at hw
+      rw [LiesOver.comap_eq w v]
+    have key2 (w : InfinitePlace L) (hw : w ∈ s) : v.mult * v.inertiaDeg w = w.mult := by
+      rw [Finset.mem_filter_univ, ← liesOver_iff_comap_eq] at hw
+      rw [InfinitePlace.inertiaDeg_eq_finrank, mult_mul_finrank]
+    have key3 : (v.placesOver L).toFinset = s := by
+      simp [InfinitePlace.placesOver, InfinitePlace.liesOver_iff_comap_eq, s]
+    simp +contextual only [Finset.prod_pow_eq_pow_sum, Finset.mul_sum,
+      ← v.sum_inertiaDeg_eq_finrank K L, key1, key2, key3]
+  · simp_rw [Function.comp_apply]
+    simp_rw [← finprod_comp_equiv NumberField.FinitePlace.equivHeightOneSpectrum.symm]
     let g : HeightOneSpectrum (𝓞 L) → HeightOneSpectrum (𝓞 K) := fun v ↦ v.under (𝓞 K)
     rw [← finprod_fiberwise_univ g, finprod_pow]
     · apply finprod_congr
@@ -280,7 +274,6 @@ theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
       let f : Ideal (𝓞 L) → ℝ :=
         fun w ↦ ⨆ i : ι, ‖(FinitePlace.embedding v) (x i)‖ ^ (w.ramificationIdx (𝓞 K) * w.inertiaDeg (𝓞 K))
       rw [foo L v (f := f)]
-
       have key : ∀ i : ι, 0 ≤ ‖(FinitePlace.embedding v) (x i)‖ := by
         intro i
         positivity

From 25e7a86dab58d0f2d57acffce925988d50dedb6e Mon Sep 17 00:00:00 2001
From: tb65536 <thomas.l.browning@gmail.com>
Date: Fri, 10 Jul 2026 22:35:36 +0100
Subject: [PATCH 4/8] next

---
 Mathlib/NumberTheory/Height/NumberField.lean | 67 ++++++++++----------
 1 file changed, 33 insertions(+), 34 deletions(-)

diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean
index 978f0cfe739bcd..f961b8a87eaf1d 100644
--- a/Mathlib/NumberTheory/Height/NumberField.lean
+++ b/Mathlib/NumberTheory/Height/NumberField.lean
@@ -214,7 +214,27 @@ theorem mult_mul_finrank (v : InfinitePlace K) (w : InfinitePlace L) [hh : w.1.L
     rw [InfinitePlace.not_isReal_iff_isComplex]
     exact InfinitePlace.IsRamified.isComplex h
 
-open IsDedekindDomain InfinitePlace in
+open IsDedekindDomain in
+theorem _root_.NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply_algebraMap
+    {K L : Type*} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
+    (v : HeightOneSpectrum (𝓞 K)) (w : HeightOneSpectrum (𝓞 L)) (x : K)
+    [w.1.LiesOver v.1] :
+    FinitePlace.equivHeightOneSpectrum.symm w (algebraMap K L x) =
+      FinitePlace.equivHeightOneSpectrum.symm v x ^
+        (w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
+  by_cases hx : x = 0
+  · rw [hx, map_zero, map_zero, map_zero, zero_pow]
+    exact (mul_pos (w.asIdeal.ramificationIdx_pos (𝓞 K)) (w.asIdeal.inertiaDeg_pos (𝓞 K))).ne'
+  simp_rw [NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply,
+    FinitePlace.norm_embedding, HeightOneSpectrum.adicAbv_def]
+  rw [← IsDedekindDomain.HeightOneSpectrum.valuation_liesOver L v, map_pow,
+    Ideal.ramificationIdx'_eq_ramificationIdx v.1 w.1 v.ne_bot,
+    WithZeroMulInt.toNNReal_neg_apply _ (by simpa), WithZeroMulInt.toNNReal_neg_apply _ (by simpa),
+    ← Ideal.absNorm_pow_inertiaDeg v.1 w.1]
+  simp only [Nat.cast_pow, NNReal.coe_zpow, ← zpow_natCast, ← zpow_mul]
+  grind
+
+open IsDedekindDomain FinitePlace InfinitePlace in
 private theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
     (x : ι → K) (hx : ∀ i, x i ≠ 0) :
     mulHeight x ^ Module.finrank K L = mulHeight (algebraMap K L ∘ x) := by
@@ -227,56 +247,35 @@ private theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
       ← Finset.univ.prod_fiberwise fun v : InfinitePlace L ↦ v.comap (algebraMap K L)]
     apply Finset.prod_congr rfl fun v _ ↦ ?_
     set s : Finset (InfinitePlace L) := {w | w.comap (algebraMap K L) = v}
-    have key1 (w : InfinitePlace L) (hw : w ∈ s) (i : ι) :
+    have key1 w (hw : w ∈ s) i :
         w.comap (algebraMap K L) (x i) = v (x i) := by
       rw [Finset.mem_filter_univ, ← liesOver_iff_comap_eq] at hw
       rw [LiesOver.comap_eq w v]
-    have key2 (w : InfinitePlace L) (hw : w ∈ s) : v.mult * v.inertiaDeg w = w.mult := by
+    have key2 w (hw : w ∈ s) : v.mult * v.inertiaDeg w = w.mult := by
       rw [Finset.mem_filter_univ, ← liesOver_iff_comap_eq] at hw
-      rw [InfinitePlace.inertiaDeg_eq_finrank, mult_mul_finrank]
+      rw [inertiaDeg_eq_finrank, mult_mul_finrank]
     have key3 : (v.placesOver L).toFinset = s := by
-      simp [InfinitePlace.placesOver, InfinitePlace.liesOver_iff_comap_eq, s]
+      simp [InfinitePlace.placesOver, liesOver_iff_comap_eq, s]
     simp +contextual only [Finset.prod_pow_eq_pow_sum, Finset.mul_sum,
       ← v.sum_inertiaDeg_eq_finrank K L, key1, key2, key3]
   · simp_rw [Function.comp_apply]
-    simp_rw [← finprod_comp_equiv NumberField.FinitePlace.equivHeightOneSpectrum.symm]
+    simp_rw [← finprod_comp_equiv equivHeightOneSpectrum.symm]
     let g : HeightOneSpectrum (𝓞 L) → HeightOneSpectrum (𝓞 K) := fun v ↦ v.under (𝓞 K)
     rw [← finprod_fiberwise_univ g, finprod_pow]
-    · apply finprod_congr
-      intro v
-      simp_rw [NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply]
-      have key : ∀ (w : HeightOneSpectrum (𝓞 L)) (hw : w ∈ ({w | g w = v})) (i : ι),
-        ‖FinitePlace.embedding w (algebraMap K L (x i))‖ = ‖FinitePlace.embedding v (x i)‖ ^
-          (w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
-        intro w hw i
-        rw [← hw]
-        simp_rw [FinitePlace.norm_embedding, HeightOneSpectrum.adicAbv_def]
+    · refine finprod_congr fun v ↦ ?_
+      have key w (hw : w ∈ ({w | g w = v})) x :
+        equivHeightOneSpectrum.symm w (algebraMap K L x) =
+          equivHeightOneSpectrum.symm v x ^ (w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
         have : w.1.LiesOver v.1 := by
           rw [Set.mem_setOf_eq, HeightOneSpectrum.ext_iff] at hw
           exact ⟨hw.symm⟩
-        rw [hw, ← IsDedekindDomain.HeightOneSpectrum.valuation_liesOver L v w (x i),
-          map_pow, Ideal.ramificationIdx'_eq_ramificationIdx v.1 w.1 v.ne_bot]
-        simp [WithZeroMulInt.toNNReal, MonoidWithZeroHom.coe_mk]
-        split_ifs
-        · simp
-          symm
-          rw [zero_pow, zero_pow]
-          exact (w.asIdeal.ramificationIdx_pos (𝓞 K)).ne'
-          exact (mul_pos (w.asIdeal.ramificationIdx_pos (𝓞 K))
-            (w.asIdeal.inertiaDeg_pos (𝓞 K))).ne'
-        · rw [← Ideal.absNorm_pow_inertiaDeg v.1 w.1]
-          simp
-          push_cast
-          simp_rw [← zpow_natCast, ← zpow_mul]
-          grind
+        apply FinitePlace.equivHeightOneSpectrum_symm_apply_algebraMap
       simp +contextual only [key]
       simp [g]
       let f : Ideal (𝓞 L) → ℝ :=
-        fun w ↦ ⨆ i : ι, ‖(FinitePlace.embedding v) (x i)‖ ^ (w.ramificationIdx (𝓞 K) * w.inertiaDeg (𝓞 K))
+        fun w ↦ ⨆ i : ι, FinitePlace.equivHeightOneSpectrum.symm v (x i) ^ (w.ramificationIdx (𝓞 K) * w.inertiaDeg (𝓞 K))
       rw [foo L v (f := f)]
-      have key : ∀ i : ι, 0 ≤ ‖(FinitePlace.embedding v) (x i)‖ := by
-        intro i
-        positivity
+      have key i : 0 ≤ FinitePlace.equivHeightOneSpectrum.symm v (x i) := by positivity
       simp_rw [f]
       simp_rw [← Real.iSup_pow key]
       rw [Finset.prod_pow_eq_pow_sum]

From 3f2d6263767bdde09ec5e3c38c871d9b6dd56555 Mon Sep 17 00:00:00 2001
From: tb65536 <thomas.l.browning@gmail.com>
Date: Fri, 10 Jul 2026 22:39:40 +0100
Subject: [PATCH 5/8] tmp

---
 Mathlib/NumberTheory/Height/NumberField.lean | 41 ++++++++++----------
 1 file changed, 21 insertions(+), 20 deletions(-)

diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean
index f961b8a87eaf1d..fbaaf724b26a97 100644
--- a/Mathlib/NumberTheory/Height/NumberField.lean
+++ b/Mathlib/NumberTheory/Height/NumberField.lean
@@ -41,6 +41,27 @@ When this file gets long, split the material on heights over `ℚ` off into a fi
 ### Instance for number fields
 -/
 
+-- PRed
+open IsDedekindDomain NumberField in
+theorem _root_.NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply_algebraMap
+    {K L : Type*} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
+    (v : HeightOneSpectrum (𝓞 K)) (w : HeightOneSpectrum (𝓞 L)) (x : K)
+    [w.1.LiesOver v.1] :
+    FinitePlace.equivHeightOneSpectrum.symm w (algebraMap K L x) =
+      FinitePlace.equivHeightOneSpectrum.symm v x ^
+        (w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
+  by_cases hx : x = 0
+  · rw [hx, map_zero, map_zero, map_zero, zero_pow]
+    exact (mul_pos (w.asIdeal.ramificationIdx_pos (𝓞 K)) (w.asIdeal.inertiaDeg_pos (𝓞 K))).ne'
+  simp_rw [NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply,
+    FinitePlace.norm_embedding, HeightOneSpectrum.adicAbv_def]
+  rw [← IsDedekindDomain.HeightOneSpectrum.valuation_liesOver L v, map_pow,
+    Ideal.ramificationIdx'_eq_ramificationIdx v.1 w.1 v.ne_bot,
+    WithZeroMulInt.toNNReal_neg_apply _ (by simpa), WithZeroMulInt.toNNReal_neg_apply _ (by simpa),
+    ← Ideal.absNorm_pow_inertiaDeg v.1 w.1]
+  simp only [Nat.cast_pow, NNReal.coe_zpow, ← zpow_natCast, ← zpow_mul]
+  grind
+
 namespace NumberField
 
 open Height
@@ -214,26 +235,6 @@ theorem mult_mul_finrank (v : InfinitePlace K) (w : InfinitePlace L) [hh : w.1.L
     rw [InfinitePlace.not_isReal_iff_isComplex]
     exact InfinitePlace.IsRamified.isComplex h
 
-open IsDedekindDomain in
-theorem _root_.NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply_algebraMap
-    {K L : Type*} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
-    (v : HeightOneSpectrum (𝓞 K)) (w : HeightOneSpectrum (𝓞 L)) (x : K)
-    [w.1.LiesOver v.1] :
-    FinitePlace.equivHeightOneSpectrum.symm w (algebraMap K L x) =
-      FinitePlace.equivHeightOneSpectrum.symm v x ^
-        (w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
-  by_cases hx : x = 0
-  · rw [hx, map_zero, map_zero, map_zero, zero_pow]
-    exact (mul_pos (w.asIdeal.ramificationIdx_pos (𝓞 K)) (w.asIdeal.inertiaDeg_pos (𝓞 K))).ne'
-  simp_rw [NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply,
-    FinitePlace.norm_embedding, HeightOneSpectrum.adicAbv_def]
-  rw [← IsDedekindDomain.HeightOneSpectrum.valuation_liesOver L v, map_pow,
-    Ideal.ramificationIdx'_eq_ramificationIdx v.1 w.1 v.ne_bot,
-    WithZeroMulInt.toNNReal_neg_apply _ (by simpa), WithZeroMulInt.toNNReal_neg_apply _ (by simpa),
-    ← Ideal.absNorm_pow_inertiaDeg v.1 w.1]
-  simp only [Nat.cast_pow, NNReal.coe_zpow, ← zpow_natCast, ← zpow_mul]
-  grind
-
 open IsDedekindDomain FinitePlace InfinitePlace in
 private theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
     (x : ι → K) (hx : ∀ i, x i ≠ 0) :

From 1520b2986c98fd3df6c0c96d1d691c1302785239 Mon Sep 17 00:00:00 2001
From: tb65536 <thomas.l.browning@gmail.com>
Date: Fri, 10 Jul 2026 23:32:31 +0100
Subject: [PATCH 6/8] add def

---
 Mathlib/NumberTheory/Height/NumberField.lean | 62 +++++++++++---------
 1 file changed, 33 insertions(+), 29 deletions(-)

diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean
index fbaaf724b26a97..cbff82d57ace34 100644
--- a/Mathlib/NumberTheory/Height/NumberField.lean
+++ b/Mathlib/NumberTheory/Height/NumberField.lean
@@ -191,8 +191,9 @@ theorem finprod_fiberwise_univ {ι κ M : Type*} [CommMonoid M]
     ∏ᶠ j, ∏ᶠ i ∈ {i | g i = j}, f i = ∏ᶠ i, f i := by
   simpa using finprod_fiberwise Set.univ g f hf
 
+variable {L} in
 open IsDedekindDomain in
-theorem foo {f : Ideal (𝓞 L) → ℝ} (v : HeightOneSpectrum (𝓞 K)) :
+theorem foo (f : Ideal (𝓞 L) → ℝ) (v : HeightOneSpectrum (𝓞 K)) :
     ∏ᶠ (w : HeightOneSpectrum (𝓞 L)) (_ : w.under (𝓞 K) = v), f w.1 =
       ∏ w : v.1.primesOver (𝓞 L), f w := by
   let s : Set (HeightOneSpectrum (𝓞 L)) := {w | w.under (𝓞 K) = v}
@@ -259,38 +260,26 @@ private theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
       simp [InfinitePlace.placesOver, liesOver_iff_comap_eq, s]
     simp +contextual only [Finset.prod_pow_eq_pow_sum, Finset.mul_sum,
       ← v.sum_inertiaDeg_eq_finrank K L, key1, key2, key3]
-  · simp_rw [Function.comp_apply]
-    simp_rw [← finprod_comp_equiv equivHeightOneSpectrum.symm]
-    let g : HeightOneSpectrum (𝓞 L) → HeightOneSpectrum (𝓞 K) := fun v ↦ v.under (𝓞 K)
-    rw [← finprod_fiberwise_univ g, finprod_pow]
+  · simp_rw [Function.comp_apply, ← finprod_comp_equiv equivHeightOneSpectrum.symm]
+    rw [← finprod_fiberwise_univ fun v : HeightOneSpectrum (𝓞 L) ↦ v.under (𝓞 K), finprod_pow]
     · refine finprod_congr fun v ↦ ?_
-      have key w (hw : w ∈ ({w | g w = v})) x :
+      have key w (hw : w ∈ ({w | w.under (𝓞 K) = v})) x :
         equivHeightOneSpectrum.symm w (algebraMap K L x) =
           equivHeightOneSpectrum.symm v x ^ (w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
         have : w.1.LiesOver v.1 := by
           rw [Set.mem_setOf_eq, HeightOneSpectrum.ext_iff] at hw
           exact ⟨hw.symm⟩
         apply FinitePlace.equivHeightOneSpectrum_symm_apply_algebraMap
-      simp +contextual only [key]
-      simp [g]
-      let f : Ideal (𝓞 L) → ℝ :=
-        fun w ↦ ⨆ i : ι, FinitePlace.equivHeightOneSpectrum.symm v (x i) ^ (w.ramificationIdx (𝓞 K) * w.inertiaDeg (𝓞 K))
-      rw [foo L v (f := f)]
-      have key i : 0 ≤ FinitePlace.equivHeightOneSpectrum.symm v (x i) := by positivity
-      simp_rw [f]
-      simp_rw [← Real.iSup_pow key]
-      rw [Finset.prod_pow_eq_pow_sum]
-      congr
-      rw [Algebra.IsAlgebraic.finrank_of_isFractionRing (𝓞 K) K (𝓞 L) L]
-      rw [← Ideal.sum_ramification_inertia_eq_finrank v.1 (𝓞 L)]
-    · apply Function.HasFiniteMulSupport.comp_of_injective
-        FinitePlace.equivHeightOneSpectrum.symm.injective
-          (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport (hx i))
-    · apply Function.HasFiniteMulSupport.comp_of_injective
-        FinitePlace.equivHeightOneSpectrum.symm.injective
-          (f := fun v ↦ ⨆ i, v (algebraMap K L (x i)))
-      exact (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport
-        ((map_ne_zero _).mpr (hx i)))
+      simp +contextual only [key, Set.mem_setOf_eq]
+      have pos i : 0 ≤ equivHeightOneSpectrum.symm v (x i) := by positivity
+      simp_rw [foo fun w ↦ ⨆ i, equivHeightOneSpectrum.symm v (x i) ^
+        (w.ramificationIdx (𝓞 K) * w.inertiaDeg (𝓞 K)), ← Real.iSup_pow pos,
+        Finset.prod_pow_eq_pow_sum, Ideal.sum_ramification_inertia_eq_finrank v.1 (𝓞 L),
+        Algebra.IsAlgebraic.finrank_of_isFractionRing (𝓞 K) K (𝓞 L) L]
+    · apply Function.HasFiniteMulSupport.comp_of_injective equivHeightOneSpectrum.symm.injective
+        (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport (hx i))
+    · apply Function.HasFiniteMulSupport.comp_of_injective equivHeightOneSpectrum.symm.injective
+        (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport (by simp [hx]))
 
 open IsDedekindDomain in
 theorem mulHeight_pow_finrank {ι : Type*} (x : ι → K) [Finite ι] :
@@ -309,14 +298,12 @@ theorem mulHeight_pow_finrank {ι : Type*} (x : ι → K) [Finite ι] :
   apply mulHeight_pow_finrank_aux
   simp
 
-#exit
-
 theorem mulHeight₁_pow_finrank (x : K) :
     mulHeight₁ x ^ Module.finrank K L = mulHeight₁ (algebraMap K L x) := by
   rw [mulHeight₁_eq_mulHeight, mulHeight₁_eq_mulHeight, mulHeight_pow_finrank]
   congr; ext i; fin_cases i <;> simp
 
-theorem finrank_nsmul_logHeight {ι : Type*} (x : ι → K) :
+theorem finrank_nsmul_logHeight {ι : Type*} [Finite ι] (x : ι → K) :
     Module.finrank K L • logHeight x = logHeight (algebraMap K L ∘ x) := by
   simp [logHeight_eq_log_mulHeight, ← mulHeight_pow_finrank]
 
@@ -324,6 +311,23 @@ theorem finrank_nsmul_logHeight₁ (x : K) :
     Module.finrank K L • logHeight₁ x = logHeight₁ (algebraMap K L x) := by
   simp [logHeight₁_eq_log_mulHeight₁, ← mulHeight₁_pow_finrank]
 
+open Classical IntermediateField in
+/-- The absolute multiplicative height of an algebraic number. -/
+noncomputable def absMulHeight₁ {K : Type*} [Field K] [CharZero K] (x : K) : ℝ :=
+  if hx : IsIntegral ℚ x then
+    haveI : FiniteDimensional ℚ ℚ⟮x⟯ := adjoin.finiteDimensional hx
+    haveI : NumberField ℚ⟮x⟯ := {}
+    (Height.mulHeight₁ (AdjoinSimple.gen ℚ x)) ^ (Module.finrank ℚ ℚ⟮x⟯ : ℝ)⁻¹
+  else 0
+
+open IntermediateField in
+theorem absMulHeight₁_eq {K : Type*} [Field K] [NumberField K] (x : K) :
+    absMulHeight₁ x = Height.mulHeight₁ x ^ (Module.finrank ℚ K : ℝ)⁻¹ := by
+  rw [absMulHeight₁, dif_pos (Algebra.IsIntegral.isIntegral x), ← AdjoinSimple.algebraMap_gen ℚ x,
+    ← mulHeight₁_pow_finrank, AdjoinSimple.algebraMap_gen, ← Real.rpow_natCast,
+    ← Real.rpow_mul (by positivity), ← Module.finrank_mul_finrank ℚ ℚ⟮x⟯ K, Nat.cast_mul,
+    mul_inv_rev, mul_inv_cancel_left₀ (by simpa using Module.finrank_pos.ne')]
+
 end extension
 
 variable (K) in

From ba499999e0f6cf432722d2ad336c66c73432e541 Mon Sep 17 00:00:00 2001
From: tb65536 <thomas.l.browning@gmail.com>
Date: Sat, 11 Jul 2026 00:38:36 +0100
Subject: [PATCH 7/8] basically there

---
 Mathlib/NumberTheory/Height/NumberField.lean | 90 +++++++++++---------
 1 file changed, 48 insertions(+), 42 deletions(-)

diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean
index cbff82d57ace34..b6b5350299e8ab 100644
--- a/Mathlib/NumberTheory/Height/NumberField.lean
+++ b/Mathlib/NumberTheory/Height/NumberField.lean
@@ -193,34 +193,34 @@ theorem finprod_fiberwise_univ {ι κ M : Type*} [CommMonoid M]
 
 variable {L} in
 open IsDedekindDomain in
-theorem foo (f : Ideal (𝓞 L) → ℝ) (v : HeightOneSpectrum (𝓞 K)) :
-    ∏ᶠ (w : HeightOneSpectrum (𝓞 L)) (_ : w.under (𝓞 K) = v), f w.1 =
-      ∏ w : v.1.primesOver (𝓞 L), f w := by
-  let s : Set (HeightOneSpectrum (𝓞 L)) := {w | w.under (𝓞 K) = v}
-  change ∏ᶠ w ∈ s, f w.1 = ∏ w : v.1.primesOver (𝓞 L), f w
-  have h1 : s.Finite := by
-    sorry
-  let ι : HeightOneSpectrum (𝓞 L) ↪ Ideal (𝓞 L) :=
-    ⟨HeightOneSpectrum.asIdeal, HeightOneSpectrum.asIdeal_injective⟩
-  have h2 : h1.toFinset.map ι = IsDedekindDomain.primesOverFinset v.1 (𝓞 L) := by
-    sorry
-  rw [finprod_mem_eq_finite_toFinset_prod _ h1]
-  transitivity ∏ i ∈ h2, f i
-
-  apply Finset.prod_of_injOn _ HeightOneSpectrum.asIdeal_injective.injOn
-  · intro p hp
-    rw [SetLike.mem_coe, IsDedekindDomain.mem_primesOverFinset_iff]
-    rw [Ideal.primesOver]
-    simp [s, HeightOneSpectrum.ext_iff] at hp
-    refine ⟨p.isPrime, ?_⟩
-    exact ⟨hp.symm⟩
-    exact v.ne_bot
-  · intro i hi h
-    contrapose! h
-    rw [IsDedekindDomain.mem_primesOverFinset_iff] at hi
+-- @[to_additive]
+theorem foobar_mul (f : HeightOneSpectrum (𝓞 L) → ℝ) (hf : f.HasFiniteMulSupport) :
+    ∏ᶠ w : HeightOneSpectrum (𝓞 L), f w =
+      ∏ᶠ v : HeightOneSpectrum (𝓞 K), ∏ w : v.1.primesOver (𝓞 L),
+        f ((HeightOneSpectrum.equivPrimesOver (𝓞 L) v.ne_bot).symm w) := by
+  classical
+  let g : HeightOneSpectrum (𝓞 L) → HeightOneSpectrum (𝓞 K) := HeightOneSpectrum.under (𝓞 K)
+  let s : Finset (HeightOneSpectrum (𝓞 K)) := hf.toFinset.image g
+  rw [finprod_eq_prod f hf, finprod_eq_prod_of_mulSupport_subset (s := s)]
+  · rw [← Finset.prod_fiberwise_of_maps_to (fun w ↦ Finset.mem_image_of_mem g)]
+    apply Finset.prod_congr rfl
+    intro v hv
+    let e := HeightOneSpectrum.equivPrimesOver (𝓞 L) v.ne_bot
+    have := Fintype.ofEquiv _ e.symm
+    rw [e.symm.prod_comp (f ·)]
     sorry
-  · intro i hi
-    rfl
+  · intro v
+    let e := HeightOneSpectrum.equivPrimesOver (𝓞 L) v.ne_bot
+    rw [Function.mem_mulSupport, Finset.mem_coe, Finset.mem_image]
+    contrapose!
+    intro hv
+    apply Finset.prod_eq_one
+    intro w hw
+    contrapose! hv
+    refine ⟨e.symm w, hf.mem_toFinset.mpr hv, ?_⟩
+    have := (e.symm w).2
+    rw [← Ideal.liesOver_iff_dvd_map (e.symm w).1.2.ne_top, Ideal.liesOver_iff] at this
+    exact HeightOneSpectrum.asIdeal_injective this.symm
 
 open scoped NumberField.LiesOver
 
@@ -261,25 +261,31 @@ private theorem mulHeight_pow_finrank_aux {ι : Type*} [Nonempty ι] [Finite ι]
     simp +contextual only [Finset.prod_pow_eq_pow_sum, Finset.mul_sum,
       ← v.sum_inertiaDeg_eq_finrank K L, key1, key2, key3]
   · simp_rw [Function.comp_apply, ← finprod_comp_equiv equivHeightOneSpectrum.symm]
-    rw [← finprod_fiberwise_univ fun v : HeightOneSpectrum (𝓞 L) ↦ v.under (𝓞 K), finprod_pow]
+    rw [foobar_mul (K := K) (L := L), finprod_pow]
     · refine finprod_congr fun v ↦ ?_
-      have key w (hw : w ∈ ({w | w.under (𝓞 K) = v})) x :
-        equivHeightOneSpectrum.symm w (algebraMap K L x) =
+      let e := HeightOneSpectrum.equivPrimesOver (𝓞 L) v.ne_bot
+      have key (w : v.asIdeal.primesOver (𝓞 L)) x :
+          equivHeightOneSpectrum.symm (e.symm w) (algebraMap K L x) =
           equivHeightOneSpectrum.symm v x ^ (w.1.ramificationIdx (𝓞 K) * w.1.inertiaDeg (𝓞 K)) := by
-        have : w.1.LiesOver v.1 := by
-          rw [Set.mem_setOf_eq, HeightOneSpectrum.ext_iff] at hw
-          exact ⟨hw.symm⟩
-        apply FinitePlace.equivHeightOneSpectrum_symm_apply_algebraMap
-      simp +contextual only [key, Set.mem_setOf_eq]
+        have : (e.symm w).1.asIdeal.LiesOver v.asIdeal := by
+          rw [Ideal.liesOver_iff_dvd_map]
+          exact (e.symm w).2
+          exact (e.symm w).1.2.ne_top
+        have : w.1 = (e.symm w).1 := by
+          conv_lhs => rw [← e.apply_symm_apply w]
+          rfl
+        have := FinitePlace.equivHeightOneSpectrum_symm_apply_algebraMap v (e.symm w).1 x
+        convert this
+      simp only [e] at key
+      simp only [key]
       have pos i : 0 ≤ equivHeightOneSpectrum.symm v (x i) := by positivity
-      simp_rw [foo fun w ↦ ⨆ i, equivHeightOneSpectrum.symm v (x i) ^
-        (w.ramificationIdx (𝓞 K) * w.inertiaDeg (𝓞 K)), ← Real.iSup_pow pos,
-        Finset.prod_pow_eq_pow_sum, Ideal.sum_ramification_inertia_eq_finrank v.1 (𝓞 L),
+      simp_rw [← Real.iSup_pow pos, Finset.prod_pow_eq_pow_sum,
+        Ideal.sum_ramification_inertia_eq_finrank v.1 (𝓞 L),
         Algebra.IsAlgebraic.finrank_of_isFractionRing (𝓞 K) K (𝓞 L) L]
-    · apply Function.HasFiniteMulSupport.comp_of_injective equivHeightOneSpectrum.symm.injective
-        (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport (hx i))
-    · apply Function.HasFiniteMulSupport.comp_of_injective equivHeightOneSpectrum.symm.injective
-        (Function.HasFiniteMulSupport.iSup fun i ↦ FinitePlace.hasFiniteMulSupport (by simp [hx]))
+    · exact Function.HasFiniteMulSupport.iSup fun i ↦ Function.HasFiniteMulSupport.comp_of_injective
+        equivHeightOneSpectrum.symm.injective (FinitePlace.hasFiniteMulSupport (by simp [hx]))
+    · exact Function.HasFiniteMulSupport.iSup fun i ↦ Function.HasFiniteMulSupport.comp_of_injective
+        equivHeightOneSpectrum.symm.injective (FinitePlace.hasFiniteMulSupport (by simp [hx]))
 
 open IsDedekindDomain in
 theorem mulHeight_pow_finrank {ι : Type*} (x : ι → K) [Finite ι] :

From 70bcdebf97053959b0a1898ca2484563bce0a719 Mon Sep 17 00:00:00 2001
From: tb65536 <thomas.l.browning@gmail.com>
Date: Sat, 11 Jul 2026 00:39:00 +0100
Subject: [PATCH 8/8] clean

---
 Mathlib/NumberTheory/Height/NumberField.lean | 28 --------------------
 1 file changed, 28 deletions(-)

diff --git a/Mathlib/NumberTheory/Height/NumberField.lean b/Mathlib/NumberTheory/Height/NumberField.lean
index b6b5350299e8ab..c95601e8c324f5 100644
--- a/Mathlib/NumberTheory/Height/NumberField.lean
+++ b/Mathlib/NumberTheory/Height/NumberField.lean
@@ -163,34 +163,6 @@ theorem _root_.NumberField.InfinitePlace.liesOver_iff_comap_eq {K L : Type*} [Fi
   rw [AbsoluteValue.liesOver_iff, AbsoluteValue.ext_iff, InfinitePlace.ext_iff]
   rfl
 
-@[to_additive]
-theorem finprod_fiberwise {ι κ M : Type*} [CommMonoid M]
-    (s : Set ι) (g : ι → κ) (f : ι → M) (hf : f.HasFiniteMulSupport) :
-    ∏ᶠ j, ∏ᶠ i ∈ {i ∈ s | g i = j}, f i = ∏ᶠ i ∈ s, f i := by
-  classical
-  let t := hf.toFinset
-  have : ∀ i, f i ≠ 1 → i ∈ t := by simp [t]
-  have : ∀ i ∈ (hf.toFinset.filter (· ∈ s)), g i ∈ t.image g := by grind
-  rw [finprod_mem_eq_prod_filter f s hf, ← Finset.prod_fiberwise_of_maps_to this,
-    finprod_eq_prod_of_mulSupport_subset]
-  · apply Finset.prod_congr rfl
-    intro k hk
-    apply finprod_mem_eq_prod_of_subset
-    · grind [Function.mem_mulSupport]
-    · grind
-  · rw [Function.mulSupport_subset_iff]
-    intro x
-    contrapose!
-    intro h
-    apply finprod_mem_eq_one_of_forall_eq_one
-    grind
-
-@[to_additive]
-theorem finprod_fiberwise_univ {ι κ M : Type*} [CommMonoid M]
-    (g : ι → κ) (f : ι → M) (hf : f.HasFiniteMulSupport) :
-    ∏ᶠ j, ∏ᶠ i ∈ {i | g i = j}, f i = ∏ᶠ i, f i := by
-  simpa using finprod_fiberwise Set.univ g f hf
-
 variable {L} in
 open IsDedekindDomain in
 -- @[to_additive]