import Definitions.Def_UnramifiedWhittaker_ZetaIntegrand

set_option autoImplicit false

open IsDedekindDomain NumberField NumberField.AdelicLevel NumberField.AdeleRing

noncomputable section

namespace NumberField.Idele

variable (F : Type) [Field F] [NumberField F]

def ord (v : HeightOneSpectrum (𝓞 F)) (a : (AdeleRing (𝓞 F) F)ˣ) : ℤ :=
  -WithZero.log (Valued.v ((a : AdeleRing (𝓞 F) F).2 v))

theorem valued_snd_ne_zero (v : HeightOneSpectrum (𝓞 F)) (a : (AdeleRing (𝓞 F) F)ˣ) :
    Valued.v ((a : AdeleRing (𝓞 F) F).2 v) ≠ 0 := by
  rw [← val_finiteUnitsComponent]
  exact (Valuation.ne_zero_iff Valued.v).mpr (Units.ne_zero _)

theorem valued_snd_eq_exp_neg_ord (v : HeightOneSpectrum (𝓞 F)) (a : (AdeleRing (𝓞 F) F)ˣ) :
    Valued.v ((a : AdeleRing (𝓞 F) F).2 v) = WithZero.exp (-(ord F v a)) := by
  rw [ord, neg_neg, WithZero.exp_log (valued_snd_ne_zero F v a)]

