k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
⊢ Function.Surjective ↑(algebraMap k K)
refine' fun x => ⟨-(minpoly k x).coeff 0, _⟩
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (hf x)
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
h : degree (minpoly k x) = 1
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
have h : (minpoly k x).degree = 1 := degree_eq_one_of_irreducible k (minpoly.irreducible (hf x))
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
h : degree (minpoly k x) = 1
this : ↑(aeval x) (minpoly k x) = 0
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
h : degree (minpoly k x) = 1
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
h : degree (minpoly k x) = 1
this : x = -↑(algebraMap k K) (coeff (minpoly k x) 0)
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
h : degree (minpoly k x) = 1
this : ↑(aeval x) (minpoly k x) = 0
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C,
  add_eq_zero_iff_eq_neg] at this
no goals
k✝ : Type u
inst✝⁴ : Field k✝
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Ring K
inst✝¹ : IsDomain K
hk : IsAlgClosed k
inst✝ : Algebra k K
hf : Algebra.IsIntegral k K
x : K
hq : leadingCoeff (minpoly k x) = 1
h : degree (minpoly k x) = 1
this : x = -↑(algebraMap k K) (coeff (minpoly k x) 0)
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm