awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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)
Tactic: rw [Pi.single_eq_of_ne (M := fun v ↦ WithAbs v.1) hw (z 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
ha : a w = 0
⊢ False
have linarith : -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith [map_zero w ▸ ha ▸ (hx w).1]
-- 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.{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)
have hu : 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⟩
-- 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
hu : LT.lt (α := ℝ) (1 : ℝ) ((u : (a : K) → ℝ) (a w)⁻¹ : ℝ)
⊢ 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)
have this : 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
-- 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)
⊢ ∃ (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 this : 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)))
-- 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)
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
have 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
Tactic: let ⟨N, h⟩ := Metric.tendsto_atTop.1 this 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
⊢ 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 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
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⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
A : Type u_2
inst_1 : Field A
inst_2 : CharZero A
inst_3 : CharZero K
inst_4 : Algebra.IsAlgebraic ℚ K
inst_5 : IsAlgClosed A
⊢ Nonempty (K →ₐ[ℚ] A)
have hK' : ∀ (s : K), IsIntegral ℚ s ∧ Polynomial.Splits (Polynomial.map (algebraMap ℚ A) (minpoly ℚ s))
Tactic: apply IntermediateField.nonempty_algHom_of_splits
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
A : Type u_2
inst_1 : Field A
inst_2 : CharZero A
inst_3 : CharZero K
inst_4 : Algebra.IsAlgebraic ℚ K
inst_5 : IsAlgClosed A
⊢ Nonempty (K →+* A)
have obtain : ∀ (f : K →ₐ[ℚ] A), Nonempty (K →+* A)
Tactic: obtain ⟨f⟩ : Nonempty (K →ₐ[ℚ] A) := by
    apply IntermediateField.nonempty_algHom_of_splits
    exact fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, IsAlgClosed.splits _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
A : Type u_2
inst_1 : Field A
inst_2 : CharZero A
inst_3 : NumberField K
inst_4 : IsAlgClosed A
⊢ Fintype.card (K →+* A) = finrank ℚ K
have rw : Fintype.card (K →ₐ[ℚ] A) = finrank ℚ K
Tactic: rw [Fintype.ofEquiv_card RingHom.equivRatAlgHom.symm, AlgHom.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
A : Type u_2
inst_1 : Field A
inst_2 : CharZero A
inst_3 : NumberField K
inst_4 : IsAlgClosed A
rw : Fintype.card (K →ₐ[ℚ] A) = finrank ℚ K
⊢ Fintype.card (K →+* A) = finrank ℚ K
have rw₁ : finrank ℚ K = finrank ℚ K
Tactic: rw [Fintype.ofEquiv_card RingHom.equivRatAlgHom.symm, AlgHom.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
A : Type u_2
inst_1 : Field A
inst_2 : CharZero A
inst_3 : NumberField K
inst_4 : IsAlgClosed A
⊢ Nonempty (K →+* A)
have rw : 0 < finrank ℚ K
Tactic: rw [← Fintype.card_pos_iff, NumberField.Embeddings.card K A]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : Field A
inst_3 : Algebra ℚ A
inst_4 : IsAlgClosed A
x : K
⊢ (range fun (φ : K →+* A) ↦ (φ : (a : K) → A) x) = rootSet (minpoly ℚ x) A
have h : Eq.{u_2 + 1} (α := Set A) (range fun (φ : K →+* A) ↦ (φ : (a : K) → A) x)
  (range fun (ψ : K →ₐ[ℚ] A) ↦ (ψ : (a : K) → A) x)
Tactic: convert! (NumberField.isAlgebraic K).range_eval_eq_rootSet_minpoly A x using 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : Field A
inst_3 : Algebra ℚ A
inst_4 : IsAlgClosed A
x : K
⊢ Eq.{u_2 + 1} (α := Set A) (range fun (φ : K →+* A) ↦ (φ : (a : K) → A) x)
    (range fun (ψ : K →ₐ[ℚ] A) ↦ (ψ : (a : K) → A) x)
have h : ∀ (a : A),
  Membership.mem (γ := Set A) (range fun (φ : K →+* A) ↦ (φ : (a : K) → A) x) a ↔
    Membership.mem (γ := Set A) (range fun (ψ : K →ₐ[ℚ] A) ↦ (ψ : (a : K) → A) x) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B
i : ℕ
⊢ ‖coeff (minpoly ℚ x) i‖ ≤ max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)
have hx : IsIntegral ℚ x
Tactic: have hx := Algebra.IsSeparable.isIntegral ℚ x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖coeff (minpoly ℚ x) i‖ ≤ max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)
have rw : ‖coeff (map (algebraMap ℚ A) (minpoly ℚ x)) i‖ ≤ max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)
Tactic: rw [← norm_algebraMap' A, ← coeff_map (algebraMap ℚ A)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖coeff (map (algebraMap ℚ A) (minpoly ℚ x)) i‖ ≤
    max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)