theorem ord_mul (v : HeightOneSpectrum (𝓞 F)) (a b : (AdeleRing (𝓞 F) F)ˣ) :
    ord F v (a * b) = ord F v a + ord F v b := by
  have hab : ((a * b : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 v =
      (a : AdeleRing (𝓞 F) F).2 v * (b : AdeleRing (𝓞 F) F).2 v := rfl
  simp only [ord]
  rw [hab, map_mul, WithZero.log_mul (valued_snd_ne_zero F v a) (valued_snd_ne_zero F v b), neg_add]

theorem ord_one (v : HeightOneSpectrum (𝓞 F)) : ord F v 1 = 0 := by
  rw [ord]
  show -WithZero.log (Valued.v (1 : v.adicCompletion F)) = 0
  rw [map_one, WithZero.log_one, neg_zero]

theorem ord_inv (v : HeightOneSpectrum (𝓞 F)) (a : (AdeleRing (𝓞 F) F)ˣ) :
    ord F v a⁻¹ = -ord F v a := by
  have h := ord_mul F v a a⁻¹
  rw [mul_inv_cancel, ord_one] at h
  omega

def unitComponent (v : HeightOneSpectrum (𝓞 F)) (a : (AdeleRing (𝓞 F) F)ˣ) : v.adicCompletion F :=
  (a : AdeleRing (𝓞 F) F).2 v *
    ((uniformizerUnit F v : (v.adicCompletion F)ˣ) : v.adicCompletion F) ^ (-(ord F v a))

theorem valued_unitComponent (v : HeightOneSpectrum (𝓞 F)) (a : (AdeleRing (𝓞 F) F)ˣ) :
    Valued.v (unitComponent F v a) = 1 := by
  rw [unitComponent, map_mul, map_zpow₀, valued_uniformizerUnit, valued_snd_eq_exp_neg_ord,
    ← WithZero.exp_zsmul, ← WithZero.exp_add, ← WithZero.exp_zero]
  congr 1
  simp only [zsmul_eq_mul, Int.cast_id, Int.cast_neg, mul_neg, mul_one, neg_neg, neg_add_cancel]

theorem unitComponent_mul_unitComponent_inv (v : HeightOneSpectrum (𝓞 F))
    (a : (AdeleRing (𝓞 F) F)ˣ) : unitComponent F v a * unitComponent F v a⁻¹ = 1 := by
  have h1 : (a : AdeleRing (𝓞 F) F).2 v * ((a⁻¹ : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 v = 1 := by
    have h : ((a * a⁻¹ : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 v = 1 := by
      rw [mul_inv_cancel]; rfl
    exact h
  simp only [unitComponent]
  rw [ord_inv, neg_neg, mul_mul_mul_comm, h1, one_mul, ← zpow_add₀ (uniformizerUnit F v).ne_zero,
    neg_add_cancel, zpow_zero]

open scoped Classical in

def truncFin (S : Finset (HeightOneSpectrum (𝓞 F))) :
    FiniteAdeleRing (𝓞 F) F →* FiniteAdeleRing (𝓞 F) F where
  toFun x := ⟨fun v => if v ∈ S then x v else 1, x.2.mono fun v hv => by
      show (if v ∈ S then x v else 1) ∈ v.adicCompletionIntegers F
      split_ifs
      · exact hv
      · exact one_mem _⟩
  map_one' := by
    refine Subtype.ext (funext fun v => ?_)
    show (if v ∈ S then (1 : FiniteAdeleRing (𝓞 F) F) v else 1) = (1 : FiniteAdeleRing (𝓞 F) F) v
    split_ifs <;> rfl
  map_mul' x y := by
    refine Subtype.ext (funext fun v => ?_)
    show (if v ∈ S then (x * y) v else 1) =
      (if v ∈ S then x v else 1) * (if v ∈ S then y v else 1)
    split_ifs
    · rfl
    · exact (one_mul (1 : v.adicCompletion F)).symm

def partAtAdele (S : Finset (HeightOneSpectrum (𝓞 F))) : AdeleRing (𝓞 F) F →* AdeleRing (𝓞 F) F where
  toFun a := (a.1, truncFin F S a.2)
  map_one' := Prod.ext rfl (map_one (truncFin F S))
  map_mul' a b := Prod.ext rfl (map_mul (truncFin F S) a.2 b.2)

def partAt (S : Finset (HeightOneSpectrum (𝓞 F))) : (AdeleRing (𝓞 F) F)ˣ →* (AdeleRing (𝓞 F) F)ˣ :=
  Units.map (partAtAdele F S)

open scoped Classical in

def unitFin (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ) :
    (FiniteAdeleRing (𝓞 F) F)ˣ where
  val := ⟨fun v => if v ∈ S then 1 else unitComponent F v a, Filter.Eventually.of_forall fun v => by
      show (if v ∈ S then (1 : v.adicCompletion F) else unitComponent F v a) ∈ v.adicCompletionIntegers F
      split_ifs
      · exact one_mem _
      · rw [HeightOneSpectrum.mem_adicCompletionIntegers]
        exact (valued_unitComponent F v a).le⟩
  inv := ⟨fun v => if v ∈ S then 1 else unitComponent F v a⁻¹, Filter.Eventually.of_forall fun v => by
      show (if v ∈ S then (1 : v.adicCompletion F) else unitComponent F v a⁻¹) ∈
        v.adicCompletionIntegers F
      split_ifs
      · exact one_mem _
      · rw [HeightOneSpectrum.mem_adicCompletionIntegers]
        exact (valued_unitComponent F v a⁻¹).le⟩
  val_inv := by
    refine Subtype.ext (funext fun v => ?_)
    show (if v ∈ S then (1 : v.adicCompletion F) else unitComponent F v a) *
        (if v ∈ S then (1 : v.adicCompletion F) else unitComponent F v a⁻¹) = 1
    split_ifs
    · exact one_mul 1
    · exact unitComponent_mul_unitComponent_inv F v a
  inv_val := by
    refine Subtype.ext (funext fun v => ?_)
    show (if v ∈ S then (1 : v.adicCompletion F) else unitComponent F v a⁻¹) *
        (if v ∈ S then (1 : v.adicCompletion F) else unitComponent F v a) = 1
    split_ifs
    · exact one_mul 1
    · rw [mul_comm]
      exact unitComponent_mul_unitComponent_inv F v a

def unitPart (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ) : (AdeleRing (𝓞 F) F)ˣ :=
  Units.map (finIncl (𝓞 F) F) (unitFin F S a)

theorem ord_uniformizerIdele_self (v : HeightOneSpectrum (𝓞 F)) :
    ord F v (AutomorphicForm.uniformizerIdele F v) = 1 := by
  rw [ord]
  show -WithZero.log (Valued.v (((localUnit (𝓞 F) F v (uniformizerUnit F v) : (FiniteAdeleRing (𝓞 F) F)ˣ) :
    FiniteAdeleRing (𝓞 F) F) v)) = 1
  rw [localUnit_apply_self, valued_uniformizerUnit, WithZero.log_exp, neg_neg]

theorem ord_uniformizerIdele_of_ne {v w : HeightOneSpectrum (𝓞 F)} (h : w ≠ v) :
    ord F w (AutomorphicForm.uniformizerIdele F v) = 0 := by
  rw [ord]
  show -WithZero.log (Valued.v (((localUnit (𝓞 F) F v (uniformizerUnit F v) : (FiniteAdeleRing (𝓞 F) F)ˣ) :
    FiniteAdeleRing (𝓞 F) F) w)) = 0
  rw [localUnit_apply_of_ne (𝓞 F) F v (uniformizerUnit F v) h, map_one, WithZero.log_one, neg_zero]

theorem ord_eq_zero_iff (v : HeightOneSpectrum (𝓞 F)) (a : (AdeleRing (𝓞 F) F)ˣ) :
    ord F v a = 0 ↔
      ((finitePartUnits (𝓞 F) F a : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v ∈
          v.adicCompletionIntegers F ∧
        (((finitePartUnits (𝓞 F) F a)⁻¹ : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v ∈
          v.adicCompletionIntegers F := by
  rw [IsDedekindDomain.FiniteAdeleRing.integer_and_inv_integer_iff_valuation_eq_one]
  show ord F v a = 0 ↔ Valued.v ((a : AdeleRing (𝓞 F) F).2 v) = 1
  constructor
  · intro h
    have h' : WithZero.log (Valued.v ((a : AdeleRing (𝓞 F) F).2 v)) = 0 := by
      rw [ord] at h; exact neg_eq_zero.mp h
    rw [← WithZero.exp_log (valued_snd_ne_zero F v a), h', WithZero.exp_zero]
  · intro h
    rw [ord, h, WithZero.log_one, neg_zero]

theorem partAt_fst (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ) :
    ((partAt F S a : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).1 = (a : AdeleRing (𝓞 F) F).1 := by
  rfl

theorem partAt_snd_of_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    {v : HeightOneSpectrum (𝓞 F)} (hv : v ∈ S) :
    ((partAt F S a : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 v = (a : AdeleRing (𝓞 F) F).2 v := by
  exact if_pos hv

theorem partAt_snd_of_not_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    {v : HeightOneSpectrum (𝓞 F)} (hv : v ∉ S) :
    ((partAt F S a : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 v = 1 := by
  exact if_neg hv

theorem unitPart_fst (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ) :
    ((unitPart F S a : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).1 = 1 := by
  rfl

theorem unitPart_snd_of_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ) :
    ∀ v ∈ S, ((unitPart F S a : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 v = 1 := by
  intro v hv
  exact if_pos hv

theorem unitPart_snd_of_not_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    {v : HeightOneSpectrum (𝓞 F)} (hv : v ∉ S) :
    ((unitPart F S a : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 v =
      (a : AdeleRing (𝓞 F) F).2 v *
        ((uniformizerUnit F v : (v.adicCompletion F)ˣ) : v.adicCompletion F) ^ (-(ord F v a)) := by
  exact if_neg hv

private theorem unitFin_val_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    (v : HeightOneSpectrum (𝓞 F)) :
    ((unitFin F S a : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v ∈ v.adicCompletionIntegers F := by
  by_cases hv : v ∈ S
  · have h : ((unitFin F S a : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v = 1 := if_pos hv
    rw [h]; exact one_mem _
  · have h : ((unitFin F S a : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v = unitComponent F v a :=
      if_neg hv
    rw [h, HeightOneSpectrum.mem_adicCompletionIntegers]; exact (valued_unitComponent F v a).le

private theorem unitFin_inv_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    (v : HeightOneSpectrum (𝓞 F)) :
    (((unitFin F S a)⁻¹ : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v ∈ v.adicCompletionIntegers F := by
  by_cases hv : v ∈ S
  · have h : (((unitFin F S a)⁻¹ : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v = 1 := if_pos hv
    rw [h]; exact one_mem _
  · have h : (((unitFin F S a)⁻¹ : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v =
        unitComponent F v a⁻¹ := if_neg hv
    rw [h, HeightOneSpectrum.mem_adicCompletionIntegers]; exact (valued_unitComponent F v a⁻¹).le

theorem finitePartUnits_unitPart_mem_unitIdeles (S : Finset (HeightOneSpectrum (𝓞 F)))
    (a : (AdeleRing (𝓞 F) F)ˣ) :
    finitePartUnits (𝓞 F) F (unitPart F S a) ∈ IsDedekindDomain.FiniteAdeleRing.unitIdeles (𝓞 F) F := by
  exact ⟨fun v => unitFin_val_mem F S a v, fun v => unitFin_inv_mem F S a v⟩

theorem unitPart_mul (S : Finset (HeightOneSpectrum (𝓞 F))) (a b : (AdeleRing (𝓞 F) F)ˣ) :
    unitPart F S (a * b) = unitPart F S a * unitPart F S b := by
  refine Units.ext ?_
  show AdelicLevel.finIncl (𝓞 F) F ((unitFin F S (a * b) : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) =
    AdelicLevel.finIncl (𝓞 F) F ((unitFin F S a : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) *
      AdelicLevel.finIncl (𝓞 F) F ((unitFin F S b : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F)
  rw [← map_mul]
  refine congrArg _ (Subtype.ext (funext fun v => ?_))
  show ((unitFin F S (a * b) : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v =
    ((unitFin F S a : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v *
      ((unitFin F S b : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v
  by_cases hv : v ∈ S
  · have h1 : ((unitFin F S (a * b) : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v = 1 := if_pos hv
    have h2 : ((unitFin F S a : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v = 1 := if_pos hv
    have h3 : ((unitFin F S b : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v = 1 := if_pos hv
    rw [h1, h2, h3, one_mul]
  · have h1 : ((unitFin F S (a * b) : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v =
        unitComponent F v (a * b) := if_neg hv
    have h2 : ((unitFin F S a : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v = unitComponent F v a :=
      if_neg hv
    have h3 : ((unitFin F S b : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) v = unitComponent F v b :=
      if_neg hv
    have hab : ((a * b : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 v =
        (a : AdeleRing (𝓞 F) F).2 v * (b : AdeleRing (𝓞 F) F).2 v := rfl
    rw [h1, h2, h3]
    simp only [unitComponent]
    rw [hab, ord_mul, neg_add, zpow_add₀ (uniformizerUnit F v).ne_zero, mul_mul_mul_comm]

private theorem idele_ext {a b : (AdeleRing (𝓞 F) F)ˣ}
    (h₁ : ∀ w : InfinitePlace F, infiniteUnitsComponent (𝓞 F) F w a = infiniteUnitsComponent (𝓞 F) F w b)
    (h₂ : ∀ w : HeightOneSpectrum (𝓞 F), finiteUnitsComponent (𝓞 F) F w a = finiteUnitsComponent (𝓞 F) F w b) :
    a = b :=
  Units.ext (Prod.ext (funext fun w => congrArg Units.val (h₁ w))
    (Subtype.ext (funext fun w => congrArg Units.val (h₂ w))))

private theorem iUC_partAt (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    (w : InfinitePlace F) : infiniteUnitsComponent (𝓞 F) F w (partAt F S a) = infiniteUnitsComponent (𝓞 F) F w a :=
  Units.ext rfl

private theorem iUC_unitPart (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    (w : InfinitePlace F) : infiniteUnitsComponent (𝓞 F) F w (unitPart F S a) = 1 :=
  Units.ext rfl

private theorem iUC_uniformizerIdele (v : HeightOneSpectrum (𝓞 F)) (w : InfinitePlace F) :
    infiniteUnitsComponent (𝓞 F) F w (AutomorphicForm.uniformizerIdele F v) = 1 :=
  Units.ext rfl

private theorem fUC_partAt_of_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    {w : HeightOneSpectrum (𝓞 F)} (hw : w ∈ S) :
    finiteUnitsComponent (𝓞 F) F w (partAt F S a) = finiteUnitsComponent (𝓞 F) F w a :=
  Units.ext (if_pos hw)

private theorem fUC_partAt_of_not_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    {w : HeightOneSpectrum (𝓞 F)} (hw : w ∉ S) : finiteUnitsComponent (𝓞 F) F w (partAt F S a) = 1 :=
  Units.ext (if_neg hw)

private theorem fUC_unitPart_of_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    {w : HeightOneSpectrum (𝓞 F)} (hw : w ∈ S) : finiteUnitsComponent (𝓞 F) F w (unitPart F S a) = 1 :=
  Units.ext (if_pos hw)

private theorem val_fUC_unitPart_of_not_mem (S : Finset (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ)
    {w : HeightOneSpectrum (𝓞 F)} (hw : w ∉ S) :
    ((finiteUnitsComponent (𝓞 F) F w (unitPart F S a) : (w.adicCompletion F)ˣ) : w.adicCompletion F) =
      (a : AdeleRing (𝓞 F) F).2 w * (uniformizerUnit F w : w.adicCompletion F) ^ (-(ord F w a)) :=
  if_neg hw

private theorem fUC_uniformizerIdele_self (w : HeightOneSpectrum (𝓞 F)) :
    finiteUnitsComponent (𝓞 F) F w (AutomorphicForm.uniformizerIdele F w) = uniformizerUnit F w :=
  Units.ext (by
    show ((localUnit (𝓞 F) F w (uniformizerUnit F w) : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) w = _
    rw [localUnit_apply_self])

private theorem fUC_uniformizerIdele_of_ne {v w : HeightOneSpectrum (𝓞 F)} (h : w ≠ v) :
    finiteUnitsComponent (𝓞 F) F w (AutomorphicForm.uniformizerIdele F v) = 1 :=
  Units.ext (by
    show ((localUnit (𝓞 F) F v (uniformizerUnit F v) : (FiniteAdeleRing (𝓞 F) F)ˣ) : FiniteAdeleRing (𝓞 F) F) w = 1
    rw [localUnit_apply_of_ne (𝓞 F) F v (uniformizerUnit F v) h])

theorem eq_partAt_mul_prod_mul_unitPart (S : Finset (HeightOneSpectrum (𝓞 F)))
    (L : List (HeightOneSpectrum (𝓞 F))) (hLS : ∀ v ∈ L, v ∉ S) (hL : L.Nodup)
    (a : (AdeleRing (𝓞 F) F)ˣ)
    (ha : a ∈ NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {v | v ∈ L})) :
    a = partAt F S a *
      (L.map fun v => AutomorphicForm.uniformizerIdele F v ^ ord F v a).prod * unitPart F S a := by
  classical
  rw [NumberField.AdeleRing.mem_unitIdelesOutside_iff] at ha
  refine idele_ext F (fun w => ?_) (fun w => ?_)
  · have hMw : infiniteUnitsComponent (𝓞 F) F w
        (L.map fun v => AutomorphicForm.uniformizerIdele F v ^ ord F v a).prod = 1 := by
      rw [map_list_prod, List.map_map]
      refine List.prod_eq_one fun x hx => ?_
      obtain ⟨v, -, rfl⟩ := List.mem_map.mp hx
      rw [Function.comp_apply, map_zpow, iUC_uniformizerIdele, one_zpow]
    rw [map_mul, map_mul, iUC_partAt, hMw, iUC_unitPart, mul_one, mul_one]
  · have hMw : finiteUnitsComponent (𝓞 F) F w
        (L.map fun v => AutomorphicForm.uniformizerIdele F v ^ ord F v a).prod =
        (finiteUnitsComponent (𝓞 F) F w (AutomorphicForm.uniformizerIdele F w) ^ ord F w a) ^
          L.count w := by
      rw [map_list_prod, List.map_map, List.prod_map_eq_pow_single w]
      · rw [Function.comp_apply, map_zpow]
      · intro v hvw _
        rw [Function.comp_apply, map_zpow, fUC_uniformizerIdele_of_ne F hvw.symm, one_zpow]
    rw [map_mul, map_mul, hMw]
    by_cases hwS : w ∈ S
    · have hwL : w ∉ L := fun h => hLS w h hwS
      rw [fUC_partAt_of_mem F S a hwS, fUC_unitPart_of_mem F S a hwS, List.count_eq_zero.mpr hwL,
        pow_zero, mul_one, mul_one]
    · rw [fUC_partAt_of_not_mem F S a hwS, one_mul]
      refine Units.ext ?_
      rw [Units.val_mul, val_fUC_unitPart_of_not_mem F S a hwS, Units.val_pow_eq_pow_val,
        Units.val_zpow_eq_zpow_val, fUC_uniformizerIdele_self]
      by_cases hwL : w ∈ L
      · rw [List.count_eq_one_of_mem hL hwL, pow_one, mul_left_comm,
          ← zpow_add₀ (uniformizerUnit F w).ne_zero, add_neg_cancel, zpow_zero, mul_one]
        rfl
      · have hw' : w ∉ (↑S ∪ {v | v ∈ L} : Set (HeightOneSpectrum (𝓞 F))) := by
          rintro (h | h)
          · exact hwS h
          · exact hwL h
        have h0 : ord F w a = 0 := (ord_eq_zero_iff F w a).mpr (ha w hw')
        rw [List.count_eq_zero.mpr hwL, pow_zero, one_mul, h0, neg_zero, zpow_zero, mul_one]
        rfl

theorem diagOne_eq_diagOne_partAt_mul_prod_mul (S : Finset (HeightOneSpectrum (𝓞 F)))
    (L : List (HeightOneSpectrum (𝓞 F))) (hLS : ∀ v ∈ L, v ∉ S) (hL : L.Nodup)
    (a : (AdeleRing (𝓞 F) F)ˣ)
    (ha : a ∈ NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {v | v ∈ L})) :
    diagOne a = diagOne (partAt F S a) *
      (L.map fun v => diagOne (AutomorphicForm.uniformizerIdele F v) ^ ord F v a).prod *
        diagOne (unitPart F S a) := by
  conv_lhs => rw [eq_partAt_mul_prod_mul_unitPart F S L hLS hL a ha]
  simp only [map_mul, map_list_prod, List.map_map, Function.comp_def, map_zpow]

theorem diagOne_mul_finEmbed_localEmbed_of_snd_eq_one {v : HeightOneSpectrum (𝓞 F)}
    (a : (AdeleRing (𝓞 F) F)ˣ) (hav : (a : AdeleRing (𝓞 F) F).2 v = 1)
    (x : GL (Fin 2) (v.adicCompletion F)) :
    diagOne a * AdelicDock.finEmbed (𝓞 F) F (AdelicDock.localEmbed (𝓞 F) F v x) =
      AdelicDock.finEmbed (𝓞 F) F (AdelicDock.localEmbed (𝓞 F) F v x) * diagOne a := by
  refine Units.ext ?_
  rw [Units.val_mul, Units.val_mul, AdelicDock.coe_finEmbed, AdelicDock.coe_localEmbed]
  refine AdelicDock.matrix_eq_of_mapMatrix_arch_fin_eq (𝓞 F) F ?_ ?_
  · rw [map_mul, map_mul, AdelicDock.mapMatrix_arch_finMat, mul_one, one_mul]
  · rw [map_mul, map_mul, AdelicDock.mapMatrix_fin_finMat]
    refine AdelicDock.matrix_eq_of_forall_mapMatrix_finAdeleEval_eq (𝓞 F) F fun w => ?_
    rw [map_mul, map_mul]
    by_cases hw : w = v
    · have h00 : finAdeleEval (𝓞 F) F v (adeleFin (𝓞 F) F (a : AdeleRing (𝓞 F) F)) = 1 := hav
      have hdiag : (finAdeleEval (𝓞 F) F v).mapMatrix ((adeleFin (𝓞 F) F).mapMatrix
          ((diagOne a : GL (Fin 2) (AdeleRing (𝓞 F) F)) : Matrix (Fin 2) (Fin 2) (AdeleRing (𝓞 F) F))) = 1 := by
        ext i j
        fin_cases i <;> fin_cases j <;>
          simp [RingHom.mapMatrix_apply, Matrix.map_apply, diagOne_coe_apply, h00]
      rw [hw, hdiag, AdelicDock.mapMatrix_localMat_self, one_mul, mul_one]
    · rw [AdelicDock.mapMatrix_localMat_of_ne (𝓞 F) F v _ hw, mul_one, one_mul]

theorem diagOne_partAt_mul_finEmbed_localEmbed (S : Finset (HeightOneSpectrum (𝓞 F)))
    (a : (AdeleRing (𝓞 F) F)ˣ) {v : HeightOneSpectrum (𝓞 F)} (hv : v ∉ S)
    (x : GL (Fin 2) (v.adicCompletion F)) :
    diagOne (partAt F S a) * AdelicDock.finEmbed (𝓞 F) F (AdelicDock.localEmbed (𝓞 F) F v x) =
      AdelicDock.finEmbed (𝓞 F) F (AdelicDock.localEmbed (𝓞 F) F v x) * diagOne (partAt F S a) := by
  exact diagOne_mul_finEmbed_localEmbed_of_snd_eq_one F (partAt F S a) (partAt_snd_of_not_mem F S a hv) x

end NumberField.Idele

namespace NumberField.Idele

open MeasureTheory

variable (F : Type) [Field F] [NumberField F]

@[reducible] def ideleBorel : MeasurableSpace (AdeleRing (𝓞 F) F)ˣ := borel _

theorem borelSpace_ideleBorel : @BorelSpace (AdeleRing (𝓞 F) F)ˣ _ (ideleBorel F) :=
  @BorelSpace.mk _ _ (ideleBorel F) rfl

attribute [local instance] ideleBorel borelSpace_ideleBorel

def idelicHaar : Measure (AdeleRing (𝓞 F) F)ˣ := Measure.haar

theorem isHaarMeasure_idelicHaar : (idelicHaar F).IsHaarMeasure := by
  rw [idelicHaar]; infer_instance

attribute [local instance] isHaarMeasure_idelicHaar

theorem isOpen_unitIdelesOutside (T : Set (HeightOneSpectrum (𝓞 F))) :
    IsOpen (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F T : Set (AdeleRing (𝓞 F) F)ˣ) := by
  have hO : IsOpen {x : FiniteAdeleRing (𝓞 F) F | ∀ v, v ∉ T → x.1 v ∈ v.adicCompletionIntegers F} :=
    RestrictedProduct.isOpen_forall_imp_mem fun v => Valued.isOpen_valuationSubring _
  have h1 : Continuous fun a : (AdeleRing (𝓞 F) F)ˣ => (a : AdeleRing (𝓞 F) F).2 :=
    continuous_snd.comp Units.continuous_val
  have h2 : Continuous fun a : (AdeleRing (𝓞 F) F)ˣ => ((a⁻¹ : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2 :=
    continuous_snd.comp Units.continuous_coe_inv
  have hset : (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F T : Set (AdeleRing (𝓞 F) F)ˣ) =
      (fun a : (AdeleRing (𝓞 F) F)ˣ => (a : AdeleRing (𝓞 F) F).2) ⁻¹'
          {x : FiniteAdeleRing (𝓞 F) F | ∀ v, v ∉ T → x.1 v ∈ v.adicCompletionIntegers F} ∩
        (fun a : (AdeleRing (𝓞 F) F)ˣ => ((a⁻¹ : (AdeleRing (𝓞 F) F)ˣ) : AdeleRing (𝓞 F) F).2) ⁻¹'
          {x : FiniteAdeleRing (𝓞 F) F | ∀ v, v ∉ T → x.1 v ∈ v.adicCompletionIntegers F} := by
    ext a
    rw [SetLike.mem_coe, NumberField.AdeleRing.mem_unitIdelesOutside_iff,
      IsDedekindDomain.FiniteAdeleRing.mem_unitIdelesOutside_iff]
    exact ⟨fun h => Set.mem_inter (fun v hv => (h v hv).1) (fun v hv => (h v hv).2),
      fun h v hv => ⟨h.1 v hv, h.2 v hv⟩⟩
  rw [hset]
  exact (hO.preimage h1).inter (hO.preimage h2)

theorem idelicHaar_unitIdelesOutside_ne_zero (T : Set (HeightOneSpectrum (𝓞 F))) :
    idelicHaar F (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F T : Set (AdeleRing (𝓞 F) F)ˣ) ≠ 0 :=
  (isOpen_unitIdelesOutside F T).measure_ne_zero _ ⟨1, Subgroup.one_mem _⟩

open scoped Classical in

theorem truncFin_eq_mapAlong (S : Finset (HeightOneSpectrum (𝓞 F))) :
    (truncFin F S : FiniteAdeleRing (𝓞 F) F → FiniteAdeleRing (𝓞 F) F) =
      RestrictedProduct.mapAlong (fun v : HeightOneSpectrum (𝓞 F) => v.adicCompletion F)
        (fun v : HeightOneSpectrum (𝓞 F) => v.adicCompletion F) id Filter.tendsto_id
        (fun v x => if v ∈ S then x else 1)
        (Filter.Eventually.of_forall fun v => by
          intro x hx
          show (if v ∈ S then x else 1) ∈ (v.adicCompletionIntegers F : Set (v.adicCompletion F))
          by_cases h : v ∈ S
          · rw [if_pos h]; exact hx
          · rw [if_neg h]; exact one_mem _) := by
  funext x
  exact RestrictedProduct.ext _ _ fun v => rfl

open scoped Classical in

theorem continuous_truncFin (S : Finset (HeightOneSpectrum (𝓞 F))) : Continuous (truncFin F S) := by
  rw [truncFin_eq_mapAlong]
  refine RestrictedProduct.mapAlong_continuous _ _ _ _ _ _ fun v => ?_
  show Continuous fun x : v.adicCompletion F => if v ∈ S then x else 1
  by_cases h : v ∈ S
  · simp only [if_pos h]; exact continuous_id
  · simp only [if_neg h]; exact continuous_const

theorem continuous_partAtAdele (S : Finset (HeightOneSpectrum (𝓞 F))) : Continuous (partAtAdele F S) :=
  Continuous.prodMk continuous_fst ((continuous_truncFin F S).comp continuous_snd)

theorem continuous_partAt (S : Finset (HeightOneSpectrum (𝓞 F))) : Continuous (partAt F S) :=
  Continuous.units_map _ (continuous_partAtAdele F S)

theorem measurable_partAt (S : Finset (HeightOneSpectrum (𝓞 F))) : Measurable (partAt F S) :=
  (continuous_partAt F S).measurable

def sPartMeasure (S : Finset (HeightOneSpectrum (𝓞 F))) : Measure (AdeleRing (𝓞 F) F)ˣ :=
  Measure.map (partAt F S)
    ((idelicHaar F).restrict (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S) : Set (AdeleRing (𝓞 F) F)ˣ))

theorem sPartMeasure_ne_zero (S : Finset (HeightOneSpectrum (𝓞 F))) : sPartMeasure F S ≠ 0 := by
  intro h
  have h1 := congrArg (fun μ : Measure (AdeleRing (𝓞 F) F)ˣ => μ Set.univ) h
  simp only [sPartMeasure, Measure.map_apply (measurable_partAt F S) MeasurableSet.univ, Set.preimage_univ,
    Measure.restrict_apply_univ, Measure.coe_zero, Pi.zero_apply] at h1
  exact idelicHaar_unitIdelesOutside_ne_zero F _ h1

private def ordHom (v : HeightOneSpectrum (𝓞 F)) : (AdeleRing (𝓞 F) F)ˣ →* Multiplicative ℤ where
  toFun a := Multiplicative.ofAdd (ord F v a)
  map_one' := by rw [ord_one]; rfl
  map_mul' a b := by rw [ord_mul]; rfl

private theorem ord_zpow (v : HeightOneSpectrum (𝓞 F)) (a : (AdeleRing (𝓞 F) F)ˣ) (n : ℤ) :
    ord F v (a ^ n) = n * ord F v a := by
  have h : Multiplicative.ofAdd (ord F v (a ^ n)) = Multiplicative.ofAdd (ord F v a) ^ n :=
    map_zpow (ordHom F v) a n
  rw [← ofAdd_zsmul] at h
  rw [Multiplicative.ofAdd.injective h, smul_eq_mul]

private theorem fUC_partAt_uniformizerIdele (S : Finset (HeightOneSpectrum (𝓞 F))) {v : HeightOneSpectrum (𝓞 F)}
    (hv : v ∉ S) (w : HeightOneSpectrum (𝓞 F)) :
    finiteUnitsComponent (𝓞 F) F w (partAt F S (AutomorphicForm.uniformizerIdele F v)) = 1 := by
  by_cases hw : w ∈ S
  · rw [fUC_partAt_of_mem F S _ hw]
    exact fUC_uniformizerIdele_of_ne F fun h => hv (h ▸ hw)
  · exact fUC_partAt_of_not_mem F S _ hw

private theorem partAt_uniformizerIdele_of_not_mem (S : Finset (HeightOneSpectrum (𝓞 F)))
    {v : HeightOneSpectrum (𝓞 F)} (hv : v ∉ S) : partAt F S (AutomorphicForm.uniformizerIdele F v) = 1 := by
  refine idele_ext F (fun w => ?_) (fun w => ?_)
  · rw [iUC_partAt, iUC_uniformizerIdele, map_one]
  · rw [fUC_partAt_uniformizerIdele F S hv, map_one]

private theorem mem_unitIdelesOutside_iff_ord (T : Set (HeightOneSpectrum (𝓞 F))) (a : (AdeleRing (𝓞 F) F)ˣ) :
    a ∈ NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F T ↔ ∀ w, w ∉ T → ord F w a = 0 := by
  rw [NumberField.AdeleRing.mem_unitIdelesOutside_iff, IsDedekindDomain.FiniteAdeleRing.mem_unitIdelesOutside_iff]
  refine forall_congr' fun w => imp_congr_right fun _ => ?_
  rw [ord_eq_zero_iff]
  rfl

private theorem mem_image_uniformizerIdele_zpow_mul_iff (T' : Set (HeightOneSpectrum (𝓞 F)))
    {v : HeightOneSpectrum (𝓞 F)} (hv : v ∉ T') (n : ℤ) (a : (AdeleRing (𝓞 F) F)ˣ) :
    a ∈ (fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b) ''
        (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F T' : Set (AdeleRing (𝓞 F) F)ˣ) ↔
      a ∈ (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (insert v T') : Set (AdeleRing (𝓞 F) F)ˣ) ∧
        ord F v a = n := by
  constructor
  · rintro ⟨b, hb, rfl⟩
    rw [SetLike.mem_coe, mem_unitIdelesOutside_iff_ord] at hb
    refine ⟨?_, ?_⟩
    · rw [SetLike.mem_coe, mem_unitIdelesOutside_iff_ord]
      intro w hw
      rw [Set.mem_insert_iff, not_or] at hw
      rw [ord_mul, ord_zpow, ord_uniformizerIdele_of_ne F hw.1, mul_zero, zero_add, hb w hw.2]
    · rw [ord_mul, ord_zpow, ord_uniformizerIdele_self, mul_one, hb v hv, add_zero]
  · rintro ⟨ha, hn⟩
    rw [SetLike.mem_coe, mem_unitIdelesOutside_iff_ord] at ha
    refine ⟨AutomorphicForm.uniformizerIdele F v ^ (-n) * a, ?_, ?_⟩
    · rw [SetLike.mem_coe, mem_unitIdelesOutside_iff_ord]
      intro w hw
      by_cases hwv : w = v
      · rw [hwv, ord_mul, ord_zpow, ord_uniformizerIdele_self, mul_one, hn, neg_add_cancel]
      · rw [ord_mul, ord_zpow, ord_uniformizerIdele_of_ne F hwv, mul_zero, zero_add]
        exact ha w fun h => (Set.mem_insert_iff.mp h).elim hwv hw
    · show AutomorphicForm.uniformizerIdele F v ^ n * (AutomorphicForm.uniformizerIdele F v ^ (-n) * a) = a
      rw [← mul_assoc, ← zpow_add, add_neg_cancel, zpow_zero, one_mul]

private theorem iUnion_image_uniformizerIdele_zpow_mul (T' : Set (HeightOneSpectrum (𝓞 F)))
    {v : HeightOneSpectrum (𝓞 F)} (hv : v ∉ T') :
    (⋃ n : ℤ, (fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b) ''
        (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F T' : Set (AdeleRing (𝓞 F) F)ˣ)) =
      (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (insert v T') : Set (AdeleRing (𝓞 F) F)ˣ) := by
  ext a
  rw [Set.mem_iUnion]
  constructor
  · rintro ⟨n, h⟩
    exact ((mem_image_uniformizerIdele_zpow_mul_iff F T' hv n a).mp h).1
  · intro h
    exact ⟨ord F v a, (mem_image_uniformizerIdele_zpow_mul_iff F T' hv _ a).mpr ⟨h, rfl⟩⟩

private theorem pairwise_disjoint_image_uniformizerIdele_zpow_mul (T' : Set (HeightOneSpectrum (𝓞 F)))
    {v : HeightOneSpectrum (𝓞 F)} (hv : v ∉ T') :
    Pairwise (Function.onFun Disjoint fun n : ℤ =>
      (fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b) ''
        (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F T' : Set (AdeleRing (𝓞 F) F)ˣ)) := by
  intro m n hmn
  refine Set.disjoint_left.mpr fun a ham han => hmn ?_
  exact ((mem_image_uniformizerIdele_zpow_mul_iff F T' hv m a).mp ham).2.symm.trans
    ((mem_image_uniformizerIdele_zpow_mul_iff F T' hv n a).mp han).2

private theorem integrableOn_and_integral_eq (S : Finset (HeightOneSpectrum (𝓞 F)))
    (f : (AdeleRing (𝓞 F) F)ˣ → ℂ) (φ : HeightOneSpectrum (𝓞 F) → ℤ → ℂ) (hf : Integrable f (sPartMeasure F S)) :
    ∀ (L : List (HeightOneSpectrum (𝓞 F))), (∀ v ∈ L, v ∉ S) → L.Nodup →
      (∀ v ∈ L, Summable fun m : ℤ => ‖φ v m‖) →
        IntegrableOn (fun a => f (partAt F S a) * (L.map fun v => φ v (ord F v a)).prod)
            (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {v | v ∈ L}) : Set (AdeleRing (𝓞 F) F)ˣ)
            (idelicHaar F) ∧
          (∫ a in (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {v | v ∈ L}) : Set (AdeleRing (𝓞 F) F)ˣ),
              f (partAt F S a) * (L.map fun v => φ v (ord F v a)).prod ∂(idelicHaar F)) =
            (∫ a, f a ∂(sPartMeasure F S)) * (L.map fun v => ∑' m : ℤ, φ v m).prod := by
  intro L
  induction L with
  | nil =>
    intro _ _ _
    have hT : (↑S ∪ {v | v ∈ ([] : List (HeightOneSpectrum (𝓞 F)))} : Set (HeightOneSpectrum (𝓞 F))) = ↑S := by
      ext w
      simp only [Set.mem_union, Set.mem_setOf_eq, List.not_mem_nil, or_false]
    simp only [List.map_nil, List.prod_nil, mul_one, hT]
    have hφm : AEMeasurable (partAt F S) ((idelicHaar F).restrict
        (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S) : Set (AdeleRing (𝓞 F) F)ˣ)) :=
      (measurable_partAt F S).aemeasurable
    rw [sPartMeasure] at hf ⊢
    exact ⟨(integrable_map_measure hf.aestronglyMeasurable hφm).mp hf,
      (integral_map hφm hf.aestronglyMeasurable).symm⟩
  | cons v L' IH =>
    intro hLS hL hφ
    have hvS : v ∉ S := hLS v (List.mem_cons.mpr (Or.inl rfl))
    have hLS' : ∀ w ∈ L', w ∉ S := fun w hw => hLS w (List.mem_cons.mpr (Or.inr hw))
    have hvL' : v ∉ L' := (List.nodup_cons.mp hL).1
    have hL' : L'.Nodup := (List.nodup_cons.mp hL).2
    have hφv : Summable fun m : ℤ => ‖φ v m‖ := hφ v (List.mem_cons.mpr (Or.inl rfl))
    have hφ' : ∀ w ∈ L', Summable fun m : ℤ => ‖φ w m‖ := fun w hw => hφ w (List.mem_cons.mpr (Or.inr hw))
    obtain ⟨IHi, IHe⟩ := IH hLS' hL' hφ'

    have hv' : v ∉ (↑S ∪ {w | w ∈ L'} : Set (HeightOneSpectrum (𝓞 F))) := by
      rintro (h | h)
      · exact hvS (Finset.mem_coe.mp h)
      · exact hvL' h
    have hT : (↑S ∪ {w | w ∈ v :: L'} : Set (HeightOneSpectrum (𝓞 F))) = insert v (↑S ∪ {w | w ∈ L'}) := by
      ext w
      simp only [Set.mem_union, Set.mem_setOf_eq, List.mem_cons, Set.mem_insert_iff, Finset.mem_coe]
      tauto
    rw [hT, ← iUnion_image_uniformizerIdele_zpow_mul F _ hv']

    have hkey : ∀ (n : ℤ) (b : (AdeleRing (𝓞 F) F)ˣ),
        b ∈ (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ) →
        f (partAt F S (AutomorphicForm.uniformizerIdele F v ^ n * b)) *
            ((v :: L').map fun w => φ w (ord F w (AutomorphicForm.uniformizerIdele F v ^ n * b))).prod =
          φ v n * (f (partAt F S b) * (L'.map fun w => φ w (ord F w b)).prod) := by
      intro n b hb
      rw [SetLike.mem_coe, mem_unitIdelesOutside_iff_ord] at hb
      have h1 : partAt F S (AutomorphicForm.uniformizerIdele F v ^ n * b) = partAt F S b := by
        rw [map_mul, map_zpow, partAt_uniformizerIdele_of_not_mem F S hvS, one_zpow, one_mul]
      have h2 : ord F v (AutomorphicForm.uniformizerIdele F v ^ n * b) = n := by
        rw [ord_mul, ord_zpow, ord_uniformizerIdele_self, mul_one, hb v hv', add_zero]
      have h3 : ((L'.map fun w => φ w (ord F w (AutomorphicForm.uniformizerIdele F v ^ n * b))) :
          List ℂ) = L'.map fun w => φ w (ord F w b) := by
        refine List.map_congr_left fun w hw => ?_
        have hwv : w ≠ v := fun h => hvL' (h ▸ hw)
        rw [ord_mul, ord_zpow, ord_uniformizerIdele_of_ne F hwv, mul_zero, zero_add]
      rw [List.map_cons, List.prod_cons, h1, h2, h3]
      ring

    have hmp : ∀ n : ℤ, MeasurePreserving
        (fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b) (idelicHaar F) (idelicHaar F) :=
      fun n => measurePreserving_mul_left (idelicHaar F) _
    have hme : ∀ n : ℤ, MeasurableEmbedding
        fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b :=
      fun n => (MeasurableEquiv.mulLeft (AutomorphicForm.uniformizerIdele F v ^ n)).measurableEmbedding
    have hU' : MeasurableSet
        (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ) :=
      (isOpen_unitIdelesOutside F _).measurableSet
    have hmeas : ∀ n : ℤ, MeasurableSet
        ((fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b) ''
          (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ)) :=
      fun n => (hme n).measurableSet_image.mpr hU'

    have hpi : ∀ n : ℤ, IntegrableOn (fun a => f (partAt F S a) * ((v :: L').map fun w => φ w (ord F w a)).prod)
        ((fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b) ''
          (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ))
        (idelicHaar F) := by
      intro n
      have hc0 : IntegrableOn (fun b => φ v n * (f (partAt F S b) * (L'.map fun w => φ w (ord F w b)).prod))
          (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ)
          (idelicHaar F) :=
        Integrable.const_mul IHi (φ v n)
      have hc : IntegrableOn (fun b => f (partAt F S (AutomorphicForm.uniformizerIdele F v ^ n * b)) *
            ((v :: L').map fun w => φ w (ord F w (AutomorphicForm.uniformizerIdele F v ^ n * b))).prod)
          (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ)
          (idelicHaar F) :=
        hc0.congr_fun (fun b hb => (hkey n b hb).symm) hU'
      exact (((hmp n).restrict_image_emb (hme n) _).integrable_comp_emb (hme n)
        (g := fun a => f (partAt F S a) * ((v :: L').map fun w => φ w (ord F w a)).prod)).mp hc
    have hnorm : ∀ n : ℤ, (∫ a in (fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b) ''
          (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ),
          ‖f (partAt F S a) * ((v :: L').map fun w => φ w (ord F w a)).prod‖ ∂(idelicHaar F)) =
        ‖φ v n‖ * ∫ b in (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) :
            Set (AdeleRing (𝓞 F) F)ˣ),
          ‖f (partAt F S b) * (L'.map fun w => φ w (ord F w b)).prod‖ ∂(idelicHaar F) := by
      intro n
      rw [(hmp n).setIntegral_image_emb (hme n), ← integral_const_mul]
      refine setIntegral_congr_fun hU' fun b hb => ?_
      show ‖f (partAt F S (AutomorphicForm.uniformizerIdele F v ^ n * b)) *
          ((v :: L').map fun w => φ w (ord F w (AutomorphicForm.uniformizerIdele F v ^ n * b))).prod‖ =
        ‖φ v n‖ * ‖f (partAt F S b) * (L'.map fun w => φ w (ord F w b)).prod‖
      rw [hkey n b hb, norm_mul]
    have hsum : Summable fun n : ℤ => ∫ a in (fun b : (AdeleRing (𝓞 F) F)ˣ =>
          AutomorphicForm.uniformizerIdele F v ^ n * b) ''
          (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ),
          ‖f (partAt F S a) * ((v :: L').map fun w => φ w (ord F w a)).prod‖ ∂(idelicHaar F) := by
      simp_rw [hnorm]
      exact hφv.mul_right _
    have hint := integrableOn_iUnion_of_summable_integral_norm hpi hsum
    refine ⟨hint, ?_⟩

    rw [integral_iUnion hmeas (pairwise_disjoint_image_uniformizerIdele_zpow_mul F _ hv') hint]
    have hval : ∀ n : ℤ, (∫ a in (fun b : (AdeleRing (𝓞 F) F)ˣ => AutomorphicForm.uniformizerIdele F v ^ n * b) ''
          (NumberField.AdeleRing.unitIdelesOutside (𝓞 F) F (↑S ∪ {w | w ∈ L'}) : Set (AdeleRing (𝓞 F) F)ˣ),
          f (partAt F S a) * ((v :: L').map fun w => φ w (ord F w a)).prod ∂(idelicHaar F)) =
        φ v n * ((∫ a, f a ∂(sPartMeasure F S)) * (L'.map fun w => ∑' m : ℤ, φ w m).prod) := by
      intro n
      rw [(hmp n).setIntegral_image_emb (hme n), ← IHe, ← integral_const_mul]
      exact setIntegral_congr_fun hU' fun b hb => hkey n b hb
    simp_rw [hval]
    rw [tsum_mul_right, List.map_cons, List.prod_cons]
    ring

def productMeasureData (S : Finset (HeightOneSpectrum (𝓞 F))) :
    @UnramifiedWhittaker.ProductMeasureData F _ _ (ideleBorel F) S (idelicHaar F) where
  c := 1
  c_pos := one_pos
  νS := sPartMeasure F S
  projS := partAt F S
  ord := ord F
  projS_off a _ hv := partAt_snd_of_not_mem F S a hv
  decomp L hLS hL a ha := ⟨unitPart F S a, unitPart_fst F S a, unitPart_snd_of_mem F S a,
    finitePartUnits_unitPart_mem_unitIdeles F S a, eq_partAt_mul_prod_mul_unitPart F S L hLS hL a ha⟩
  tonelli L hLS hL f φ hf hφ := by
    obtain ⟨h1, h2⟩ := integrableOn_and_integral_eq F S f φ hf L hLS hL hφ
    exact ⟨h1, by rw [h2, Complex.ofReal_one, one_mul]⟩
  measurableSet L _ _ := (isOpen_unitIdelesOutside F _).measurableSet

end NumberField.Idele