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)
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:
exact ⟨y N, dist_comm z (algebraMap K _ (y N)) ▸ h N le_rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
hK' : ∀ (s : K), IsIntegral ℚ s ∧ Polynomial.Splits (Polynomial.map (algebraMap ℚ A) (minpoly ℚ s))
⊢ Nonempty (K →ₐ[ℚ] A)

Tactic:
apply IntermediateField.nonempty_algHom_of_splits

Premises used: IntermediateField.nonempty_algHom_of_splits
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
⊢ ∀ (s : K), IsIntegral ℚ s ∧ Polynomial.Splits (Polynomial.map (algebraMap ℚ A) (minpoly ℚ s))

Tactic:
fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, IsAlgClosed.splits _⟩

Premises used: Algebra.IsIntegral.isIntegral, Algebra.algebraMap, Rat, minpoly, And.intro, IsAlgClosed.splits, Polynomial.map
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
⊢ ∀ (s : K), IsIntegral ℚ s ∧ Polynomial.Splits (Polynomial.map (algebraMap ℚ A) (minpoly ℚ s))

Tactic:
exact fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, IsAlgClosed.splits _⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
obtain : ∀ (f : K →ₐ[ℚ] A), Nonempty (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 _⟩

Premises used: AlgHom, Rat, Nonempty
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
f : K →ₐ[ℚ] A
⊢ Nonempty (K →+* A)

Tactic:
⟨f.toRingHom⟩

Premises used: Nonempty.intro, AlgHom.toRingHom
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
f : K →ₐ[ℚ] A
⊢ Nonempty (K →+* A)

Tactic:
exact ⟨f.toRingHom⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
rw₁ rw₂ : finrank ℚ K = finrank ℚ K
⊢ Fintype.card (K →+* A) = finrank ℚ K

Tactic:
rw [Fintype.ofEquiv_card RingHom.equivRatAlgHom.symm, AlgHom.card]

Premises used: Fintype.ofEquiv_card, AlgHom.card, Equiv.symm, RingHom.equivRatAlgHom
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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 : 0 < finrank ℚ K
⊢ Nonempty (K →+* A)

Tactic:
rw [← Fintype.card_pos_iff, NumberField.Embeddings.card K A]

Premises used: NumberField.Embeddings.card, Fintype.card_pos_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
⊢ 0 < finrank ℚ K

Tactic:
Module.finrank_pos

Premises used: Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
⊢ 0 < finrank ℚ K

Tactic:
exact Module.finrank_pos

Premises used: Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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

Tactic:
(NumberField.isAlgebraic K).range_eval_eq_rootSet_minpoly A x

Premises used: Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
h :
  Eq.{u_2 + 1} (α := Set A) (range fun (φ : K →+* A) ↦ (φ : (a : K) → A) x)
    (range fun (ψ : K →ₐ[ℚ] A) ↦ (ψ : (a : K) → A) x)
⊢ (range fun (φ : K →+* A) ↦ (φ : (a : K) → A) x) = rootSet (minpoly ℚ x) A

Tactic:
convert! (NumberField.isAlgebraic K).range_eval_eq_rootSet_minpoly A x using 1

Premises used: Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
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
⊢ Eq.{u_2 + 1} (α := Set A) (range fun (φ : K →+* A) ↦ (φ : (a : K) → A) x)
    (range fun (ψ : K →ₐ[ℚ] A) ↦ (ψ : (a : K) → A) x)

Tactic:
ext a
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
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:
⟨fun ⟨φ, hφ⟩ => ⟨φ.toRatAlgHom, hφ⟩, fun ⟨φ, hφ⟩ => ⟨φ.toRingHom, hφ⟩⟩

Premises used: _private.0.NumberField.Embeddings.range_eval_eq_rootSet_minpoly.match_1, Membership.mem, RingHom.toRatAlgHom, AlgHom.toRingHom, Iff.intro, Exists.intro, Set.range, DFunLike.coe, _private.0.NumberField.Embeddings.range_eval_eq_rootSet_minpoly.match_2
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
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:
exact ⟨fun ⟨φ, hφ⟩ => ⟨φ.toRatAlgHom, hφ⟩, fun ⟨φ, hφ⟩ => ⟨φ.toRingHom, hφ⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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 : ℕ
⊢ IsIntegral ℚ x

Tactic:
have hx := Algebra.IsSeparable.isIntegral ℚ x
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
rw :
  ‖coeff (map (algebraMap ℚ A) (minpoly ℚ x)) i‖ ≤
    max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)
