awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : Complex.im ((f : (a : K) → ℂ) ζ) = 0
⊢ False
have hre : Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1
Tactic: have hre : (f ζ).re = 1 ∨ (f ζ).re = -1 := by
    rw [← Complex.abs_re_eq_norm] at him
    have := Complex.norm_eq_one_of_pow_eq_one hζ'.pow_eq_one (by lia)
    rwa [← him, ← abs_one, abs_eq_abs] at this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : Complex.im ((f : (a : K) → ℂ) ζ) = 0
hnegone : Complex.re ((f : (a : K) → ℂ) ζ) = -1
⊢ False
have hζ'₁ : k = orderOf (G := ℂ) ((f : (a : K) → ℂ) ζ : ℂ)
Tactic: replace hζ' := hζ'.eq_orderOf
Cleared hypotheses: hζ'
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
him : Complex.im ((f : (a : K) → ℂ) ζ) = 0
hnegone : Complex.re ((f : (a : K) → ℂ) ζ) = -1
hζ' : k = orderOf (G := ℂ) ((f : (a : K) → ℂ) ζ : ℂ)
⊢ False
have hζ'₁ : k = if Eq (α := ℕ) 0 2 then 1 else 2
Tactic: simp only [show f ζ = -1 from Complex.ext (by simp [hnegone]) (by simp [him]),
      orderOf_neg_one, ringChar.eq_zero] at hζ'
Cleared hypotheses: hζ'
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : Complex.im ((f : (a : K) → ℂ) ζ) = 0
hre : Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1
⊢ False
have inl : ∀ (hone : Complex.re ((f : (a : K) → ℂ) ζ) = 1), False
Tactic: cases hre with
  | inl hone =>
    exact hζ'.ne_one (by lia) <| Complex.ext (by simp [hone]) (by simp [him])
  | inr hnegone =>
    replace hζ' := hζ'.eq_orderOf
    simp only [show f ζ = -1 from Complex.ext (by simp [hnegone]) (by simp [him]),
      orderOf_neg_one, ringChar.eq_zero] at hζ'
    lia
Cleared hypotheses: hre
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x : { w : InfinitePlace K // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (M := ℂ) ((f : (a : K) → ℂ) ζ : ℂ) k
him : Complex.im ((f : (a : K) → ℂ) ζ) = 0
hre : Complex.re ((f : (a : K) → ℂ) ζ) = 1 ∨ Complex.re ((f : (a : K) → ℂ) ζ) = -1
inl : ∀ (hone : Complex.re ((f : (a : K) → ℂ) ζ) = 1), False
⊢ False
have inr : ∀ (hnegone : Complex.re ((f : (a : K) → ℂ) ζ) = -1), False
Tactic: cases hre with
  | inl hone =>
    exact hζ'.ne_one (by lia) <| Complex.ext (by simp [hone]) (by simp [him])
  | inr hnegone =>
    replace hζ' := hζ'.eq_orderOf
    simp only [show f ζ = -1 from Complex.ext (by simp [hnegone]) (by simp [him]),
      orderOf_neg_one, ringChar.eq_zero] at hζ'
    lia
Cleared hypotheses: hre
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
v : InfinitePlace ℚ
x : ℚ
⊢ Eq (α := ℝ) (((↑v : AbsoluteValue ℚ ℝ) : (a : ℚ) → ℝ) x : ℝ) ((↑|x| : ℝ) : ℝ)
have obtain : ∀ (w : ℚ →+* ℂ),
  Eq (α := ℝ)
    (((↑(Subtype.mk (p := fun (w : AbsoluteValue ℚ ℝ) ↦ ∃ (φ : ℚ →+* ℂ), place φ = w) (place w) sorry) :
            AbsoluteValue ℚ ℝ) :
          (a : ℚ) → ℝ)
        x :
      ℝ)
    ((↑|x| : ℝ) : ℝ)
Tactic: obtain ⟨_, _, rfl⟩ := v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
a b : InfinitePlace ℚ
⊢ a = b
have h : ∀ (k : ℚ), Eq (α := ℝ) ((a : (a : ℚ) → ℝ) k : ℝ) ((b : (a : ℚ) → ℝ) k : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
⊢ ComplexEmbedding.IsReal (castHom ℂ)
have a : ∀ (x : ℚ), Eq (α := ℂ) ((star (castHom ℂ) : (a : ℚ) → ℂ) x : ℂ) ((castHom ℂ : (a : ℚ) → ℂ) x : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
x : ℚ
⊢ (v : (a : K) → ℝ) (↑x : K) = ‖x‖
have rcases : ∀ (val : AbsoluteValue K ℝ) (property : ∃ (φ : K →+* ℂ), place φ = val),
  (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) val property : (a : K) → ℝ) (↑x : K) =
    ‖x‖
Tactic: rcases v with ⟨_, _⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
n : ℕ
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) (↑n : K) : ℝ) ((↑n : ℝ) : ℝ)
have rcases : ∀ (val : AbsoluteValue K ℝ) (property : ∃ (φ : K →+* ℂ), place φ = val),
  Eq (α := ℝ)
    ((Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) val property : (a : K) → ℝ)
        (↑n : K) :
      ℝ)
    ((↑n : ℝ) : ℝ)
