awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u : InfinitePlace K
refine :
  ∀ (w : InfinitePlace K),
    Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w →
      Tendsto (β := WithAbs (↑u : AbsoluteValue K ℝ))
        (fun (i : ℕ) ↦
          HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
            (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
                (1 / (1 + (a w)⁻¹ ^ i)) :
              WithAbs (↑u : AbsoluteValue K ℝ))
            (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
                ((WithAbs.equiv (↑w : AbsoluteValue K ℝ) : (a : WithAbs (↑w : AbsoluteValue K ℝ)) → K) (z w)) :
              WithAbs (↑u : AbsoluteValue K ℝ)))
        atTop
        (𝓝 (Pi.single (M := fun (i : InfinitePlace K) ↦ WithAbs (↑i : AbsoluteValue K ℝ)) w (z w) u) :
          Filter (WithAbs (↑u : AbsoluteValue K ℝ)))
⊢ Tendsto.{0, u_1} (β := WithAbs (↑u : AbsoluteValue K ℝ))
    (fun (i : ℕ) ↦
      ∑ x : InfinitePlace K,
        HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
          (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
              (1 / (1 + (a x)⁻¹ ^ i)) :
            WithAbs (↑u : AbsoluteValue K ℝ))
          (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
              ((WithAbs.equiv (↑x : AbsoluteValue K ℝ) : (a : WithAbs (↑x : AbsoluteValue K ℝ)) → K) (z x)) :
            WithAbs (↑u : AbsoluteValue K ℝ)))
    atTop
    (𝓝 (∑ j : InfinitePlace K, Pi.single (M := fun (i : InfinitePlace K) ↦ WithAbs (↑i : AbsoluteValue K ℝ)) j (z j) u))

Tactic:
refine tendsto_finsetSum _ fun w _ ↦ ?_

Premises used: tendsto_finsetSum
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
pos :
  ∀ (hw : u = w),
    Tendsto (β := WithAbs (↑u : AbsoluteValue K ℝ))
      (fun (i : ℕ) ↦
        HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
          (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
              (1 / (1 + (a w)⁻¹ ^ i)) :
            WithAbs (↑u : AbsoluteValue K ℝ))
          (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
              ((WithAbs.equiv (↑w : AbsoluteValue K ℝ) : (a : WithAbs (↑w : AbsoluteValue K ℝ)) → K) (z w)) :
            WithAbs (↑u : AbsoluteValue K ℝ)))
      atTop
      (𝓝 (Pi.single (M := fun (i : InfinitePlace K) ↦ WithAbs (↑i : AbsoluteValue K ℝ)) w (z w) u) :
        Filter (WithAbs (↑u : AbsoluteValue K ℝ)))
neg :
  ∀ (hw : ¬u = w),
    Tendsto (β := WithAbs (↑u : AbsoluteValue K ℝ))
      (fun (i : ℕ) ↦
        HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
          (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
              (1 / (1 + (a w)⁻¹ ^ i)) :
            WithAbs (↑u : AbsoluteValue K ℝ))
          (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
              ((WithAbs.equiv (↑w : AbsoluteValue K ℝ) : (a : WithAbs (↑w : AbsoluteValue K ℝ)) → K) (z w)) :
            WithAbs (↑u : AbsoluteValue K ℝ)))
      atTop
      (𝓝 (Pi.single (M := fun (i : InfinitePlace K) ↦ WithAbs (↑i : AbsoluteValue K ℝ)) w (z w) u) :
        Filter (WithAbs (↑u : AbsoluteValue K ℝ)))
