记录一道Lean练习题，主要涉及$p$-adic的东西。通过这题主要是学一下无穷乘积（tprod），Finset的attach和map。

---

数学背景

先说一下$\mathbb{Q}$上的$p$-adic Norm的定义：给定一个有理数$x$和素数$p$，我们总可以把$x$写成$p^k \cdot \frac{m}{n}$，使得$k$为整数并且$m$和$n$都是不能再被$p$整除的整数（就是把$x$里面的$p$提干净），然后我们就把$x$的$p$进范数$|x|_p$定义为$p^{-k}$。特殊地，我们一般令$|0|_p = 0$。与实数中“距离原点越远数值越大”不同，$p$进范数衡量的是数被$p$整除的“次数”。$x$被$p$整除的次数越多（就是$k$越大），$|x|_p$就越小。很明显$|x|_p$总是等于$|-x|_p$，所以我们总是考虑正的$x$（或者说$|x|$）。

对这题，我们可以先把$|x|$写成$\frac{m}{n}$，然后对$m$和$n$分别做素因数分解得到

$$ |x|=\frac{m}{n}=\frac{\prod_i p_i^{a_i}}{\prod_i p_i^{b_i}} = \prod_i p_i^{a_i - b_1} $$

$\{p_i\}$是$m$和$n$的素因子之集的并集。因此，

$$ |x|_{p_i} = p_i^{- a_i + b_i} $$

而对于不属于$\{p_i\}$的素数$r$（也就是和$m$和$n$都互质的），$|x|_r = 1$。

所以，

$$ \prod_{p \text { prime }}|x|_{p} = \prod_{i} |x|_{p_i} \\ = \prod_i p_i^{- a_i + b_i} = \frac{\prod_i p_i^{b_i}}{\prod_i p_i^{a_i}} = \frac{n}{m} = |x|^{-1} $$

这样就证完了。

---

Lean准备

有理数

variable (x : ℚ)
#check x.den --分母，ℕ
#check x.num --分子，ℤ
#check x.num.natAbs --分子绝对值，ℕ

素数

variable (p : ℕ)
#check p.Prime -- p是素数，Prop

