k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
⊢ (Set.range fun ψ => ↑ψ x) = rootSet (minpoly F x) A
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
⊢ (Set.range fun ψ => ↑ψ x) = rootSet (minpoly F x) A
have hFK := Algebra.isAlgebraic_iff_isIntegral.1 hK
case h
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
⊢ (a ∈ Set.range fun ψ => ↑ψ x) ↔ a ∈ rootSet (minpoly F x) A
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
⊢ (Set.range fun ψ => ↑ψ x) = rootSet (minpoly F x) A
ext a
case h
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
⊢ (a ∈ Set.range fun ψ => ↑ψ x) ↔ ↑(aeval a) (minpoly F x) = 0
case h
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
⊢ (a ∈ Set.range fun ψ => ↑ψ x) ↔ a ∈ rootSet (minpoly F x) A
rw [mem_rootSet_of_ne (minpoly.ne_zero (hFK x))]
case h.refine'_1
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
⊢ (a ∈ Set.range fun ψ => ↑ψ x) → ↑(aeval a) (minpoly F x) = 0

case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
⊢ (a ∈ Set.range fun ψ => ↑ψ x) ↔ ↑(aeval a) (minpoly F x) = 0
refine' ⟨_, fun ha => _⟩
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
⊢ a ∈ Set.range fun ψ => ↑ψ x
let Fx := AdjoinRoot (minpoly F x)
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
⊢ a ∈ Set.range fun ψ => ↑ψ x
have hx : aeval x (minpoly F x) = 0 := minpoly.aeval F x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
⊢ a ∈ Set.range fun ψ => ↑ψ x
letI : Algebra Fx A := (AdjoinRoot.lift (algebraMap F A) a ha).toAlgebra
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝ : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
⊢ a ∈ Set.range fun ψ => ↑ψ x
letI : Algebra Fx K := (AdjoinRoot.lift (algebraMap F K) x hx).toAlgebra
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝¹ : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this✝ : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
this : IsScalarTower F Fx A
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝ : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
⊢ a ∈ Set.range fun ψ => ↑ψ x
haveI : IsScalarTower F Fx A := IsScalarTower.of_ring_hom (AdjoinRoot.liftHom _ a ha)
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝² : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this✝¹ : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
this✝ : IsScalarTower F Fx A
this : IsScalarTower F Fx K
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝¹ : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this✝ : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
this : IsScalarTower F Fx A
⊢ a ∈ Set.range fun ψ => ↑ψ x
haveI : IsScalarTower F Fx K := IsScalarTower.of_ring_hom (AdjoinRoot.liftHom _ x hx)
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝³ : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this✝² : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
this✝¹ : IsScalarTower F Fx A
this✝ : IsScalarTower F Fx K
this : Fact (Irreducible (minpoly F x))
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝² : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this✝¹ : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
this✝ : IsScalarTower F Fx A
this : IsScalarTower F Fx K
⊢ a ∈ Set.range fun ψ => ↑ψ x
haveI : Fact (Irreducible <| minpoly F x) := ⟨minpoly.irreducible <| hFK x⟩
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝³ : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this✝² : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
this✝¹ : IsScalarTower F Fx A
this✝ : IsScalarTower F Fx K
this : Fact (Irreducible (minpoly F x))
ψ₀ : K →ₐ[Fx] A := IsAlgClosed.lift (_ : IsAlgebraic Fx K)
⊢ a ∈ Set.range fun ψ => ↑ψ x
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝³ : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this✝² : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
this✝¹ : IsScalarTower F Fx A
this✝ : IsScalarTower F Fx K
this : Fact (Irreducible (minpoly F x))
⊢ a ∈ Set.range fun ψ => ↑ψ x
let ψ₀ : K →ₐ[Fx] A := IsAlgClosed.lift (Algebra.isAlgebraic_of_larger_base F Fx hK)
no goals
case h.refine'_2
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
ha : ↑(aeval a) (minpoly F x) = 0
Fx : Type u_1 := AdjoinRoot (minpoly F x)
hx : ↑(aeval x) (minpoly F x) = 0
this✝³ : Algebra Fx A := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F A) a ha)
this✝² : Algebra Fx K := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F K) x hx)
this✝¹ : IsScalarTower F Fx A
this✝ : IsScalarTower F Fx K
this : Fact (Irreducible (minpoly F x))
ψ₀ : K →ₐ[Fx] A := IsAlgClosed.lift (_ : IsAlgebraic Fx K)
⊢ a ∈ Set.range fun ψ => ↑ψ x
exact
  ⟨ψ₀.restrictScalars F,
    (congr_arg ψ₀ (AdjoinRoot.lift_root hx).symm).trans <|
      (ψ₀.commutes _).trans <| AdjoinRoot.lift_root ha⟩
case h.refine'_1.intro
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
ψ : K →ₐ[F] A
⊢ ↑(aeval ((fun ψ => ↑ψ x) ψ)) (minpoly F x) = 0
case h.refine'_1
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
a : (fun x => A) x
⊢ (a ∈ Set.range fun ψ => ↑ψ x) → ↑(aeval a) (minpoly F x) = 0
rintro ⟨ψ, rfl⟩
no goals
case h.refine'_1.intro
k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : IsAlgClosed A
inst✝¹ : Algebra F K
hK : IsAlgebraic F K
inst✝ : Algebra F A
x : K
hFK : Algebra.IsIntegral F K
ψ : K →ₐ[F] A
⊢ ↑(aeval ((fun ψ => ↑ψ x) ψ)) (minpoly F x) = 0
rw [aeval_algHom_apply ψ x, minpoly.aeval, map_zero]