⊢ Tendsto (β := WithAbs (↑u : AbsoluteValue K ℝ))
    (fun (i : ℕ) ↦
      HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            (1 / (1 + (a w)⁻¹ ^ i)) :
          WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            ((WithAbs.equiv (↑w : AbsoluteValue K ℝ) : (a : WithAbs (↑w : AbsoluteValue K ℝ)) → K) (z w)) :
          WithAbs (↑u : AbsoluteValue K ℝ)))
    atTop
    (𝓝 (Pi.single (M := fun (i : InfinitePlace K) ↦ WithAbs (↑i : AbsoluteValue K ℝ)) w (z w) u) :
      Filter (WithAbs (↑u : AbsoluteValue K ℝ)))

Tactic:
by_cases hw : u = w
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : u = w
pos :
  Tendsto
    (fun (i : ℕ) ↦
      HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            (1 / (1 + (a u)⁻¹ ^ i)) :
          WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            ((WithAbs.equiv (↑u : AbsoluteValue K ℝ) : (a : WithAbs (↑u : AbsoluteValue K ℝ)) → K) (z u)) :
          WithAbs (↑u : AbsoluteValue K ℝ)))
    atTop (𝓝 (z u))
⊢ Tendsto (β := WithAbs (↑u : AbsoluteValue K ℝ))
    (fun (i : ℕ) ↦
      HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            (1 / (1 + (a w)⁻¹ ^ i)) :
          WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            ((WithAbs.equiv (↑w : AbsoluteValue K ℝ) : (a : WithAbs (↑w : AbsoluteValue K ℝ)) → K) (z w)) :
          WithAbs (↑u : AbsoluteValue K ℝ)))
    atTop
    (𝓝 (Pi.single (M := fun (i : InfinitePlace K) ↦ WithAbs (↑i : AbsoluteValue K ℝ)) w (z w) u) :
      Filter (WithAbs (↑u : AbsoluteValue K ℝ)))

Tactic:
rw [← hw, Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : u = w
⊢ LT.lt (α := ℝ) ((u : (a : K) → ℝ) (a u)⁻¹ : ℝ) (1 : ℝ)

Tactic:
simpa [← inv_pow, inv_lt_one_iff₀] using .inr (hx u).1

Premises used: inv_pow, inv_lt_one_iff₀
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : u = w
⊢ LT.lt (α := ℝ) ((u : (a : K) → ℝ) (a u)⁻¹ : ℝ) (1 : ℝ)

Tactic:
have : u (a u)⁻¹ < 1 := by simpa [← inv_pow, inv_lt_one_iff₀] using .inr (hx u).1
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : u = w
this : LT.lt (α := ℝ) ((u : (a : K) → ℝ) (a u)⁻¹ : ℝ) (1 : ℝ)
⊢ Tendsto
    (fun (i : ℕ) ↦
      HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            (1 / (1 + (a u)⁻¹ ^ i)) :
          WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            ((WithAbs.equiv (↑u : AbsoluteValue K ℝ) : (a : WithAbs (↑u : AbsoluteValue K ℝ)) → K) (z u)) :
          WithAbs (↑u : AbsoluteValue K ℝ)))
    atTop (𝓝 (z u))

Tactic:
simpa using (WithAbs.tendsto_one_div_one_add_pow_nhds_one this).mul_const (z u)

Premises used: WithAbs.tendsto_one_div_one_add_pow_nhds_one, Filter.Tendsto.mul_const
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : ¬u = w
neg :
  Tendsto.{0, u_1} (β := WithAbs (↑u : AbsoluteValue K ℝ))
    (fun (i : ℕ) ↦
      HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            (1 / (1 + (a w)⁻¹ ^ i)) :
          WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            ((WithAbs.equiv (↑w : AbsoluteValue K ℝ) : (a : WithAbs (↑w : AbsoluteValue K ℝ)) → K) (z w)) :
          WithAbs (↑u : AbsoluteValue K ℝ)))
    atTop (𝓝 0)
