-- 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 : ℝ
let let₁ let₂ :
  Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
let₃ :
  let 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}
let₄ let₅ :
  let 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
let₆ :
  let 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),
    ∃ (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)
let₇ :
  let 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)
refine_1 :
  let 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
refine_2 refine_2₁ :
  let 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 : ℕ),
    Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (coeff (minpoly ℤ x) i)
refine_2₂ :
  let 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 : ℕ),
    LE.le (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) (↑(↑C : ℤ) : ℝ)
refine_2₃ :
  let 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 : ℕ),
    (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
⊢ Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}

Tactic:
classical
  let C := Nat.ceil (max B 1 ^ finrank ℚ K * (finrank ℚ K).choose (finrank ℚ K / 2))
  have := bUnion_roots_finite (algebraMap ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C)
  refine this.subset fun x hx => ?_; simp_rw [mem_iUnion]
  have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
  refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
  · rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]
    exact minpoly.natDegree_le x
  rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
  refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
  rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]

Premises used: Int.cast_abs, Polynomial.coeff_map, Int.cast_le, abs_le, Set.mem_iUnion, Int.norm_eq_abs, eq_intCast, Int.norm_cast_rat, Set.mem_Icc