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
ζ : 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
hone : Complex.re ((f : (a : K) → ℂ) ζ) = 1
⊢ Complex.re ((f : (a : K) → ℂ) ζ) = Complex.re 1

Tactic:
simp [hone]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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
hone : Complex.re ((f : (a : K) → ℂ) ζ) = 1
⊢ Complex.im ((f : (a : K) → ℂ) ζ) = Complex.im 1

Tactic:
simp [him]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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
hone : Complex.re ((f : (a : K) → ℂ) ζ) = 1
⊢ False

Tactic:
exact hζ'.ne_one (by lia) <| Complex.ext (by simp [hone]) (by simp [him])

Premises used: Complex.ext, IsPrimitiveRoot.ne_one
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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
⊢ k = orderOf (G := ℂ) ((f : (a : K) → ℂ) ζ : ℂ)

Tactic:
replace hζ' := hζ'.eq_orderOf
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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) → ℂ) ζ : ℂ)
⊢ Complex.re ((f : (a : K) → ℂ) ζ) = Complex.re (-1)

Tactic:
simp [hnegone]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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) → ℂ) ζ : ℂ)
⊢ Complex.im ((f : (a : K) → ℂ) ζ) = Complex.im (-1)

Tactic:
simp [him]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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) → ℂ) ζ : ℂ)
⊢ 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ζ'

Premises used: orderOf_neg_one, Complex.ext, ringChar.eq_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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 = if Eq (α := ℕ) 0 2 then 1 else 2
⊢ False

Tactic:
lia
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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
inr : ∀ (hnegone : Complex.re ((f : (a : K) → ℂ) ζ) = -1), False
⊢ 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

Premises used: orderOf_neg_one, Complex.ext, IsPrimitiveRoot.ne_one, ringChar.eq_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
v : InfinitePlace ℚ
x : ℚ
obtain :
  ∀ (w : ℚ →+* ℂ),
    Eq (α := ℝ)
      (((↑(Subtype.mk (p := fun (w : AbsoluteValue ℚ ℝ) ↦ ∃ (φ : ℚ →+* ℂ), place φ = w) (place w) ⋯) :
              AbsoluteValue ℚ ℝ) :
            (a : ℚ) → ℝ)
          x :
        ℝ)
      ((↑|x| : ℝ) : ℝ)
⊢ Eq (α := ℝ) (((↑v : AbsoluteValue ℚ ℝ) : (a : ℚ) → ℝ) x : ℝ) ((↑|x| : ℝ) : ℝ)

Tactic:
obtain ⟨_, _, rfl⟩ := v

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
x : ℚ
w : ℚ →+* ℂ
⊢ Eq (α := ℝ)
    (((↑(Subtype.mk (p := fun (w : AbsoluteValue ℚ ℝ) ↦ ∃ (φ : ℚ →+* ℂ), place φ = w) (place w) ⋯) :
            AbsoluteValue ℚ ℝ) :
          (a : ℚ) → ℝ)
        x :
      ℝ)
    ((↑|x| : ℝ) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
a b : InfinitePlace ℚ
h : ∀ (k : ℚ), Eq (α := ℝ) ((a : (a : ℚ) → ℝ) k : ℝ) ((b : (a : ℚ) → ℝ) k : ℝ)
⊢ a = b

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
a b : InfinitePlace ℚ
k : ℚ
⊢ Eq (α := ℝ) ((a : (a : ℚ) → ℝ) k : ℝ) ((b : (a : ℚ) → ℝ) k : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
a : ∀ (x : ℚ), Eq (α := ℂ) ((star (castHom ℂ) : (a : ℚ) → ℂ) x : ℂ) ((castHom ℂ : (a : ℚ) → ℂ) x : ℂ)
⊢ ComplexEmbedding.IsReal (castHom ℂ)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
x : ℚ
⊢ Eq (α := ℂ) ((star (castHom ℂ) : (a : ℚ) → ℂ) x : ℂ) ((castHom ℂ : (a : ℚ) → ℂ) x : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
x : ℚ
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‖
⊢ (v : (a : K) → ℝ) (↑x : K) = ‖x‖

Tactic:
rcases v with ⟨_, _⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
x : ℚ
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:
aesop (add simp [coe_apply])

Premises used: NumberField.InfinitePlace.coe_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
n : ℕ
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 : ℝ) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) (↑n : K) : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
rcases v with ⟨_, _⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
n : ℕ
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:
aesop (add simp [coe_apply])

Premises used: NumberField.InfinitePlace.coe_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
z : ℤ
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‖
⊢ (v : (a : K) → ℝ) (↑z : K) = ‖z‖

Tactic:
rcases v with ⟨_, _⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
z : ℤ
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:
aesop (add simp [coe_apply])

Premises used: NumberField.InfinitePlace.coe_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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) → ℝ)
obtain : ∀ (n : ℕ) (hn : 1 < n), t = 1
⊢ t = 1

Tactic:
obtain ⟨n, hn⟩ := exists_gt (1 : ℕ)

Premises used: NoMaxOrder.exists_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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) → ℝ)
n : ℕ
hn : 1 < n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
grind [Nat.cast_pos]