Tactic: rcases v with ⟨_, _⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
z : ℤ
⊢ (v : (a : K) → ℝ) (↑z : K) = ‖z‖
have rcases : ∀ (val : AbsoluteValue K ℝ) (property : ∃ (φ : K →+* ℂ), place φ = val),
  (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) val property : (a : K) → ℝ) (↑z : K) =
    ‖z‖
Tactic: rcases v with ⟨_, _⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v w : InfinitePlace K
t : ℝ
h : HPow.hPow (α := K → ℝ) (fun (x : K) ↦ (w : (a : K) → ℝ) x) t = (⇑v : (a : K) → ℝ)
⊢ t = 1
have obtain : ∀ (n : ℕ) (hn : 1 < n), t = 1
Tactic: obtain ⟨n, hn⟩ := exists_gt (1 : ℕ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v w : InfinitePlace K
⊢ w = v ↔ (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)
have refine : ∀ (h : (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)), w = v
Tactic: refine ⟨fun h ↦ h ▸ .rfl, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v w : InfinitePlace K
h : (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)
⊢ w = v
have obtain : ∀ (t : ℝ),
  0 < t →
    ∀
      (h :
        Eq (α := K → ℝ) (fun (x : K) ↦ HPow.hPow (α := ℝ) (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) x : ℝ) t)
          (⇑(↑v : AbsoluteValue K ℝ) : (a : K) → ℝ)),
      w = v
Tactic: obtain ⟨t, _, h⟩ := w.1.isEquiv_iff_exists_rpow_eq.1 h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
⊢ (↑v : AbsoluteValue K ℝ).IsNontrivial
have obtain : ∀ (n : ℕ) (hn : 1 < n), (↑v : AbsoluteValue K ℝ).IsNontrivial
Tactic: obtain ⟨n, hn⟩ := exists_gt (1 : ℕ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
⊢ Ne (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (↑n : K) : ℝ) (1 : ℝ)
have simp : ¬n = 1
Tactic: simp [← coe_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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 ℝ))
have refine : ∀ (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
Tactic: refine Metric.denseRange_iff.mpr fun z r hr ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
have choose : ∀ (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
Tactic: 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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)
have refine : ∀ (u : InfinitePlace K),
  Tendsto
    (fun (i : ℕ) ↦ ((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ)) (y i))
    atTop (𝓝 (z u))
Tactic: refine tendsto_pi_nhds.mpr fun u ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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
⊢ Tendsto
    (fun (i : ℕ) ↦ ((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ)) (y i))
    atTop (𝓝 (z u))
have simp_rw : 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: simp_rw [← Fintype.sum_pi_single u z, y, map_sum, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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
⊢ 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))
have 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 ℝ)))
Tactic: refine tendsto_finsetSum _ fun w _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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
⊢ 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 ℝ)))
have 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 ℝ)))
Tactic: by_cases hw : u = w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 ℝ)))
⊢ 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 ℝ)))
have 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 ℝ)))
Tactic: by_cases hw : u = w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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
⊢ 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 ℝ)))
have 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))
Tactic: rw [← hw, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
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
⊢ 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))
have this : 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