have refine : ∀ (z : A) (hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))), ‖z‖ ≤ B
Tactic: refine coeff_bdd_of_roots_le _ (minpoly.monic hx)
      (IsAlgClosed.splits _) (minpoly.natDegree_le x) (fun z hz => ?_) i
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
⊢ ‖z‖ ≤ B
have hz₁ : z ∈ (roots (map (algebraMap ℚ A) (minpoly ℚ x))).toFinset
Tactic: rw [← Multiset.mem_toFinset] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (roots (map (algebraMap ℚ A) (minpoly ℚ x))).toFinset
⊢ ‖z‖ ≤ B
have obtain : ∀ (φ : K →+* A)
  (hz : (fun (φ : K →+* A) ↦ ((φ : (a : K) → A) x : A)) φ ∈ (roots (map (algebraMap ℚ A) (minpoly ℚ x))).toFinset),
  norm.{u_2} (E := A) ((fun (φ : K →+* A) ↦ ((φ : (a : K) → A) x : A)) φ) ≤ B
Tactic: obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
⊢ ‖z‖ ≤ B
have rw : ∀ (hz : z ∈ (roots (map (algebraMap ℚ A) (minpoly ℚ x))).toFinset), ‖z‖ ≤ B
Tactic: classical
  rw [← Multiset.mem_toFinset] at hz
  obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
  exact h φ
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
rw rw₁ rw₂ : ∀ (hz : z ∈ (roots (map (algebraMap ℚ A) (minpoly ℚ x))).toFinset), ‖z‖ ≤ B
⊢ ‖z‖ ≤ B
have rw₃ : ∀ (φ : K →+* A)
  (hz : (fun (φ : K →+* A) ↦ ((φ : (a : K) → A) x : A)) φ ∈ (roots (map (algebraMap ℚ A) (minpoly ℚ x))).toFinset),
  norm.{u_2} (E := A) ((fun (φ : K →+* A) ↦ ((φ : (a : K) → A) x : A)) φ) ≤ B
Tactic: classical
  rw [← Multiset.mem_toFinset] at hz
  obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
  exact h φ
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
⊢ Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
have this : Set.Finite.{u_1} (α := K)
  (⋃ (f : ℤ[X]),
    ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
      (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
Tactic: have := bUnion_roots_finite (algebraMap ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
⊢ Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
have refine : ∀ (x : K)
  (hx :
    Membership.mem (γ := Set K)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x),
  Membership.mem (γ := Set K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
    x
Tactic: refine this.subset fun x hx => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
⊢ Membership.mem (γ := Set K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
    x
have simp_rw : ∃ (i : ℤ[X]) (_ :
  i.natDegree ≤ finrank ℚ K ∧ ∀ (i_1 : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (i.coeff i_1)),
  x ∈ (↑(roots (map (algebraMap ℤ K) i)).toFinset : Set K)
Tactic: simp_rw [mem_iUnion]