⊢ Tendsto (β := WithAbs (↑u : AbsoluteValue K ℝ))
    (fun (i : ℕ) ↦
      HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            (1 / (1 + (a w)⁻¹ ^ i)) :
          WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            ((WithAbs.equiv (↑w : AbsoluteValue K ℝ) : (a : WithAbs (↑w : AbsoluteValue K ℝ)) → K) (z w)) :
          WithAbs (↑u : AbsoluteValue K ℝ)))
    atTop
    (𝓝 (Pi.single (M := fun (i : InfinitePlace K) ↦ WithAbs (↑i : AbsoluteValue K ℝ)) w (z w) u) :
      Filter (WithAbs (↑u : AbsoluteValue K ℝ)))

Tactic:
rw [Pi.single_eq_of_ne (M := fun v ↦ WithAbs v.1) hw (z w)]

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : ¬u = w
ha : a w = 0
linarith : -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ False

Tactic:
linarith [map_zero w ▸ ha ▸ (hx w).1]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : ¬u = w
⊢ LT.lt (α := ℝ) (1 : ℝ) ((u : (a : K) → ℝ) (a w)⁻¹ : ℝ)

Tactic:
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⟩

Premises used: one_lt_inv_iff₀
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : ¬u = w
⊢ LT.lt (α := ℝ) (1 : ℝ) ((u : (a : K) → ℝ) (a w)⁻¹ : ℝ)

Tactic:
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⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : ¬u = w
hu : LT.lt (α := ℝ) (1 : ℝ) ((u : (a : K) → ℝ) (a w)⁻¹ : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ((↑u : AbsoluteValue K ℝ) : (a : K) → ℝ) (1 / (1 + (a w)⁻¹ ^ n))) atTop (𝓝 0)

Tactic:
have := u.1.tendsto_div_one_add_pow_nhds_zero hu
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
u w : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ w
hw : ¬u = w
hu : LT.lt (α := ℝ) (1 : ℝ) ((u : (a : K) → ℝ) (a w)⁻¹ : ℝ)
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖WithAbs.toAbs (↑u : AbsoluteValue K ℝ) (1 / (1 + (a w)⁻¹ ^ n))‖) atTop (𝓝 0)
⊢ Tendsto.{0, u_1} (β := WithAbs (↑u : AbsoluteValue K ℝ))
    (fun (i : ℕ) ↦
      HMul.hMul (α := WithAbs (↑u : AbsoluteValue K ℝ)) (β := WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            (1 / (1 + (a w)⁻¹ ^ i)) :
          WithAbs (↑u : AbsoluteValue K ℝ))
        (((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ))
            ((WithAbs.equiv (↑w : AbsoluteValue K ℝ) : (a : WithAbs (↑w : AbsoluteValue K ℝ)) → K) (z w)) :
          WithAbs (↑u : AbsoluteValue K ℝ)))
    atTop (𝓝 0)

Tactic:
simpa using (tendsto_zero_iff_norm_tendsto_zero.2 this).mul_const
        ((WithAbs.equiv u.1).symm (WithAbs.equiv w.1 (z w)))

Premises used: Iff.mpr, WithAbs.equiv, Filter.Tendsto.mul_const, tendsto_zero_iff_norm_tendsto_zero, Subtype.val, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
⊢ Tendsto
    (fun (n : ℕ) (v : InfinitePlace K) ↦
      ((WithAbs.equiv (↑v : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑v : AbsoluteValue K ℝ)) (y n))
    atTop (𝓝 z)

Tactic:
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)))
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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)
let :
  ∀ (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
⊢ ∃ (y : K),
    dist z
        ((algebraMap K ((v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ)) :
            (a : K) → (v : InfinitePlace K) → WithAbs (↑v : AbsoluteValue K ℝ))
          y) <
      r

Tactic:
let ⟨N, h⟩ := Metric.tendsto_atTop.1 this r hr
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : (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

Tactic:
⟨y N, dist_comm z (algebraMap K _ (y N)) ▸ h N le_rfl⟩

Premises used: le_rfl, Algebra.algebraMap, Eq.rec, dist_comm, Exists.intro, Eq.symm, DFunLike.coe