⊢ ‖coeff (minpoly ℚ x) i‖ ≤ max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)

Tactic:
rw [← norm_algebraMap' A, ← coeff_map (algebraMap ℚ A)]

Premises used: Polynomial.coeff_map, Algebra.algebraMap, Rat, norm_algebraMap'
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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)) : ℝ)

Tactic:
coeff_bdd_of_roots_le _ (minpoly.monic hx)
      (IsAlgClosed.splits _) (minpoly.natDegree_le x) (fun z hz => ?_) i

Premises used: minpoly.monic, Polynomial.coeff_bdd_of_roots_le, IsAlgClosed.splits, minpoly.natDegree_le
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
refine : ∀ (z : A) (hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))), ‖z‖ ≤ B
⊢ ‖coeff (map (algebraMap ℚ A) (minpoly ℚ x)) i‖ ≤
    max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)

Tactic:
refine coeff_bdd_of_roots_le _ (minpoly.monic hx)
      (IsAlgClosed.splits _) (minpoly.natDegree_le x) (fun z hz => ?_) i

Premises used: minpoly.monic, Polynomial.coeff_bdd_of_roots_le, IsAlgClosed.splits, minpoly.natDegree_le
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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 ∈ (roots (map (algebraMap ℚ A) (minpoly ℚ x))).toFinset

Tactic:
rw [← Multiset.mem_toFinset] at hz

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
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
⊢ ‖z‖ ≤ B

Tactic:
obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz

Premises used: Eq.subset, Eq.symm, NumberField.Embeddings.range_eval_eq_rootSet_minpoly, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
φ : 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:
h φ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
φ : 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:
exact h φ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
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
⊢ ‖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 φ

Premises used: Eq.subset, Eq.symm, NumberField.Embeddings.range_eval_eq_rootSet_minpoly, Multiset.mem_toFinset, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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)
    (⋃ (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)
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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}

Tactic:
this.subset fun x hx => ?_

Premises used: Set.Finite.subset
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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))
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
⊢ Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}

Tactic:
refine this.subset fun x hx => ?_

Premises used: Set.Finite.subset
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
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)
⊢ 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:
simp_rw [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
⊢ minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)

Tactic:
have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ ∃ (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:
⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩

Premises used: Iff.mpr, Int, minpoly.aeval, And.left, And.intro, Exists.intro, Polynomial.mem_rootSet, minpoly.ne_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
refine_1 : natDegree (minpoly ℤ x) ≤ finrank ℚ K
refine_2 : ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (coeff (minpoly ℤ x) i)
⊢ ∃ (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:
refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
refine_1 : natDegree (minpoly ℚ x) ≤ finrank ℚ K
⊢ natDegree (minpoly ℤ x) ≤ finrank ℚ K

Tactic:
rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]

Premises used: minpoly.monic, Algebra.algebraMap, Rat, Int, Polynomial.Monic.natDegree_map, And.left
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ natDegree (minpoly ℚ x) ≤ finrank ℚ K

Tactic:
minpoly.natDegree_le x

Premises used: minpoly.natDegree_le
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
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
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ natDegree (minpoly ℚ x) ≤ finrank ℚ K

Tactic:
exact minpoly.natDegree_le x

Premises used: minpoly.natDegree_le