-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem coeff_bdd_of_norm_le {B : ℝ} {x : K} (h : ∀ φ : K →+* A, ‖φ x‖ ≤ B) (i : ℕ) :
    ‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ finrank ℚ K * (finrank ℚ K).choose (finrank ℚ K / 2)

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖(minpoly ℚ x).coeff i‖ ≤ (B ⊔ 1) ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))

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

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖(map (algebraMap ℚ A) (minpoly ℚ x)).coeff i‖ ≤ (B ⊔ 1) ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots.toFinset
⊢ ‖z‖ ≤ B

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

Result:
case intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
φ : K →+* A
hz : (fun φ => φ x) φ ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots.toFinset
⊢ ‖(fun φ => φ x) φ‖ ≤ B

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots
⊢ ‖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 φ

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
φ : K →+* A
hz : (fun φ => φ x) φ ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots.toFinset
⊢ ‖(fun φ => φ x) φ‖ ≤ B

Tactic:
exact h φ

Result:
no goals

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖(map (algebraMap ℚ A) (minpoly ℚ x)).coeff i‖ ≤ (B ⊔ 1) ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))

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

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots
⊢ ‖z‖ ≤ B

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots
⊢ ‖z‖ ≤ B

Tactic:
rw [← Multiset.mem_toFinset] at hz

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : A
hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots.toFinset
⊢ ‖z‖ ≤ B

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
⊢ ‖(minpoly ℚ x).coeff i‖ ≤ (B ⊔ 1) ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))

Tactic:
have hx := Algebra.IsSeparable.isIntegral ℚ x

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖(minpoly ℚ x).coeff i‖ ≤ (B ⊔ 1) ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))