-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
We :
  ∀ (z : (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) (r : ℝ) (hr : r > 0),
    ∃ (y : K),
      dist z
          ((algebraMap K ((v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) :
              (a : K) → (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ))
            y) <
        r
We₁ :
  ∀ (z : (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) (r : ℝ) (hr : r > 0) (a : (i : InfinitePlace K) → K)
    (hx :
      ∀ (i : InfinitePlace K),
        LT.lt (α := ℝ) (1 : ℝ) (((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (a i) : ℝ) ∧
          ∀ (j : InfinitePlace K), j ≠ i → LT.lt (α := ℝ) (((↑j : AbsoluteValue K ℝ) : (a : K) → ℝ) (a i) : ℝ) (1 : ℝ)),
    ∃ (y : K),
      dist z
          ((algebraMap K ((v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) :
              (a : K) → (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ))
            y) <
        r
We₂ :
  ∀ (z : (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) (r : ℝ) (hr : r > 0) (a : (i : InfinitePlace K) → K)
    (hx :
      ∀ (i : InfinitePlace K),
        LT.lt (α := ℝ) (1 : ℝ) (((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (a i) : ℝ) ∧
          ∀ (j : InfinitePlace K), j ≠ i → LT.lt (α := ℝ) (((↑j : AbsoluteValue K ℝ) : (a : K) → ℝ) (a i) : ℝ) (1 : ℝ)),
    ∃ (y : K),
      dist z
          ((algebraMap K ((v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) :
              (a : K) → (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ))
            y) <
        r
We₃ :
  ∀ (z : (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) (r : ℝ) (hr : r > 0) (a : (i : InfinitePlace K) → K)
    (hx :
      ∀ (i : InfinitePlace K),
        LT.lt (α := ℝ) (1 : ℝ) (((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (a i) : ℝ) ∧
          ∀ (j : InfinitePlace K), j ≠ i → LT.lt (α := ℝ) (((↑j : AbsoluteValue K ℝ) : (a : K) → ℝ) (a i) : ℝ) (1 : ℝ)),
    let y : (n : ℕ) → K := fun (n : ℕ) ↦
      ∑ v : InfinitePlace K,
        HMul.hMul (β := K) (1 / (1 + (a v)⁻¹ ^ n))
          ((WithAbs.equiv (↑v : AbsoluteValue K ℝ) : (a : WithAbs (↑v : AbsoluteValue K ℝ)) → K) (z v) : K);
    ∀
      (this :
        Tendsto
          (fun (n : ℕ) (v : InfinitePlace K) ↦
            ((WithAbs.equiv (↑v : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑v : AbsoluteValue K ℝ)) (y n))
          atTop (𝓝 z)),
      ∃ (y : K),
        dist z
            ((algebraMap K ((v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) :
                (a : K) → (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ))
              y) <
          r
We₄ :
  ∀ (z : (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) (r : ℝ) (hr : r > 0) (a : (i : InfinitePlace K) → K)
    (hx :
      ∀ (i : InfinitePlace K),
        LT.lt (α := ℝ) (1 : ℝ) (((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (a i) : ℝ) ∧
          ∀ (j : InfinitePlace K), j ≠ i → LT.lt (α := ℝ) (((↑j : AbsoluteValue K ℝ) : (a : K) → ℝ) (a i) : ℝ) (1 : ℝ)),
    let y : (n : ℕ) → K := fun (n : ℕ) ↦
      ∑ v : InfinitePlace K,
        HMul.hMul (β := K) (1 / (1 + (a v)⁻¹ ^ n))
          ((WithAbs.equiv (↑v : AbsoluteValue K ℝ) : (a : WithAbs (↑v : AbsoluteValue K ℝ)) → K) (z v) : K);
    ∀
      (this :
        Tendsto
          (fun (n : ℕ) (v : InfinitePlace K) ↦
            ((WithAbs.equiv (↑v : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑v : AbsoluteValue K ℝ)) (y n))
          atTop (𝓝 z))
      (N : ℕ)
      (h :
        ∀ n ≥ N,
          dist
              (fun (v : InfinitePlace K) ↦
                ((WithAbs.equiv (↑v : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑v : AbsoluteValue K ℝ)) (y n))
              z <
            r),
      ∃ (y : K),
        dist z
            ((algebraMap K ((v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) :
                (a : K) → (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ))
              y) <
          r
⊢ DenseRange (X := (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) (α := K)
    (⇑(algebraMap K ((v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ))) :
      (a : K) → (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ))

Tactic:
classical
  -- We have to show that given `(zᵥ)ᵥ` with `zᵥ : WithAbs v.1`, there is a `y : K` that is
  -- arbitrarily close to each `zᵥ` in `v`'s topology.
  refine Metric.denseRange_iff.mpr fun z r hr ↦ ?_
  -- Given `v`, by previous results we can select a `aᵥ : K` for each infinite place `v`
  -- such that `1 < v aᵥ` while `w aᵥ < 1` for all `w ≠ v`.
  choose a hx using AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv isNontrivial
    fun _ _ hwv ↦ (eq_iff_isEquiv (K := K)).not.mp hwv
  -- Define the sequence `yₙ = ∑ v, 1 / (1 + aᵥ⁻ⁿ) * zᵥ` in `K`
  let y := fun n ↦ ∑ v, (1 / (1 + (a v)⁻¹ ^ n)) * WithAbs.equiv v.1 (z v)
  -- We will show that this sequence converges to `z` in the product topology.
  have : atTop.Tendsto
      (fun n (v : InfinitePlace K) ↦ (WithAbs.equiv v.1).symm (y n)) (𝓝 z) := by
    -- At a fixed place `u`, the limit of `y` with respect to `u`'s topology is `zᵤ`.
    refine tendsto_pi_nhds.mpr fun u ↦ ?_
    simp_rw [← Fintype.sum_pi_single u z, y, map_sum, map_mul]
    refine tendsto_finsetSum _ fun w _ ↦ ?_
    by_cases hw : u = w
    · -- Because `1 / (1 + aᵤ⁻ⁿ) → 1` in `WithAbs u.1`.
      rw [← hw, Pi.single_eq_same]
      have : u (a u)⁻¹ < 1 := by simpa [← inv_pow, inv_lt_one_iff₀] using .inr (hx u).1
      simpa using (WithAbs.tendsto_one_div_one_add_pow_nhds_one this).mul_const (z u)
    · -- And `1 / (1 + aᵤ⁻ⁿ) → 0` in `WithAbs w.1` when `w ≠ u`.
      rw [Pi.single_eq_of_ne (M := fun v ↦ WithAbs v.1) hw (z w)]
      have hu : 1 < u (a w)⁻¹ := by simpa [one_lt_inv_iff₀] using
        ⟨u.pos_iff.2 fun ha ↦ by linarith [map_zero w ▸ ha ▸ (hx w).1], (hx w).2 u hw⟩
      have := u.1.tendsto_div_one_add_pow_nhds_zero hu
      simp_rw [← WithAbs.norm_toAbs_eq] at this
      simpa using (tendsto_zero_iff_norm_tendsto_zero.2 this).mul_const
        ((WithAbs.equiv u.1).symm (WithAbs.equiv w.1 (z w)))
  -- So taking a sufficiently large index of the sequence `yₙ` gives the desired term.
  let ⟨N, h⟩ := Metric.tendsto_atTop.1 this r hr
  exact ⟨y N, dist_comm z (algebraMap K _ (y N)) ▸ h N le_rfl⟩

Premises used: NumberField.InfinitePlace.isNontrivial, NumberField.InfinitePlace.eq_iff_isEquiv, Iff.mpr, Iff.not, AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv, Iff.mp, Metric.denseRange_iff