Premises used: Nat.cast_pos
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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) → ℝ)
n : ℕ
hn : 1 < n
⊢ Ne (α := ℝ) (↑n : ℝ) 1

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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) → ℝ)
n : ℕ
hn : 1 < n
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) t = HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1

Tactic:
simpa using funext_iff.1 h n

Premises used: funext_iff, Nat.cast, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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) → ℝ)
n : ℕ
hn : 1 < n
⊢ t = 1

Tactic:
exact ((n : ℝ).rpow_right_inj (by grind [Nat.cast_pos]) (by aesop)).1 <|
    by simpa using funext_iff.1 h n

Premises used: Iff.mp, Real.rpow_right_inj
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v w : InfinitePlace K
⊢ w = v ↔ (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)

Tactic:
⟨fun h ↦ h ▸ .rfl, fun h ↦ ?_⟩

Premises used: AbsoluteValue.IsEquiv.rfl, Eq.rec, Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v w : InfinitePlace K
refine : ∀ (h : (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)), w = v
⊢ w = v ↔ (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)

Tactic:
refine ⟨fun h ↦ h ▸ .rfl, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v w : InfinitePlace K
h : (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)
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
⊢ w = v

Tactic:
obtain ⟨t, _, h⟩ := w.1.isEquiv_iff_exists_rpow_eq.1 h

Premises used: Iff.mp, AbsoluteValue.isEquiv_iff_exists_rpow_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v w : InfinitePlace K
h_1 : (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)
t : ℝ
left : 0 < t
h :
  Eq (α := K → ℝ) (fun (x : K) ↦ HPow.hPow (α := ℝ) (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) x : ℝ) t)
    (⇑(↑v : AbsoluteValue K ℝ) : (a : K) → ℝ)
k : K
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) k : ℝ) ((v : (a : K) → ℝ) k : ℝ)

Tactic:
simpa [eq_one_of_rpow_eq h, ext, coe_apply] using funext_iff.1 h k

Premises used: NumberField.InfinitePlace.coe_apply, funext_iff, NumberField.InfinitePlace.eq_one_of_rpow_eq, Iff.mp, NumberField.InfinitePlace.ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v w : InfinitePlace K
h_1 : (↑w : AbsoluteValue K ℝ).IsEquiv (↑v : AbsoluteValue K ℝ)
t : ℝ
left : 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:
exact ext _ _ fun k ↦ by simpa [eq_one_of_rpow_eq h, ext, coe_apply] using funext_iff.1 h k

Premises used: NumberField.InfinitePlace.ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
obtain : ∀ (n : ℕ) (hn : 1 < n), (↑v : AbsoluteValue K ℝ).IsNontrivial
⊢ (↑v : AbsoluteValue K ℝ).IsNontrivial

Tactic:
obtain ⟨n, hn⟩ := exists_gt (1 : ℕ)

Premises used: NoMaxOrder.exists_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
⊢ LT.lt (α := ℝ) (1 : ℝ) ((v : (a : K) → ℝ) (↑n : K) : ℝ)

Tactic:
simpa
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
simp : ¬n = 1
⊢ Ne (α := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (↑n : K) : ℝ) (1 : ℝ)

Tactic:
simp [← coe_apply]

Premises used: NumberField.InfinitePlace.coe_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
⊢ ¬n = 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
⊢ (↑v : AbsoluteValue K ℝ).IsNontrivial

Tactic:
exact ⟨n, v.pos_iff.1 <| zero_lt_one.trans (by simpa), by simp [← coe_apply]; grind⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
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 ℝ))

Tactic:
Metric.denseRange_iff.mpr fun z r hr ↦ ?_

Premises used: Iff.mpr, Metric.denseRange_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
⊢ 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:
refine Metric.denseRange_iff.mpr fun z r hr ↦ ?_

Premises used: Iff.mpr, Metric.denseRange_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
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
⊢ ∃ (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

Premises used: NumberField.InfinitePlace.isNontrivial, NumberField.InfinitePlace.eq_iff_isEquiv, Iff.not, AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv, Iff.mp
-- 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:
tendsto_pi_nhds.mpr fun u ↦ ?_

Premises used: Iff.mpr, tendsto_pi_nhds
-- 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)
refine :
  ∀ (u : InfinitePlace K),
    Tendsto
      (fun (i : ℕ) ↦ ((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ)) (y i))
      atTop (𝓝 (z u))
⊢ Tendsto
    (fun (n : ℕ) (v : InfinitePlace K) ↦
      ((WithAbs.equiv (↑v : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑v : AbsoluteValue K ℝ)) (y n))
    atTop (𝓝 z)

Tactic:
refine tendsto_pi_nhds.mpr fun u ↦ ?_

Premises used: Iff.mpr, tendsto_pi_nhds
-- 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
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))
⊢ Tendsto
    (fun (i : ℕ) ↦ ((WithAbs.equiv (↑u : AbsoluteValue K ℝ)).symm : (a : K) → WithAbs (↑u : AbsoluteValue K ℝ)) (y i))
    atTop (𝓝 (z u))

Tactic:
simp_rw [← Fintype.sum_pi_single u z, y, map_sum, map_mul]

Premises used: map_sum, map_mul, Fintype.sum_pi_single
-- 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
⊢ 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:
tendsto_finsetSum _ fun w _ ↦ ?_

Premises used: tendsto_finsetSum