-- The type of prime numbers
def Primes :=
  { p : ℕ // p.Prime }
  deriving DecidableEq

-- `primesBelow n` is the set of primes less than `n` as a `Finset`.
def primesBelow (n : ℕ) : Finset ℕ := (Finset.range n).filter (fun p ↦ p.Prime)

#check Nat.Prime
#check Nat.Primes
#check Nat.primesBelow

#check Nat.prod_pow_prime_padicValNat -- 素因数分解，分解成p ^ padicValNat p n的乘积

#check Finset.mem_filter -- 用来取出上面filter的性质（p.Prime）
#check Finset.mem_range -- 用来取出p < n

p-adic

-- If `q ≠ 0`, the `p`-adic norm of a rational `q` is `p ^ (-padicValRat p q)`.
-- If `q = 0`, the `p`-adic norm of `q` is `0`.
def padicNorm (p : ℕ) (q : ℚ) : ℚ :=
  if q = 0 then 0 else (p : ℚ) ^ (-padicValRat p q)

--`padicValRat` defines the valuation of a rational `q` to be the valuation of `q.num` minus the
-- valuation of `q.den`. If `q = 0` or `p = 1`, then `padicValRat p q` defaults to `0`.
def padicValRat (p : ℕ) (q : ℚ) : ℤ :=
  padicValInt p q.num - padicValNat p q.den

-- For `p ≠ 1`, the `p`-adic valuation of an integer `z ≠ 0` is the largest natural number `k` such
-- that `p^k` divides `z`. If `x = 0` or `p = 1`, then `padicValInt p q` defaults to `0`.
def padicValInt (p : ℕ) (z : ℤ) : ℕ :=
  padicValNat p z.natAbs

-- padicValNat (p : ℕ) (n : ℕ) 就是求p在n中的次数，
#eval padicValNat 2 4 -- 2
#eval padicValNat 2 5 -- 0
-- padicValInt (p : ℕ) (z : ℤ) 就是z的绝对值的padicValNat
#eval padicValInt 2 (- 4) -- 2
-- padicValRat (p : ℕ) (q : ℚ) 就是把有理数里p的次数提出来
#eval padicValRat 2 (4 / 3) -- 2
-- padicNorm (p : ℕ) (q : ℚ) 就是前面定义的p进范数
#eval padicNorm 2 (4 / 3) -- 1 / 4

连乘号

-- `∏ x ∈ s, f x` is the product of `f x` as `x` ranges over the elements of the finite set `s`.
-- When the index type is a `Fintype`, the notation `∏ x, f x`, is a shorthand for
-- `∏ x ∈ Finset.univ, f x`.
#check Finset.prod

-- -  ∑\∏ x, f x                -- x's type should be a Fintype
-- -  ∑\∏ x ∈ s, f x            -- s should be a Finset
-- -  ∑\∏ x ∈ s with p x, f x   -- p is some property for ele in s

-- `∏' i, f i` is the product of `f` if it exists and is unconditionally convergent,
-- or 1 otherwise.
#check tprod

-- `Multipliable f` means that `f` has some (infinite) product. Use `tprod` to get the value.
#check Multipliable -- ∃ a, HasProd f a

-- `HasProd f a` means that the (potentially infinite) product of the `f b` for `b : β` 
-- converges to `a`.
#check HasProd

-- `mulSupport` of a function is the set of points `x` such that `f x ≠ 1`.
#check Function.mulSupport

-- 要写（有定义的）无穷乘积，首先要说明`Multipliable`，也就是可乘，一般也就是乘积收敛。
-- 最好还可以再说明乘性支集`Function.mulSupport`是有限的，也即乘积项几乎都为1，只有有限项不为1，
-- 这样就可以把无穷乘积限制成在有限支集上的有限乘积`finprod`。
-- 但是`finprod`还不是我们最想要的`Finset.prod`
-- ↓ 把`finprod`转换成乘性支集（的超集）上的`Finset.prod`
#check finprod_eq_finset_prod_of_mulSupport_subset

---

开写~

首先我们从Finset的prod出发。精确地说，$\prod_{p \text { prime }}|x|_{p}$的乘性支集是x.den和x.num.natAbs的素因子集之并（ℚ要求分子分母互质，所以支集恰好是...之并），即

$$ \prod_{p \text { prime }}|x|_{p} = \prod_{p \in \text{prime factors of x.den or x.num.natAbs}}|x|_p $$

但是我感觉写什么什么的素因子集之并比较麻烦，我们直接粗放地说，对足够大的$m$（只要比x.den和x.num.natAbs都大），$|x|_p = 1, \forall p > m$。因此有

$$ \prod_{p \text { prime }}|x|_{p} = \prod_{p < \text{max(x.den,x.num.natAbs)}}|x|_p $$

第一个lemma

所以我们写出我们要证的第一个定理：对于足够大的$m, \ \prod_{p < m} p^{\text{padicValRat p x}} = |x|$（基本上就是有理数版的素数分解）

import Mathlib

variable {x : ℚ} (h : x ≠ 0)

include h in
lemma prod_pow_prime_padicValRat : ∀ m, x.den < m ∧ x.num.natAbs < m →
    ∏ p ∈ Finset.filter Nat.Prime (Finset.range m),
      (p : ℚ) ^ padicValRat p x = |x| := sorry

首先用自然数的分解把x.den和x.num.natAbs拆开：（x.den不为0因为分母不为零，x.num.natAbs不为0因为x非零）

  intro m ⟨hden, hnum⟩
  have prod1 := Nat.prod_pow_prime_padicValNat x.den x.den_nz m hden
  have prod2 := Nat.prod_pow_prime_padicValNat x.num.natAbs
    (Int.natAbs_ne_zero.2 ((x.num_ne_zero).2 h)) m hnum

然后把两个分解相除得到：（用Finset.prod_div_distrib）

  have eq1 : ∏ p ∈ Finset.filter Nat.Prime (Finset.range m),
    (p ^ padicValNat p x.num.natAbs : ℚ) / (p ^ padicValNat p x.den : ℚ) =
      x.num.natAbs / x.den := by
    nth_rw 2 [← prod1, ← prod2]
    simp only [Finset.prod_div_distrib, Nat.cast_prod, Nat.cast_pow]

再把(p ^ padicValNat p x.num.natAbs : ℚ) / (p ^ padicValNat p x.den : ℚ)转成(p : ℚ) ^ padicValRat p x，有

have eq2 : ∏ p ∈ Finset.filter Nat.Prime (Finset.range m),
      (p : ℚ) ^ padicValRat p x = x.num.natAbs / x.den := sorry

这个转换理应是显然的，但是有很多zpow和pow的转换问题，首先我们证明两个连乘相等可以用Finset.prod_congr转成逐项相等，然后写一个lemma去证逐项相等：

lemma Rat.pow_padiv {p : ℕ} (hp : p ≠ 0) :
  (p : ℚ) ^ padicValRat p x =
    (p : ℚ) ^ padicValNat p x.num.natAbs / (p : ℚ) ^ padicValNat p x.den := by
  have : ((p : ℚ) ^ padicValRat p x) * (p : ℚ) ^ padicValNat p x.den =
      (p : ℚ) ^ padicValNat p x.num.natAbs := by
    unfold padicValRat padicValInt
    calc
      _ = (p : ℚ) ^ (((padicValNat p x.num.natAbs) : ℤ) - ((padicValNat p x.den) : ℤ) +
      (padicValNat p x.den : ℤ)) := by
        rw [zpow_add', zpow_natCast]
        refine Or.intro_left _ (Nat.cast_ne_zero.2 hp)
      _ = _ := by
        rw [sub_add_cancel, zpow_natCast]
  rw [← this, ← mul_div, div_self, mul_one]
  simp only [ne_eq, pow_eq_zero_iff', Nat.cast_eq_zero, hp,
    padicValNat.eq_zero_iff, Rat.den_ne_zero, false_or, not_or, Decidable.not_not,
    false_and, not_false_eq_true]

  have eq2 : ∏ p ∈ Finset.filter Nat.Prime (Finset.range m),
      (p : ℚ) ^ padicValRat p x = x.num.natAbs / x.den := by
    rw [← eq1]
    refine Finset.prod_congr rfl ?_
    simp only [Finset.mem_filter, Finset.mem_range, and_imp]
    exact fun p hp₁ hp₂ ↦ Rat.pow_padiv (Nat.Prime.ne_zero hp₂)

之后我们把x.num.natAbs / x.den转换回|x|就行了：

  have eq3 : |x| = x.num.natAbs / x.den := by
    rw [Rat.abs_def, (Rat.natCast_div_eq_divInt x.num.natAbs x.den).symm]
  rwa [← eq3] at eq2

贴一个着色比较好的codesnap（lean的highlight.js在干什么(￣ ‘i ￣;)）：

第二个lemma

然后我们取倒数就可以得到p-adic Norm的乘积：对于足够大的$m, \ \prod_{p < m} |x|_p = |x|^{-1}$

include h in
lemma prod_prime_padicNorm : ∀ m, x.den < m ∧ x.num.natAbs < m →
    ∏ p ∈ Finset.filter Nat.Prime (Finset.range m), padicNorm p x = |x|⁻¹ := by
  simp only [padicNorm, h, ↓reduceIte, zpow_neg, Finset.prod_inv_distrib, inv_inj]
  exact prod_pow_prime_padicValRat h

从数学上，这就是$\prod_{p \text{prime}} |x|_p$的部分乘积，所以接下来我们只需要“令$m$趋于无穷大”就行了，我们可以再明确地指出对足够大的$p$，$|x|_p = 1$：

include h in
lemma padicNorm_ne_one {m : ℕ} (hm : m ≠ 1) : x.den < m ∧ x.num.natAbs < m →
    padicNorm m x = 1 := by
  intro hp'
  simp only [padicNorm, h, ↓reduceIte, zpow_neg, inv_eq_one, padicValRat]
  rw [zpow_eq_one_iff_right₀ m.cast_nonneg' (Nat.cast_ne_one.2 hm), sub_eq_zero]
  congr
  have ndvd1 : ¬↑m ∣ x.num := by
    convert_to ¬↑m ∣ x.num.natAbs
    exact Int.ofNat_dvd_left
    exact Nat.not_dvd_of_pos_of_lt (Int.natAbs_pos.2 (Rat.num_ne_zero.2 h)) hp'.2
  have ndvd2 : ¬m ∣ x.den := Nat.not_dvd_of_pos_of_lt x.den_pos hp'.1
  rw [padicValInt.eq_zero_of_not_dvd ndvd1, padicValNat.eq_zero_of_not_dvd ndvd2]

这段没什么要解释的，多用congr和convert_to可以增强书写体验（

构造Finset Nat.Primes

我们最后要写的是∏' p : Nat.Primes, padicNorm p x = |x|⁻¹，在证明这个padicNorm · x的Multipliable时，我们会需要一个Finset Nat.Primes。这里其实卡了我很久因为我至今没太看懂Finset怎么构造的（似乎是要一个Multiset，但是Multiset是List的一个Quotient？）

长话短说，我们要的是所有小于$m$的素数组成的Finset Nat.Primes，而Nat.primesBelow是一个Finset ℕ。但是我们可以用Finset.attach把(Nat.primesBelow m : Finset ℕ)转换成Finset { x // x ∈ m.primesBelow }，然后再用Finset.map（通过一个嵌入）打到Finset Nat.Primes。如下：

def Primes.below (m : ℕ) : Finset Nat.Primes :=
  let inj_fun : { x // x ∈ m.primesBelow } ↪ Nat.Primes := {
    toFun := fun x ↦ ⟨x.val, Nat.prime_of_mem_primesBelow x.property⟩
    inj' := fun _ _ h12 ↦ let_fun this := Subtype.val_inj.mpr h12; Subtype.eq this
  }
  --           ↓ attach                                 ↓ map
  -- Finset ℕ → Finset { x : ℕ // x ∈ m.primesBelow } → Finset Nat.Primes
  (Nat.primesBelow m).attach.map inj_fun

一些杂项

这些定理都是为了描述前面定义的Primes.below的性质的：

lemma Primes.below_not_mem_le {m : ℕ} {p : Nat.Primes} : p ∉ (Primes.below m) → m ≤ p := by
  contrapose!
  refine fun hpm ↦ Finset.mem_map.2
    ⟨⟨p.val, Nat.mem_primesBelow.2 ⟨hpm, p.property⟩⟩, ?_⟩
  simp only [Finset.mem_attach, Function.Embedding.coeFn_mk, Subtype.coe_eta, and_self]

lemma Primes.below_mem_lt {m : ℕ} {p : Nat.Primes} : p ∈ (Primes.below m) → p < m := by
  intro hpa
  obtain ⟨q, ⟨hq1, hq2⟩⟩ := Finset.mem_map.1 hpa
  suffices q < m from lt_of_eq_of_lt (congrArg Subtype.val hq2.symm) this
  exact (Nat.mem_primesBelow.1 q.2).1

lemma Primes.below_prime_mem_iff {m : ℕ} {p : Nat.Primes} :
    p ∈ (Primes.below m) ↔ p < m := by
  constructor
  · exact Primes.below_mem_lt
  · contrapose!; exact Primes.below_not_mem_le

include h

lemma Primes.below_not_mem_padicNorm {m : ℕ} {p : Nat.Primes}
    (hm : x.den < m ∧ x.num.natAbs < m) : p ∉ (Primes.below m) → padicNorm p x = 1 := by
  intro hp
  replace hp : m ≤ p := Primes.below_not_mem_le hp
  exact padicNorm_ne_one h p.property.ne_one ⟨(LE.le.trans hm.1 hp), LE.le.trans hm.2 hp⟩

注意一下Finset.mem_map，其它的应该没有什么需要说明的。

Primes.below上的prod

然后我们就可以把之前在Nat.primesBelow上的Finset.prod换成在Primes.below上的了：

lemma prod_primesBelow_padic {m : ℕ} (hm : x.den < m ∧ x.num.natAbs < m) :
    ∏ p ∈ (Primes.below m), padicNorm p x = |x|⁻¹ := by
  rw [← prod_prime_padicNorm h m hm]
  refine Finset.prod_bij ?_ ?_ ?_ ?_ ?_ (α := ℚ)
  · exact fun p _ ↦ p.val
  · exact fun p hp ↦
      Finset.mem_filter.2 ⟨Finset.mem_range.2 <| Primes.below_mem_lt hp, p.property⟩
  · exact fun a₁ _ a₂ _ h12 ↦ (Nat.Primes.coe_nat_inj a₁ a₂).mp h12
  · intro b hb
    have := Finset.mem_filter.1 hb
    exact ⟨⟨b, this.2⟩, ⟨Primes.below_prime_mem_iff.2 (Finset.mem_range.1 this.1), rfl⟩⟩
  · exact fun _ _ ↦ rfl

注意证明两个连乘相等还可以用Finset.prod_bij（实际上就是重新排序）

Last Kick

我们现在可以向final goal进发了（

为此有两个需要的事情：

1. Multipliable fun (p : Nat.Primes) ↦ padicNorm p x和
2. (Function.mulSupport fun (p : Nat.Primes) ↦ padicNorm p x).Finite，
   也即无穷乘积收敛和乘性支集有限。

Multipliable

lemma multipliable_padicNorm : Multipliable fun (p : Nat.Primes) ↦ padicNorm p x := by
  sorry

起手先把Multipliable, HasProd, nhds都simp掉，这时的goal就会变成：

⊢ ∃ a, ∀ (i : Set ℚ), a ∈ i → IsOpen i → ∃ a, ∀ (b : Finset Nat.Primes), a ⊆ b → ∏ x_1 ∈ b, padicNorm (↑x_1) x ∈ i

其中第一个a是ℚ，第二个是Finset Nat.Primes，那这个定义和我们熟悉的极限的定义就一样了。从前面可以知道，这个乘积的极限应该就是|x|⁻¹。所以

  refine ⟨|x|⁻¹, fun i i_one i_open ↦ ?_⟩

把第一个a取成|x|⁻¹。那么前面也证明了对比x.den和x.num.natAbs都大的m，连乘的值都是|x|⁻¹，所以我们先取出这样的m，

  obtain ⟨m , ⟨hden, hnum⟩⟩ := exists_ge_of_linear x.den.succ x.num.natAbs.succ

第二个a我们就取成(Primes.below m)，

  refine ⟨(Primes.below m), fun b hab ↦ ?_⟩

此时的goal为

⊢ ∏ x_1 ∈ b, padicNorm (↑x_1) x ∈ i

也即是说这个乘积在|x|⁻¹的开邻域里，那我只要说明这个乘积等于|x|⁻¹就好了

  suffices ∏ p ∈ b, padicNorm p x = |x|⁻¹ from this.symm ▸ i_one

随后我们把b拆成(Primes.below m) ∪ (b \ (Primes.below m))，这样对于在前一半里的p，这个乘积就是|x|⁻¹

  have : b = (Primes.below m) ∪ (b \ (Primes.below m)) :=
    (Finset.union_sdiff_of_subset hab).symm
  rw [this, Finset.prod_union, prod_primesBelow_padic h ⟨hden, hnum⟩]
  suffices ∏ p ∈ b \ (Primes.below m), padicNorm p x = 1 from by
    rw [this, mul_one]

那最后只需要说明对于后一半里的p这个乘积就是1就行了

  refine Finset.prod_eq_one fun p hp ↦ ?_
  exact Primes.below_not_mem_padicNorm h ⟨hden, hnum⟩ (Finset.mem_sdiff.1 hp).2
  exact Finset.disjoint_sdiff

Finsupport

lemma finsupport_padicNorm :
    (Function.mulSupport fun (p : Nat.Primes) ↦ padicNorm p x).Finite := by
  sorry

这个乘性支集是有限的，因为它是Primes.below的子集，也就是这个支集中的素数肯定小于某个m。还是一样的我们先取出比x.den和x.num.natAbs都大的数m，然后，

  refine Set.Finite.subset (Primes.below m).finite_toSet
    <| Function.mulSupport_subset_iff.2 fun p ↦ ?_
  contrapose!
  exact Primes.below_not_mem_padicNorm h hm

Final Goal

最后的目标就近在咫尺了

lemma tprod_prime_padicNorm : ∏' p : Nat.Primes, padicNorm p x = |x|⁻¹ := by
  sorry

取出m，tprod_def展开，用multipliable_padicNorm h和finsupport_padicNorm h把ite(if...then...else...)和dite(if h : ... then...else...)都simp掉

  obtain ⟨m , hm⟩ := exists_ge_of_linear x.den.succ x.num.natAbs.succ
  simp only [tprod_def, multipliable_padicNorm h, ↓reduceDIte, finsupport_padicNorm h,
    ↓reduceIte, ← prod_primesBelow_padic h hm]

这里的goal会变成

⊢ ∏ᶠ (p : Nat.Primes), padicNorm (↑p) x = ∏ p ∈ Primes.below m, padicNorm (↑p) x

那证明一个finprod和Finset.prod相等，我们可以用finprod_eq_finset_prod_of_mulSupport_subset，也就是把finprod换成在Function.mulSupport的超集上的Finset.prod。这里我们refine一下

  refine finprod_eq_finset_prod_of_mulSupport_subset
    (fun (p : Nat.Primes) ↦ padicNorm p x) ?_

然后就只用证明

⊢ (Function.mulSupport fun p ↦ padicNorm (↑p) x) ⊆ ↑(Primes.below m)

然而这就很显然了

  simp only [Function.mulSupport_subset_iff, ne_eq, Finset.mem_coe]
  intro p hp
  by_contra hpa
  exact hp <| Primes.below_not_mem_padicNorm h hm hpa

---

总结

先贴一张由Gemini注释的总的代码：

import Mathlib

/-
Let $0 \neq x \in \mathbb{Q}$. Show that $|x| \prod_{p \text { prime }}|x|_{p}=1$. (First show that $|x|_{p}=1$ for almost all primes $p$. )
-/

variable {x : ℚ} (h : x ≠ 0)

/--$(p : \mathbb{Q})^{\text{padicValRat } p x} = \frac{(p : \mathbb{Q})^{\text{padicValNat } p |x.num|}}{(p : \mathbb{Q})^{\text{padicValNat } p x.den}}$.-/
lemma Rat.pow_padiv {p : ℕ} (hp : p ≠ 0) :
  (p : ℚ) ^ padicValRat p x =
    (p : ℚ) ^ padicValNat p x.num.natAbs / (p : ℚ) ^ padicValNat p x.den := by
  have : ((p : ℚ) ^ padicValRat p x) * (p : ℚ) ^ padicValNat p x.den =
      (p : ℚ) ^ padicValNat p x.num.natAbs := by
    -- Start with the definition of p-adic valuation for rationals: $\text{padicValRat } p x = \text{padicValInt } p x = \text{padicValNat } p |x.num| - \text{padicValNat } p x.den$.
    unfold padicValRat padicValInt
    calc
      -- Substitute the definition into the exponent: $(p : \mathbb{Q})^{(\text{padicValNat } p |x.num| - \text{padicValNat } p x.den)} \cdot (p : \mathbb{Q})^{\text{padicValNat } p x.den}$.
      _ = (p : ℚ) ^ (((padicValNat p x.num.natAbs) : ℤ) - ((padicValNat p x.den) : ℤ) +
      (padicValNat p x.den : ℤ)) := by
        -- Apply the exponent rule $a^{b+c} = a^b \cdot a^c$ in reverse, $a^{u-v} \cdot a^v = a^{(u-v)+v} = a^u$.
        rw [zpow_add', zpow_natCast]
        -- Ensure the base $(p : \mathbb{Q}) \neq 0$ for the power rule, which is true as $p \neq 0$.
        refine Or.intro_left _ (Nat.cast_ne_zero.2 hp)
      -- Simplify the exponent by canceling $-(\text{padicValNat } p x.den) + (\text{padicValNat } p x.den)$.
      _ = _ := by
        -- Apply basic arithmetic to simplify the exponent: $(u-v)+v = u$.
        rw [sub_add_cancel, zpow_natCast]
  -- Divide both sides of the equation by $(p : \mathbb{Q})^{\text{padicValNat } p x.den}$ to isolate $(p : \mathbb{Q})^{\text{padicValRat } p x}$.
  rw [← this, ← mul_div, div_self, mul_one]
  -- Simplify the resulting expression by canceling the common term and using $a/a = 1$ and $1 \cdot b = b$.
  simp only [ne_eq, pow_eq_zero_iff', Nat.cast_eq_zero, hp,
    padicValNat.eq_zero_iff, Rat.den_ne_zero, false_or, not_or, Decidable.not_not,
    false_and, not_false_eq_true]

include h in
/--The product of $(p : \mathbb{Q})^{\text{padicValRat } p x}$ for primes $p < m$ yields $|x|$ for sufficiently large $m$. -/
lemma prod_pow_prime_padicValRat : ∀ m, x.den < m ∧ x.num.natAbs < m →
    ∏ p ∈ Finset.filter Nat.Prime (Finset.range m),
      (p : ℚ) ^ padicValRat p x = |x| := by
  intro m ⟨hden, hnum⟩
  -- Use the prime factorization of the denominator: $x.den = \prod_{p< m, p \text{ prime}} p^{\text{padicValNat } p x.den}$.
  have prod1 := Nat.prod_pow_prime_padicValNat x.den x.den_nz m hden
  -- Use the prime factorization of the numerator's absolute value: $|x.num| = \prod_{p< m, p \text{ prime}} p^{\text{padicValNat } p |x.num|}$.
  have prod2 := Nat.prod_pow_prime_padicValNat x.num.natAbs
    (Int.natAbs_ne_zero.2 ((x.num_ne_zero).2 h)) m hnum
  -- Express the ratio of numerator and denominator factorizations as a product of ratios.
  have eq1 : ∏ p ∈ Finset.filter Nat.Prime (Finset.range m),
    (p ^ padicValNat p x.num.natAbs : ℚ) / (p ^ padicValNat p x.den : ℚ) =
      x.num.natAbs / x.den := by
    -- Substitute the prime factorizations into the ratio $x.num.natAbs / x.den$.
    nth_rw 2 [← prod1, ← prod2]
    -- Distribute the division over the product: $\frac{\prod a_i}{\prod b_i} = \prod \frac{a_i}{b_i}$.
    simp only [Finset.prod_div_distrib, Nat.cast_prod, Nat.cast_pow]
  -- Relate the product of $(p : \mathbb{Q})^{\text{padicValRat } p x}$ to the ratio $x.num.natAbs / x.den$.
  have eq2 : ∏ p ∈ Finset.filter Nat.Prime (Finset.range m),
      (p : ℚ) ^ padicValRat p x = x.num.natAbs / x.den := by
    -- Replace the product of ratios with the product of powers using the previous lemma.
    rw [← eq1]
    -- Show term-wise equality inside the product using the lemma `Rat.pow_padiv`.
    refine Finset.prod_congr rfl ?_
    simp only [Finset.mem_filter, Finset.mem_range, and_imp]
    -- Apply `Rat.pow_padiv` to each term in the product, using the fact that $p$ is prime hence $p \neq 0$.
    exact fun p hp₁ hp₂ ↦ Rat.pow_padiv (Nat.Prime.ne_zero hp₂)
  -- Use the definition of the absolute value of a rational number: $|x| = \frac{|x.num|}{|x.den|} = \frac{x.num.natAbs}{x.den}$.
  have eq3 : |x| = x.num.natAbs / x.den := by
    rw [Rat.abs_def, (Rat.natCast_div_eq_divInt x.num.natAbs x.den).symm]
  -- Replace $x.num.natAbs / x.den$ with $|x|$ in the equation to obtain the desired approximation.
  rwa [← eq3] at eq2

include h in
/--The product of $|x|_p$ for primes $p < m$ yields $|x|^{-1}$ for sufficiently large $m$. -/
lemma prod_prime_padicNorm : ∀ m, x.den < m ∧ x.num.natAbs < m →
    ∏ p ∈ Finset.filter Nat.Prime (Finset.range m), padicNorm p x = |x|⁻¹ := by
  -- Rewrite the product using the definition of p-adic norm: $|x|_p = p^{-\text{padicValRat } p x} = (p^{\text{padicValRat } p x})^{-1}$.
  simp only [padicNorm, h, ↓reduceIte, zpow_neg, Finset.prod_inv_distrib, inv_inj]
  -- After simplification, the goal is equivalent to the previous lemma `prod_pow_prime_padicValRat h`.
  exact prod_pow_prime_padicValRat h

include h in
/--If $m$ is coprime to both numerator and denominator (implied by $m > \max(|x.num|, x.den)$ and $m \neq 1$), then $|x|_m = 1$.-/
lemma padicNorm_ne_one {m : ℕ} (hm : m ≠ 1) : x.den < m ∧ x.num.natAbs < m →
    padicNorm m x = 1 := by
  intro hp'
  simp only [padicNorm, h, ↓reduceIte, zpow_neg, inv_eq_one, padicValRat]
  -- $|x|_m = 1 \iff |(m : \mathbb{Q})^{-\text{padicValRat } m x}| = 1 \iff (m : \mathbb{Q})^{-\text{padicValRat } m x} = \pm 1$. Since norm is non-negative, it means $(m : \mathbb{Q})^{-\text{padicValRat } m x} = 1$.
  -- This is equivalent to $-\text{padicValRat } m x = 0 \iff \text{padicValRat } m x = 0 \iff \text{padicValNat } m |x.num| - \text{padicValNat } m x.den = 0$.
  rw [zpow_eq_one_iff_right₀ m.cast_nonneg' (Nat.cast_ne_one.2 hm), sub_eq_zero]
  -- We need to show $\text{padicValNat } m |x.num| = \text{padicValNat } m x.den$.
  congr
  -- If $m > |x.num|$, then $m \nmid x.num$, hence $\text{padicValNat } m |x.num| = 0$.
  have ndvd1 : ¬↑m ∣ x.num := by
    convert_to ¬↑m ∣ x.num.natAbs
    exact Int.ofNat_dvd_left
    exact Nat.not_dvd_of_pos_of_lt (Int.natAbs_pos.2 (Rat.num_ne_zero.2 h)) hp'.2
  -- If $m > x.den$, then $m \nmid x.den$, hence $\text{padicValNat } m x.den = 0$.
  have ndvd2 : ¬m ∣ x.den := Nat.not_dvd_of_pos_of_lt x.den_pos hp'.1
  -- If $m \nmid x.num$ and $m \nmid x.den$, then both valuations are 0.
  rw [padicValInt.eq_zero_of_not_dvd ndvd1, padicValNat.eq_zero_of_not_dvd ndvd2]

/--Define a finset containing all prime numbers less than $m$.-/
def Primes.below (m : ℕ) : Finset Nat.Primes :=
  -- This definition constructs a finset of `Nat.Primes` from `Nat.primesBelow m` (primes below m as natural numbers).
  let inj_fun : { x // x ∈ m.primesBelow } ↪ Nat.Primes := {
    toFun := fun x ↦ ⟨x.val, Nat.prime_of_mem_primesBelow x.property⟩
    inj' := fun _ _ h12 ↦ let_fun this := Subtype.val_inj.mpr h12; Subtype.eq this
  }
  (Nat.primesBelow m).attach.map inj_fun

/--If a prime $p$ is not in $\text{Primes.below } m$, it means $p \ge m$.-/
lemma Primes.below_not_mem_le {m : ℕ} {p : Nat.Primes} : p ∉ (Primes.below m) → m ≤ p := by
  contrapose!
  -- Prove the contrapositive: $p < m \implies p \in \text{Primes.below } m$.
  refine fun hpm ↦ Finset.mem_map.2
    ⟨⟨p.val, Nat.mem_primesBelow.2 ⟨hpm, p.property⟩⟩, ?_⟩
  simp only [Finset.mem_attach, Function.Embedding.coeFn_mk, Subtype.coe_eta, and_self]
  -- This follows directly from the definition of `Primes.below` and `Nat.primesBelow`.

/--If a prime $p$ is in $\text{Primes.below } m$, it means $p < m$.-/
lemma Primes.below_mem_lt {m : ℕ} {p : Nat.Primes} : p ∈ (Primes.below m) → p < m := by
  intro hpa
  obtain ⟨q, ⟨hq1, hq2⟩⟩ := Finset.mem_map.1 hpa
  suffices q < m from lt_of_eq_of_lt (congrArg Subtype.val hq2.symm) this
  exact (Nat.mem_primesBelow.1 q.2).1
  -- This also follows directly from the definition of `Primes.below` and `Nat.primesBelow`.

/--Equivalence: $p \in \text{Primes.below } m$ if and only if $p < m$.-/
lemma Primes.below_prime_mem_iff {m : ℕ} {p : Nat.Primes} :
    p ∈ (Primes.below m) ↔ p < m := by
  -- Prove both directions of the equivalence.
  constructor
  · exact Primes.below_mem_lt -- $p \in \text{Primes.below } m \implies p < m$.
  · contrapose!; exact Primes.below_not_mem_le -- $p < m \implies p \in \text{Primes.below } m$ (by contrapositive).

include h

/--If $p \ge m$ and $m > \max(|x.den|, |x.num.natAbs|)$, then $|x|_p = 1$.-/
lemma Primes.below_not_mem_padicNorm {m : ℕ} {p : Nat.Primes}
    (hm : x.den < m ∧ x.num.natAbs < m) : p ∉ (Primes.below m) → padicNorm p x = 1 := by
  intro hp
  replace hp : m ≤ p := Primes.below_not_mem_le hp
  exact padicNorm_ne_one h p.property.ne_one ⟨(LE.le.trans hm.1 hp), LE.le.trans hm.2 hp⟩
  -- Combine `Primes.below_not_mem_le` and `padicNorm_ne_one` to show $|x|_p = 1$ for primes outside `Primes.below m`.

/--The product of $|x|_p$ throughout $\text{Primes.below } m$ is $|x|^{-1}$-/
lemma prod_primesBelow_padic {m : ℕ} (hm : x.den < m ∧ x.num.natAbs < m) :
    ∏ p ∈ (Primes.below m), padicNorm p x = |x|⁻¹ := by
  -- Rewrite the product over primes in $\text{Primes.below } m$ in terms of $|x|^{-1}$.
  rw [← prod_prime_padicNorm h m hm]
  -- We need to show that the product over `Primes.below m` is the same as the product over `Finset.filter Nat.Prime (Finset.range m)`.
  refine Finset.prod_bij ?_ ?_ ?_ ?_ ?_ (α := ℚ)
  -- Construct a bijection between `Primes.below m` and `Finset.filter Nat.Prime (Finset.range m)`.
  · exact fun p _ ↦ p.val -- Function: `Nat.Primes` -> `ℕ`, map prime structure to natural number value.
  · exact fun p hp ↦
      Finset.mem_filter.2 ⟨Finset.mem_range.2 <| Primes.below_mem_lt hp, p.property⟩
      -- Show that if $p \in \text{Primes.below } m$, then $p.val \in \text{Finset.filter Nat.Prime (Finset.range m)}$.
      -- $p \in \text{Primes.below } m \implies p < m \implies p.val < m \implies p.val \in \text{Finset.range } m$. Also $p.val$ is prime by definition of `Nat.Primes`.
  · exact fun a₁ _ a₂ _ h12 ↦ (Nat.Primes.coe_nat_inj a₁ a₂).mp h12
    -- Injectivity of the map: if $p_1.val = p_2.val$, then $p_1 = p_2$ for $p_1, p_2 \in \text{Primes.below } m$.
  · intro b hb
    have := Finset.mem_filter.1 hb
    exact ⟨⟨b, this.2⟩, ⟨Primes.below_prime_mem_iff.2 (Finset.mem_range.1 this.1), rfl⟩⟩
    -- Surjectivity: for each $b \in \text{Finset.filter Nat.Prime (Finset.range m)}$, there exists $p \in \text{Primes.below } m$ such that $p.val = b$.
    -- If $b \in \text{Finset.filter Nat.Prime (Finset.range m)}$, then $b$ is prime and $b < m$. So $b \in \text{Nat.primesBelow } m$. We can construct $p = \langle b, \text{prime proof}\rangle \in \text{Primes.below } m$.
  · exact fun _ _ ↦ rfl -- Map preserves the value: $\text{padicNorm } p x = \text{padicNorm } (p.val) x$.

/--The infinite product $\prod_{p} |x|_p$ converges.-/
lemma multipliable_padicNorm : Multipliable fun (p : Nat.Primes) ↦ padicNorm p x := by
  simp only [Multipliable, HasProd, nhds, Set.mem_setOf_eq, Filter.tendsto_iInf,
    Filter.tendsto_principal, Filter.eventually_atTop, ge_iff_le, Finset.le_eq_subset, and_imp]
  -- Choose $m$ large enough such that $m > \max(|x.den|, |x.num.natAbs|)$.
  obtain ⟨m , ⟨hden, hnum⟩⟩ := exists_ge_of_linear x.den.succ x.num.natAbs.succ
  refine ⟨|x|⁻¹, fun i i_one i_open ↦ ?_⟩
  refine ⟨(Primes.below m), fun b hab ↦ ?_⟩
  suffices ∏ p ∈ b, padicNorm p x = |x|⁻¹ from this.symm ▸ i_one
  -- Split the product over a finite set $b$ into product over $\text{Primes.below } m$ and the remaining primes.
  have : b = (Primes.below m) ∪ (b \ (Primes.below m)) :=
    (Finset.union_sdiff_of_subset hab).symm
  rw [this, Finset.prod_union, prod_primesBelow_padic h ⟨hden, hnum⟩]
  -- For primes $p \in b \setminus \text{Primes.below } m$, we have $p \ge m$, so $|x|_p = 1$.
  suffices ∏ p ∈ b \ (Primes.below m), padicNorm p x = 1 from by
    rw [this, mul_one]
  refine Finset.prod_eq_one fun p hp ↦ ?_
  exact Primes.below_not_mem_padicNorm h ⟨hden, hnum⟩ (Finset.mem_sdiff.1 hp).2
  exact Finset.disjoint_sdiff
  -- The product over primes $p \ge m$ is 1 because $|x|_p = 1$ for such primes.

/--The set of primes $p$ where $|x|_p \neq 1$ is finite.-/
lemma finsupport_padicNorm :
    (Function.mulSupport fun (p : Nat.Primes) ↦ padicNorm p x).Finite := by
  -- Choose $m$ large enough such that $m > \max(|x.den|, |x.num.natAbs|)$.
  obtain ⟨m , hm⟩ := exists_ge_of_linear x.den.succ x.num.natAbs.succ
  -- The set of primes with $|x|_p \neq 1$ is a subset of $\text{Primes.below } m$, which is finite.
  refine Set.Finite.subset (Primes.below m).finite_toSet
    <| Function.mulSupport_subset_iff.2 fun p ↦ ?_
  contrapose!
  exact Primes.below_not_mem_padicNorm h hm

/--Prove the product formula: $\prod_{p \text{ prime }}|x|_{p} = |x|^{-1}$.-/
lemma tprod_prime_padicNorm : ∏' p : Nat.Primes, padicNorm p x = |x|⁻¹ := by
  -- Choose $m$ large enough such that $m > \max(|x.den|, |x.num.natAbs|)$.
  obtain ⟨m , hm⟩ := exists_ge_of_linear x.den.succ x.num.natAbs.succ
  simp only [tprod_def, multipliable_padicNorm h, ↓reduceDIte, finsupport_padicNorm h,
    ↓reduceIte, ← prod_primesBelow_padic h hm]
  -- Reduce the infinite product to a finite product over the finset `Primes.below m` because $|x|_p = 1$ outside this finset.
  refine finprod_eq_finset_prod_of_mulSupport_subset
    (fun (p : Nat.Primes) ↦ padicNorm p x) ?_
  simp only [Function.mulSupport_subset_iff, ne_eq, Finset.mem_coe]
  intro p hp
  by_contra hpa
  exact hp <| Primes.below_not_mem_padicNorm h hm hpa
  -- For $p \notin \text{Primes.below } m$, $|x|_p = 1$, so these terms do not affect the product.

总结一下，