[GOAL]
k✝ : Type u
inst✝³ : Field k✝
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : IsAlgClosed k
inst✝ : Field K
f : K →+* k
p : K[X]
⊢ Splits f p
[PROOFSTEP]
convert IsAlgClosed.splits (p.map f)
[GOAL]
case a
k✝ : Type u
inst✝³ : Field k✝
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : IsAlgClosed k
inst✝ : Field K
f : K →+* k
p : K[X]
⊢ Splits f p ↔ Splits (RingHom.id k) (map f p)
[PROOFSTEP]
simp [splits_map_iff]
[GOAL]
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
have : degree (X ^ n - C x) ≠ 0 := by
  rw [degree_X_pow_sub_C hn x]
  exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
[GOAL]
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ degree (X ^ n - ↑C x) ≠ 0
[PROOFSTEP]
rw [degree_X_pow_sub_C hn x]
[GOAL]
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
[GOAL]
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this
[GOAL]
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
use z
[GOAL]
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ z ^ n = x
[PROOFSTEP]
simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
[GOAL]
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
z : k
hz : z ^ n - x = 0
⊢ z ^ n = x
[PROOFSTEP]
exact sub_eq_zero.1 hz
[GOAL]
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
⊢ ∃ z, x = z * z
[PROOFSTEP]
rcases exists_pow_nat_eq x zero_lt_two with ⟨z, rfl⟩
[GOAL]
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1
[PROOFSTEP]
exact ⟨z, sq z⟩
[GOAL]
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
⊢ roots p = 0 ↔ p = ↑C (coeff p 0)
[PROOFSTEP]
refine' ⟨fun h => _, fun hp => by rw [hp, roots_C]⟩
[GOAL]
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
hp : p = ↑C (coeff p 0)
⊢ roots p = 0
[PROOFSTEP]
rw [hp, roots_C]
[GOAL]
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
cases' le_or_lt (degree p) 0 with hd hd
[GOAL]
case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : degree p ≤ 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
exact eq_C_of_degree_le_zero hd
[GOAL]
case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
obtain ⟨z, hz⟩ := IsAlgClosed.exists_root p hd.ne'
[GOAL]
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
z : k
hz : IsRoot p z
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
[GOAL]
case inr.intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
h : roots p = 0
hd : 0 < degree p
z : k
hz : z ∈ 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
simp at hz
[GOAL]
k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ↑f
p : R[X]
hp : degree p ≠ 0
⊢ degree (map f p) ≠ 0
[PROOFSTEP]
rwa [degree_map_eq_of_injective hf]
[GOAL]
k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ↑f
p : R[X]
hp : degree p ≠ 0
x : k
hx : IsRoot (map f p) x
⊢ eval₂ f x p = 0
[PROOFSTEP]
rwa [eval₂_eq_eval_map, ← IsRoot]
[GOAL]
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
⊢ IsAlgClosed k
[PROOFSTEP]
refine ⟨fun p ↦ Or.inr ?_⟩
[GOAL]
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p : k[X]
⊢ ∀ {g : k[X]}, Irreducible g → g ∣ map (RingHom.id k) p → degree g = 1
[PROOFSTEP]
intro q hq _
[GOAL]
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ degree q = 1
[PROOFSTEP]
have : Irreducible (q * C (leadingCoeff q)⁻¹) :=
  by
  rw [← coe_normUnit_of_ne_zero hq.ne_zero]
  exact (associated_normalize _).irreducible hq
[GOAL]
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * ↑C (leadingCoeff q)⁻¹)
[PROOFSTEP]
rw [← coe_normUnit_of_ne_zero hq.ne_zero]
[GOAL]
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
⊢ Irreducible (q * ↑(normUnit q))
[PROOFSTEP]
exact (associated_normalize _).irreducible hq
[GOAL]
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
⊢ degree q = 1
[PROOFSTEP]
obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) this
[GOAL]
case intro
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Monic p → Irreducible p → ∃ x, eval x p = 0
p q : k[X]
hq : Irreducible q
a✝ : q ∣ map (RingHom.id k) p
this : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
x : k
hx : eval x (q * ↑C (leadingCoeff q)⁻¹) = 0
⊢ degree q = 1
[PROOFSTEP]
exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx
[GOAL]
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)
[PROOFSTEP]
refine' fun x => ⟨-(minpoly k x).coeff 0, _⟩
[GOAL]
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
[PROOFSTEP]
have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (hf x)
[GOAL]
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
[PROOFSTEP]
have h : (minpoly k x).degree = 1 := degree_eq_one_of_irreducible k (minpoly.irreducible (hf x))
[GOAL]
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
[PROOFSTEP]
have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
[GOAL]
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
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
h : E₁ ≤ E₂
⊢ ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x
[PROOFSTEP]
rw [le_def] at h
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
h✝ : E₁ ≤ E₂
h : ∃ h, ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion h) x) = ↑E₁.emb x
⊢ ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x
[PROOFSTEP]
cases h
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
h : E₁ ≤ E₂
w✝ : E₁.carrier ≤ E₂.carrier
h✝ : ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion w✝) x) = ↑E₁.emb x
⊢ ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x
[PROOFSTEP]
assumption
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ E : SubfieldWithHom K L M
⊢ ∀ (x : { x // x ∈ E.carrier }), ↑E.emb (↑(inclusion (_ : E.carrier ≤ E.carrier)) x) = ↑E.emb x
[PROOFSTEP]
simp
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁✝ E₂✝ E₃✝ E₁ E₂ E₃ : SubfieldWithHom K L M
h₁₂ : E₁ ≤ E₂
h₂₃ : E₂ ≤ E₃
⊢ E₁ ≤ E₃
[PROOFSTEP]
refine ⟨h₁₂.1.trans h₂₃.1, fun _ ↦ ?_⟩
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁✝ E₂✝ E₃✝ E₁ E₂ E₃ : SubfieldWithHom K L M
h₁₂ : E₁ ≤ E₂
h₂₃ : E₂ ≤ E₃
x✝ : { x // x ∈ E₁.carrier }
⊢ ↑E₃.emb (↑(inclusion (_ : E₁.carrier ≤ E₃.carrier)) x✝) = ↑E₁.emb x✝
[PROOFSTEP]
erw [← inclusion_inclusion h₁₂.fst h₂₃.fst, compat h₂₃, compat h₁₂]
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
by_cases hcn : c.Nonempty
[GOAL]
case pos
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
case neg
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : ¬Set.Nonempty c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
case neg => rw [Set.not_nonempty_iff_eq_empty] at hcn ; simp [hcn]
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : ¬Set.Nonempty c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
case neg => rw [Set.not_nonempty_iff_eq_empty] at hcn ; simp [hcn]
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : ¬Set.Nonempty c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
rw [Set.not_nonempty_iff_eq_empty] at hcn
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : c = ∅
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
simp [hcn]
[GOAL]
case pos
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
case pos =>
  have : Nonempty c := Set.Nonempty.to_subtype hcn
  let ub : SubfieldWithHom K L M :=
    ⟨⨆ i : c, (i : SubfieldWithHom K L M).carrier,
      @Subalgebra.iSupLift _ _ _ _ _ _ _ _ _ this (fun i : c => (i : SubfieldWithHom K L M).carrier)
        (fun i j =>
          let ⟨k, hik, hjk⟩ := directedOn_iff_directed.1 hc.directedOn i j
          ⟨k, hik.fst, hjk.fst⟩)
        (fun i => (i : SubfieldWithHom K L M).emb)
        (by
          intro i j h
          ext x
          cases' hc.total i.prop j.prop with hij hji
          · simp [← hij.snd x]
          · erw [AlgHom.comp_apply, ← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x])
        _ rfl⟩
  exact
    ⟨ub, fun N hN =>
      ⟨(le_iSup (fun i : c => (i : SubfieldWithHom K L M).carrier) ⟨N, hN⟩ : _),
        by
        intro x
        simp⟩⟩
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
case pos =>
  have : Nonempty c := Set.Nonempty.to_subtype hcn
  let ub : SubfieldWithHom K L M :=
    ⟨⨆ i : c, (i : SubfieldWithHom K L M).carrier,
      @Subalgebra.iSupLift _ _ _ _ _ _ _ _ _ this (fun i : c => (i : SubfieldWithHom K L M).carrier)
        (fun i j =>
          let ⟨k, hik, hjk⟩ := directedOn_iff_directed.1 hc.directedOn i j
          ⟨k, hik.fst, hjk.fst⟩)
        (fun i => (i : SubfieldWithHom K L M).emb)
        (by
          intro i j h
          ext x
          cases' hc.total i.prop j.prop with hij hji
          · simp [← hij.snd x]
          · erw [AlgHom.comp_apply, ← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x])
        _ rfl⟩
  exact
    ⟨ub, fun N hN =>
      ⟨(le_iSup (fun i : c => (i : SubfieldWithHom K L M).carrier) ⟨N, hN⟩ : _),
        by
        intro x
        simp⟩⟩
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
have : Nonempty c := Set.Nonempty.to_subtype hcn
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
let ub : SubfieldWithHom K L M :=
  ⟨⨆ i : c, (i : SubfieldWithHom K L M).carrier,
    @Subalgebra.iSupLift _ _ _ _ _ _ _ _ _ this (fun i : c => (i : SubfieldWithHom K L M).carrier)
      (fun i j =>
        let ⟨k, hik, hjk⟩ := directedOn_iff_directed.1 hc.directedOn i j
        ⟨k, hik.fst, hjk.fst⟩)
      (fun i => (i : SubfieldWithHom K L M).emb)
      (by
        intro i j h
        ext x
        cases' hc.total i.prop j.prop with hij hji
        · simp [← hij.snd x]
        · erw [AlgHom.comp_apply, ← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x])
      _ rfl⟩
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
⊢ ∀ (i j : ↑c) (h : (fun i => (↑i).carrier) i ≤ (fun i => (↑i).carrier) j),
    (fun i => (↑i).emb) i = AlgHom.comp ((fun i => (↑i).emb) j) (inclusion h)
[PROOFSTEP]
intro i j h
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
i j : ↑c
h : (fun i => (↑i).carrier) i ≤ (fun i => (↑i).carrier) j
⊢ (fun i => (↑i).emb) i = AlgHom.comp ((fun i => (↑i).emb) j) (inclusion h)
[PROOFSTEP]
ext x
[GOAL]
case H
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
i j : ↑c
h : (fun i => (↑i).carrier) i ≤ (fun i => (↑i).carrier) j
x : { x // x ∈ (↑i).carrier }
⊢ ↑((fun i => (↑i).emb) i) x = ↑(AlgHom.comp ((fun i => (↑i).emb) j) (inclusion h)) x
[PROOFSTEP]
cases' hc.total i.prop j.prop with hij hji
[GOAL]
case H.inl
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
i j : ↑c
h : (fun i => (↑i).carrier) i ≤ (fun i => (↑i).carrier) j
x : { x // x ∈ (↑i).carrier }
hij : ↑i ≤ ↑j
⊢ ↑((fun i => (↑i).emb) i) x = ↑(AlgHom.comp ((fun i => (↑i).emb) j) (inclusion h)) x
[PROOFSTEP]
simp [← hij.snd x]
[GOAL]
case H.inr
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
i j : ↑c
h : (fun i => (↑i).carrier) i ≤ (fun i => (↑i).carrier) j
x : { x // x ∈ (↑i).carrier }
hji : ↑j ≤ ↑i
⊢ ↑((fun i => (↑i).emb) i) x = ↑(AlgHom.comp ((fun i => (↑i).emb) j) (inclusion h)) x
[PROOFSTEP]
erw [AlgHom.comp_apply, ← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x]
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
ub : SubfieldWithHom K L M :=
  { carrier := ⨆ (i : ↑c), (↑i).carrier,
    emb :=
      iSupLift (fun i => (↑i).carrier)
        (_ :
          ∀ (i j : ↑c),
            ∃ z,
              (fun x x_1 => x ≤ x_1) ((fun i => (↑i).carrier) i) ((fun i => (↑i).carrier) z) ∧
                (fun x x_1 => x ≤ x_1) ((fun i => (↑i).carrier) j) ((fun i => (↑i).carrier) z))
        (fun i => (↑i).emb)
        (_ :
          ∀ (i j : ↑c) (h : (fun i => (↑i).carrier) i ≤ (fun i => (↑i).carrier) j),
            (fun i => (↑i).emb) i = AlgHom.comp ((fun i => (↑i).emb) j) (inclusion h))
        (⨆ (i : ↑c), (↑i).carrier) (_ : ⨆ (i : ↑c), (↑i).carrier = ⨆ (i : ↑c), (↑i).carrier) }
⊢ ∃ ub, ∀ (N : SubfieldWithHom K L M), N ∈ c → N ≤ ub
[PROOFSTEP]
exact
  ⟨ub, fun N hN =>
    ⟨(le_iSup (fun i : c => (i : SubfieldWithHom K L M).carrier) ⟨N, hN⟩ : _),
      by
      intro x
      simp⟩⟩
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
ub : SubfieldWithHom K L M :=
  { carrier := ⨆ (i : ↑c), (↑i).carrier,
    emb :=
      iSupLift (fun i => (↑i).carrier)
        (_ :
          ∀ (i j : ↑c),
            ∃ z,
              (fun x x_1 => x ≤ x_1) ((fun i => (↑i).carrier) i) ((fun i => (↑i).carrier) z) ∧
                (fun x x_1 => x ≤ x_1) ((fun i => (↑i).carrier) j) ((fun i => (↑i).carrier) z))
        (fun i => (↑i).emb)
        (_ :
          ∀ (i j : ↑c) (h : (fun i => (↑i).carrier) i ≤ (fun i => (↑i).carrier) j),
            (fun i => (↑i).emb) i = AlgHom.comp ((fun i => (↑i).emb) j) (inclusion h))
        (⨆ (i : ↑c), (↑i).carrier) (_ : ⨆ (i : ↑c), (↑i).carrier = ⨆ (i : ↑c), (↑i).carrier) }
N : SubfieldWithHom K L M
hN : N ∈ c
⊢ ∀ (x : { x // x ∈ N.carrier }),
    ↑ub.emb (↑(inclusion (_ : (↑{ val := N, property := hN }).carrier ≤ ⨆ (i : ↑c), (↑i).carrier)) x) = ↑N.emb x
[PROOFSTEP]
intro x
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
c : Set (SubfieldWithHom K L M)
hc : IsChain (fun x x_1 => x ≤ x_1) c
hcn : Set.Nonempty c
this : Nonempty ↑c
ub : SubfieldWithHom K L M :=
  { carrier := ⨆ (i : ↑c), (↑i).carrier,
    emb :=
      iSupLift (fun i => (↑i).carrier)
        (_ :
          ∀ (i j : ↑c),
            ∃ z,
              (fun x x_1 => x ≤ x_1) ((fun i => (↑i).carrier) i) ((fun i => (↑i).carrier) z) ∧
                (fun x x_1 => x ≤ x_1) ((fun i => (↑i).carrier) j) ((fun i => (↑i).carrier) z))
        (fun i => (↑i).emb)
        (_ :
          ∀ (i j : ↑c) (h : (fun i => (↑i).carrier) i ≤ (fun i => (↑i).carrier) j),
            (fun i => (↑i).emb) i = AlgHom.comp ((fun i => (↑i).emb) j) (inclusion h))
        (⨆ (i : ↑c), (↑i).carrier) (_ : ⨆ (i : ↑c), (↑i).carrier = ⨆ (i : ↑c), (↑i).carrier) }
N : SubfieldWithHom K L M
hN : N ∈ c
x : { x // x ∈ N.carrier }
⊢ ↑ub.emb (↑(inclusion (_ : (↑{ val := N, property := hN }).carrier ≤ ⨆ (i : ↑c), (↑i).carrier)) x) = ↑N.emb x
[PROOFSTEP]
simp
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
⊢ (maximalSubfieldWithHom K L M).carrier = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
⊢ ⊤ ≤ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
intro x _
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
let N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
letI : Field N := (Subalgebra.isField_of_algebraic N hL).toField
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
letI : Algebra N M := (maximalSubfieldWithHom K L M).emb.toRingHom.toAlgebra
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
obtain ⟨y, hy⟩ :=
  IsAlgClosed.exists_aeval_eq_zero M (minpoly N x) <|
    (minpoly.degree_pos (isAlgebraic_iff_isIntegral.1 (Algebra.isAlgebraic_of_larger_base _ hL x))).ne'
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
let O : Subalgebra N L := Algebra.adjoin N {(x : L)}
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
letI : Algebra N O := Subalgebra.algebra O
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
let larger_emb : O →ₐ[N] M := Algebra.adjoin.liftSingleton N x y hy
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
let larger_emb' : O →ₐ[K] M := AlgHom.restrictScalars K (S := N) (A := O) (B := M) larger_emb
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
have hNO : N ≤ O.restrictScalars K := by
  intro z hz
  show algebraMap N L ⟨z, hz⟩ ∈ O
  exact O.algebraMap_mem _
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
⊢ N ≤ Subalgebra.restrictScalars K O
[PROOFSTEP]
intro z hz
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
z : L
hz : z ∈ N
⊢ z ∈ Subalgebra.restrictScalars K O
[PROOFSTEP]
show algebraMap N L ⟨z, hz⟩ ∈ O
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
z : L
hz : z ∈ N
⊢ ↑(algebraMap { x // x ∈ N } L) { val := z, property := hz } ∈ O
[PROOFSTEP]
exact O.algebraMap_mem _
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
let O' : SubfieldWithHom K L M := ⟨O.restrictScalars K, larger_emb'⟩
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
have hO' : maximalSubfieldWithHom K L M ≤ O' := by
  refine' ⟨hNO, _⟩
  intro z
  show Algebra.adjoin.liftSingleton N x y hy (@algebraMap N O _ _ (Subalgebra.algebra O) z) = algebraMap N M z
  exact AlgHom.commutes _ _
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
⊢ maximalSubfieldWithHom K L M ≤ O'
[PROOFSTEP]
refine' ⟨hNO, _⟩
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
⊢ ∀ (x : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }),
    ↑O'.emb (↑(inclusion hNO) x) = ↑(maximalSubfieldWithHom K L M).emb x
[PROOFSTEP]
intro z
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
z : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }
⊢ ↑O'.emb (↑(inclusion hNO) z) = ↑(maximalSubfieldWithHom K L M).emb z
[PROOFSTEP]
show Algebra.adjoin.liftSingleton N x y hy (@algebraMap N O _ _ (Subalgebra.algebra O) z) = algebraMap N M z
[GOAL]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
z : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }
⊢ ↑(Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy) (↑(algebraMap { x // x ∈ N } { x // x ∈ O }) z) =
    ↑(algebraMap { x // x ∈ N } M) z
[PROOFSTEP]
exact AlgHom.commutes _ _
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
[PROOFSTEP]
refine' (maximalSubfieldWithHom_is_maximal K L M O' hO').fst _
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ O'.carrier
[PROOFSTEP]
show x ∈ Algebra.adjoin N {(x : L)}
[GOAL]
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ Algebra.adjoin { x // x ∈ N } {x}
[PROOFSTEP]
exact Algebra.subset_adjoin (Set.mem_singleton x)
[GOAL]
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
[PROOFSTEP]
letI : IsDomain R := (NoZeroSMulDivisors.algebraMap_injective R S).isDomain _
[GOAL]
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
[PROOFSTEP]
intro
[GOAL]
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
x✝ : FractionRing S
⊢ IsAlgebraic (FractionRing R) x✝
[PROOFSTEP]
exact
  (IsFractionRing.isAlgebraic_iff R (FractionRing R) (FractionRing S)).1
    ((IsFractionRing.isAlgebraic_iff' R S (FractionRing S)).1 hS _)
[GOAL]
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
⊢ S →ₐ[R] M
[PROOFSTEP]
letI : IsDomain R := (NoZeroSMulDivisors.algebraMap_injective R S).isDomain _
[GOAL]
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
⊢ S →ₐ[R] M
[PROOFSTEP]
have : Algebra.IsAlgebraic (FractionRing R) (FractionRing S) := FractionRing.isAlgebraic hS
[GOAL]
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this✝ : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
this : Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
⊢ S →ₐ[R] M
[PROOFSTEP]
let f : FractionRing S →ₐ[FractionRing R] M := lift_aux (FractionRing R) (FractionRing S) M this
[GOAL]
k : Type u
inst✝¹³ : Field k
K : Type u
inst✝¹² : Field K
L : Type v
M : Type w
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Field M
inst✝⁸ : Algebra K M
inst✝⁷ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Algebra R M
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
this✝ : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)
this : Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
f : FractionRing S →ₐ[FractionRing R] M := IsAlgClosed.lift_aux (FractionRing R) (FractionRing S) M this
⊢ S →ₐ[R] M
[PROOFSTEP]
exact (f.restrictScalars R).comp ((Algebra.ofId S (FractionRing S)).restrictScalars R)
[GOAL]
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
⊢ Infinite K
[PROOFSTEP]
apply Infinite.of_not_fintype
[GOAL]
case h
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
⊢ Fintype K → False
[PROOFSTEP]
intro hfin
[GOAL]
case h
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
⊢ False
[PROOFSTEP]
set n := Fintype.card K
[GOAL]
case h
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
⊢ False
[PROOFSTEP]
set f := (X : K[X]) ^ (n + 1) - 1
[GOAL]
case h
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
⊢ False
[PROOFSTEP]
have hfsep : Separable f := separable_X_pow_sub_C 1 (by simp) one_ne_zero
[GOAL]
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
⊢ ↑(n + 1) ≠ 0
[PROOFSTEP]
simp
[GOAL]
case h
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : Separable f
⊢ False
[PROOFSTEP]
apply Nat.not_succ_le_self (Fintype.card K)
[GOAL]
case h
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : Separable f
⊢ Nat.succ (Fintype.card K) ≤ Fintype.card K
[PROOFSTEP]
have hroot : n.succ = Fintype.card (f.rootSet K) := by
  erw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _), natDegree_X_pow_sub_C]
[GOAL]
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : Separable f
⊢ Nat.succ n = Fintype.card ↑(rootSet f K)
[PROOFSTEP]
erw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _), natDegree_X_pow_sub_C]
[GOAL]
case h
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : Separable f
hroot : Nat.succ n = Fintype.card ↑(rootSet f K)
⊢ Nat.succ (Fintype.card K) ≤ Fintype.card K
[PROOFSTEP]
rw [hroot]
[GOAL]
case h
k : Type u
inst✝¹⁵ : Field k
K✝ : Type u
inst✝¹⁴ : Field K✝
L : Type v
M : Type w
inst✝¹³ : Field L
inst✝¹² : Algebra K✝ L
inst✝¹¹ : Field M
inst✝¹⁰ : Algebra K✝ M
inst✝⁹ : IsAlgClosed M
hL : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝⁸ : CommRing R
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R M
inst✝³ : NoZeroSMulDivisors R S
inst✝² : NoZeroSMulDivisors R M
hS : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : Separable f
hroot : Nat.succ n = Fintype.card ↑(rootSet f K)
⊢ Fintype.card ↑(rootSet f K) ≤ Fintype.card K
[PROOFSTEP]
exact Fintype.card_le_of_injective _ Subtype.coe_injective
[GOAL]
k : Type u
inst✝⁹ : Field k
R : Type u
inst✝⁸ : CommRing R
L : Type v
M : Type w
inst✝⁷ : Field L
inst✝⁶ : Field M
inst✝⁵ : Algebra R M
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : IsAlgClosure R M
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : IsAlgClosure R L
this : IsAlgClosed M
f : L →ₐ[R] M := IsAlgClosed.lift (_ : Algebra.IsAlgebraic R L)
⊢ Function.Surjective ↑f
[PROOFSTEP]
letI : Algebra L M := RingHom.toAlgebra f
[GOAL]
k : Type u
inst✝⁹ : Field k
R : Type u
inst✝⁸ : CommRing R
L : Type v
M : Type w
inst✝⁷ : Field L
inst✝⁶ : Field M
inst✝⁵ : Algebra R M
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : IsAlgClosure R M
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : IsAlgClosure R L
this✝ : IsAlgClosed M
f : L →ₐ[R] M := IsAlgClosed.lift (_ : Algebra.IsAlgebraic R L)
this : Algebra L M := RingHom.toAlgebra ↑f
⊢ Function.Surjective ↑f
[PROOFSTEP]
letI : IsScalarTower R L M :=
  IsScalarTower.of_algebraMap_eq <| by
    simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_coe, AlgHom.commutes, forall_const]
[GOAL]
k : Type u
inst✝⁹ : Field k
R : Type u
inst✝⁸ : CommRing R
L : Type v
M : Type w
inst✝⁷ : Field L
inst✝⁶ : Field M
inst✝⁵ : Algebra R M
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : IsAlgClosure R M
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : IsAlgClosure R L
this✝ : IsAlgClosed M
f : L →ₐ[R] M := IsAlgClosed.lift (_ : Algebra.IsAlgebraic R L)
this : Algebra L M := RingHom.toAlgebra ↑f
⊢ ∀ (x : R), ↑(algebraMap R M) x = ↑(algebraMap L M) (↑(algebraMap R L) x)
[PROOFSTEP]
simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_coe, AlgHom.commutes, forall_const]
[GOAL]
k : Type u
inst✝⁹ : Field k
R : Type u
inst✝⁸ : CommRing R
L : Type v
M : Type w
inst✝⁷ : Field L
inst✝⁶ : Field M
inst✝⁵ : Algebra R M
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : IsAlgClosure R M
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : IsAlgClosure R L
this✝¹ : IsAlgClosed M
f : L →ₐ[R] M := IsAlgClosed.lift (_ : Algebra.IsAlgebraic R L)
this✝ : Algebra L M := RingHom.toAlgebra ↑f
this : IsScalarTower R L M :=
  IsScalarTower.of_algebraMap_eq
    (of_eq_true
      (Eq.trans
        (forall_congr fun x =>
          Eq.trans (congrArg (Eq (↑(algebraMap R M) x)) (AlgHom.commutes (IsAlgClosed.lift algebraic) x))
            (eq_self (↑(algebraMap R M) x)))
        (_auxLemma.3 R)))
⊢ Function.Surjective ↑f
[PROOFSTEP]
letI : IsAlgClosed L := IsAlgClosure.alg_closed R
[GOAL]
k : Type u
inst✝⁹ : Field k
R : Type u
inst✝⁸ : CommRing R
L : Type v
M : Type w
inst✝⁷ : Field L
inst✝⁶ : Field M
inst✝⁵ : Algebra R M
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : IsAlgClosure R M
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : IsAlgClosure R L
this✝² : IsAlgClosed M
f : L →ₐ[R] M := IsAlgClosed.lift (_ : Algebra.IsAlgebraic R L)
this✝¹ : Algebra L M := RingHom.toAlgebra ↑f
this✝ : IsScalarTower R L M :=
  IsScalarTower.of_algebraMap_eq
    (of_eq_true
      (Eq.trans
        (forall_congr fun x =>
          Eq.trans (congrArg (Eq (↑(algebraMap R M) x)) (AlgHom.commutes (IsAlgClosed.lift algebraic) x))
            (eq_self (↑(algebraMap R M) x)))
        (_auxLemma.3 R)))
this : IsAlgClosed L := alg_closed R
⊢ Function.Surjective ↑f
[PROOFSTEP]
show Function.Surjective (algebraMap L M)
[GOAL]
k : Type u
inst✝⁹ : Field k
R : Type u
inst✝⁸ : CommRing R
L : Type v
M : Type w
inst✝⁷ : Field L
inst✝⁶ : Field M
inst✝⁵ : Algebra R M
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : IsAlgClosure R M
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : IsAlgClosure R L
this✝² : IsAlgClosed M
f : L →ₐ[R] M := IsAlgClosed.lift (_ : Algebra.IsAlgebraic R L)
this✝¹ : Algebra L M := RingHom.toAlgebra ↑f
this✝ : IsScalarTower R L M :=
  IsScalarTower.of_algebraMap_eq
    (of_eq_true
      (Eq.trans
        (forall_congr fun x =>
          Eq.trans (congrArg (Eq (↑(algebraMap R M) x)) (AlgHom.commutes (IsAlgClosed.lift algebraic) x))
            (eq_self (↑(algebraMap R M) x)))
        (_auxLemma.3 R)))
this : IsAlgClosed L := alg_closed R
⊢ Function.Surjective ↑(algebraMap L M)
[PROOFSTEP]
exact
  IsAlgClosed.algebraMap_surjective_of_isAlgebraic
    (Algebra.isAlgebraic_of_larger_base_of_injective (NoZeroSMulDivisors.algebraMap_injective R _)
      IsAlgClosure.algebraic)
[GOAL]
k : Type u
inst✝²⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²³ : Field K
inst✝²² : Field J
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Field L
inst✝¹⁸ : Field M
inst✝¹⁷ : Algebra R M
inst✝¹⁶ : NoZeroSMulDivisors R M
inst✝¹⁵ : IsAlgClosure R M
inst✝¹⁴ : Algebra K M
inst✝¹³ : IsAlgClosure K M
inst✝¹² : Algebra S L
inst✝¹¹ : NoZeroSMulDivisors S L
inst✝¹⁰ : IsAlgClosure S L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : Algebra K J
inst✝⁵ : Algebra J L
inst✝⁴ : IsAlgClosure J L
inst✝³ : Algebra K L
inst✝² : IsScalarTower K J L
inst✝¹ : Nontrivial S
inst✝ : NoZeroSMulDivisors R S
hRL : Algebra.IsAlgebraic R L
⊢ L ≃ₐ[R] M
[PROOFSTEP]
letI : NoZeroSMulDivisors R L :=
  NoZeroSMulDivisors.of_algebraMap_injective <|
    by
    rw [IsScalarTower.algebraMap_eq R S L]
    exact
      (Function.Injective.comp (NoZeroSMulDivisors.algebraMap_injective S L)
          (NoZeroSMulDivisors.algebraMap_injective R S) :
        _)
[GOAL]
k : Type u
inst✝²⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²³ : Field K
inst✝²² : Field J
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Field L
inst✝¹⁸ : Field M
inst✝¹⁷ : Algebra R M
inst✝¹⁶ : NoZeroSMulDivisors R M
inst✝¹⁵ : IsAlgClosure R M
inst✝¹⁴ : Algebra K M
inst✝¹³ : IsAlgClosure K M
inst✝¹² : Algebra S L
inst✝¹¹ : NoZeroSMulDivisors S L
inst✝¹⁰ : IsAlgClosure S L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : Algebra K J
inst✝⁵ : Algebra J L
inst✝⁴ : IsAlgClosure J L
inst✝³ : Algebra K L
inst✝² : IsScalarTower K J L
inst✝¹ : Nontrivial S
inst✝ : NoZeroSMulDivisors R S
hRL : Algebra.IsAlgebraic R L
⊢ Function.Injective ↑(algebraMap R L)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq R S L]
[GOAL]
k : Type u
inst✝²⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²³ : Field K
inst✝²² : Field J
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Field L
inst✝¹⁸ : Field M
inst✝¹⁷ : Algebra R M
inst✝¹⁶ : NoZeroSMulDivisors R M
inst✝¹⁵ : IsAlgClosure R M
inst✝¹⁴ : Algebra K M
inst✝¹³ : IsAlgClosure K M
inst✝¹² : Algebra S L
inst✝¹¹ : NoZeroSMulDivisors S L
inst✝¹⁰ : IsAlgClosure S L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : Algebra K J
inst✝⁵ : Algebra J L
inst✝⁴ : IsAlgClosure J L
inst✝³ : Algebra K L
inst✝² : IsScalarTower K J L
inst✝¹ : Nontrivial S
inst✝ : NoZeroSMulDivisors R S
hRL : Algebra.IsAlgebraic R L
⊢ Function.Injective ↑(RingHom.comp (algebraMap S L) (algebraMap R S))
[PROOFSTEP]
exact
  (Function.Injective.comp (NoZeroSMulDivisors.algebraMap_injective S L) (NoZeroSMulDivisors.algebraMap_injective R S) :
    _)
[GOAL]
k : Type u
inst✝²⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²³ : Field K
inst✝²² : Field J
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Field L
inst✝¹⁸ : Field M
inst✝¹⁷ : Algebra R M
inst✝¹⁶ : NoZeroSMulDivisors R M
inst✝¹⁵ : IsAlgClosure R M
inst✝¹⁴ : Algebra K M
inst✝¹³ : IsAlgClosure K M
inst✝¹² : Algebra S L
inst✝¹¹ : NoZeroSMulDivisors S L
inst✝¹⁰ : IsAlgClosure S L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : Algebra K J
inst✝⁵ : Algebra J L
inst✝⁴ : IsAlgClosure J L
inst✝³ : Algebra K L
inst✝² : IsScalarTower K J L
inst✝¹ : Nontrivial S
inst✝ : NoZeroSMulDivisors R S
hRL : Algebra.IsAlgebraic R L
this : NoZeroSMulDivisors R L :=
  NoZeroSMulDivisors.of_algebraMap_injective
    (Eq.mpr (id (IsScalarTower.algebraMap_eq R S L ▸ Eq.refl (Function.Injective ↑(algebraMap R L))))
      (Function.Injective.comp (NoZeroSMulDivisors.algebraMap_injective S L)
        (NoZeroSMulDivisors.algebraMap_injective R S)))
⊢ L ≃ₐ[R] M
[PROOFSTEP]
letI : IsAlgClosure R L :=
  { alg_closed := IsAlgClosure.alg_closed S
    algebraic := hRL }
[GOAL]
k : Type u
inst✝²⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²³ : Field K
inst✝²² : Field J
inst✝²¹ : CommRing R
inst✝²⁰ : CommRing S
inst✝¹⁹ : Field L
inst✝¹⁸ : Field M
inst✝¹⁷ : Algebra R M
inst✝¹⁶ : NoZeroSMulDivisors R M
inst✝¹⁵ : IsAlgClosure R M
inst✝¹⁴ : Algebra K M
inst✝¹³ : IsAlgClosure K M
inst✝¹² : Algebra S L
inst✝¹¹ : NoZeroSMulDivisors S L
inst✝¹⁰ : IsAlgClosure S L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : Algebra K J
inst✝⁵ : Algebra J L
inst✝⁴ : IsAlgClosure J L
inst✝³ : Algebra K L
inst✝² : IsScalarTower K J L
inst✝¹ : Nontrivial S
inst✝ : NoZeroSMulDivisors R S
hRL : Algebra.IsAlgebraic R L
this✝ : NoZeroSMulDivisors R L :=
  NoZeroSMulDivisors.of_algebraMap_injective
    (Eq.mpr (id (IsScalarTower.algebraMap_eq R S L ▸ Eq.refl (Function.Injective ↑(algebraMap R L))))
      (Function.Injective.comp (NoZeroSMulDivisors.algebraMap_injective S L)
        (NoZeroSMulDivisors.algebraMap_injective R S)))
this : IsAlgClosure R L := { alg_closed := alg_closed S, algebraic := hRL }
⊢ L ≃ₐ[R] M
[PROOFSTEP]
exact IsAlgClosure.equiv _ _ _
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
letI : Algebra R S := RingHom.toAlgebra hSR.symm.toRingHom
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
letI : Algebra S R := RingHom.toAlgebra hSR.toRingHom
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
letI : IsDomain R := (NoZeroSMulDivisors.algebraMap_injective R M).isDomain _
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝¹ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
letI : IsDomain S := (NoZeroSMulDivisors.algebraMap_injective S L).isDomain _
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝² : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝¹ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
letI : Algebra R L := RingHom.toAlgebra ((algebraMap S L).comp (algebraMap R S))
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝³ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝² : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝¹ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
haveI : IsScalarTower R S L := IsScalarTower.of_algebraMap_eq fun _ => rfl
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁴ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝³ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝² : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝¹ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝ : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this : IsScalarTower R S L
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
haveI : IsScalarTower S R L := IsScalarTower.of_algebraMap_eq (by simp [RingHom.algebraMap_toAlgebra])
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁴ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝³ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝² : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝¹ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝ : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this : IsScalarTower R S L
⊢ ∀ (x : S), ↑(algebraMap S L) x = ↑(algebraMap R L) (↑(algebraMap S R) x)
[PROOFSTEP]
simp [RingHom.algebraMap_toAlgebra]
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁵ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁴ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝³ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝² : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝¹ : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝ : IsScalarTower R S L
this : IsScalarTower S R L
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
haveI : NoZeroSMulDivisors R S := NoZeroSMulDivisors.of_algebraMap_injective hSR.symm.injective
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
⊢ { e //
    RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }
[PROOFSTEP]
refine'
  ⟨equivOfAlgebraic' R S L M
      (Algebra.isAlgebraic_of_larger_base_of_injective (show Function.Injective (algebraMap S R) from hSR.injective)
        IsAlgClosure.algebraic),
    _⟩
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
⊢ RingHom.comp (RingEquiv.toRingHom ↑(equivOfAlgebraic' R S L M (_ : Algebra.IsAlgebraic R L))) (algebraMap S L) =
    RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR)
[PROOFSTEP]
ext x
[GOAL]
case a
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
x : S
⊢ ↑(RingHom.comp (RingEquiv.toRingHom ↑(equivOfAlgebraic' R S L M (_ : Algebra.IsAlgebraic R L))) (algebraMap S L)) x =
    ↑(RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR)) x
[PROOFSTEP]
simp only [RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingHom.coe_comp, AlgEquiv.coe_ringEquiv,
  RingEquiv.coe_toRingHom]
[GOAL]
case a
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
x : S
⊢ ↑(equivOfAlgebraic' R S L M (_ : Algebra.IsAlgebraic R L)) (↑(algebraMap S L) x) = ↑(algebraMap R M) (↑hSR x)
[PROOFSTEP]
conv_lhs => rw [← hSR.symm_apply_apply x]
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
x : S
| ↑(equivOfAlgebraic' R S L M (_ : Algebra.IsAlgebraic R L)) (↑(algebraMap S L) x)
[PROOFSTEP]
rw [← hSR.symm_apply_apply x]
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
x : S
| ↑(equivOfAlgebraic' R S L M (_ : Algebra.IsAlgebraic R L)) (↑(algebraMap S L) x)
[PROOFSTEP]
rw [← hSR.symm_apply_apply x]
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
x : S
| ↑(equivOfAlgebraic' R S L M (_ : Algebra.IsAlgebraic R L)) (↑(algebraMap S L) x)
[PROOFSTEP]
rw [← hSR.symm_apply_apply x]
[GOAL]
case a
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
x : S
⊢ ↑(equivOfAlgebraic' R S L M (_ : Algebra.IsAlgebraic R L)) (↑(algebraMap S L) (↑(RingEquiv.symm hSR) (↑hSR x))) =
    ↑(algebraMap R M) (↑hSR x)
[PROOFSTEP]
show equivOfAlgebraic' R S L M _ (algebraMap R L (hSR x)) = _
[GOAL]
case a
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
this✝⁶ : Algebra R S := RingHom.toAlgebra (RingEquiv.toRingHom (RingEquiv.symm hSR))
this✝⁵ : Algebra S R := RingHom.toAlgebra (RingEquiv.toRingHom hSR)
this✝⁴ : IsDomain R := Function.Injective.isDomain (algebraMap R M) (NoZeroSMulDivisors.algebraMap_injective R M)
this✝³ : IsDomain S := Function.Injective.isDomain (algebraMap S L) (NoZeroSMulDivisors.algebraMap_injective S L)
this✝² : Algebra R L := RingHom.toAlgebra (RingHom.comp (algebraMap S L) (algebraMap R S))
this✝¹ : IsScalarTower R S L
this✝ : IsScalarTower S R L
this : NoZeroSMulDivisors R S
x : S
⊢ ↑(equivOfAlgebraic' R S L M (_ : Algebra.IsAlgebraic R L)) (↑(algebraMap R L) (↑hSR x)) = ↑(algebraMap R M) (↑hSR x)
[PROOFSTEP]
rw [AlgEquiv.commutes]
[GOAL]
k : Type u
inst✝¹⁴ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹³ : Field K
inst✝¹² : Field J
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : NoZeroSMulDivisors R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra K M
inst✝³ : IsAlgClosure K M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
r : R
⊢ ↑(equivOfEquiv L M hSR) (↑(RingEquiv.symm (equivOfEquiv L M hSR)) (↑(algebraMap R M) r)) =
    ↑(equivOfEquiv L M hSR) (↑(algebraMap S L) (↑(RingEquiv.symm hSR) r))
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
have hFK := Algebra.isAlgebraic_iff_isIntegral.1 hK
[GOAL]
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
[PROOFSTEP]
ext a
[GOAL]
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
[PROOFSTEP]
rw [mem_rootSet_of_ne (minpoly.ne_zero (hFK x))]
[GOAL]
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
[PROOFSTEP]
refine' ⟨_, fun ha => _⟩
[GOAL]
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
[PROOFSTEP]
rintro ⟨ψ, rfl⟩
[GOAL]
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
[PROOFSTEP]
rw [aeval_algHom_apply ψ x, minpoly.aeval, map_zero]
[GOAL]
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
[PROOFSTEP]
let Fx := AdjoinRoot (minpoly F x)
[GOAL]
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
[PROOFSTEP]
have hx : aeval x (minpoly F x) = 0 := minpoly.aeval F x
[GOAL]
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
[PROOFSTEP]
letI : Algebra Fx A := (AdjoinRoot.lift (algebraMap F A) a ha).toAlgebra
[GOAL]
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
[PROOFSTEP]
letI : Algebra Fx K := (AdjoinRoot.lift (algebraMap F K) x hx).toAlgebra
[GOAL]
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
[PROOFSTEP]
haveI : IsScalarTower F Fx A := IsScalarTower.of_ring_hom (AdjoinRoot.liftHom _ a ha)
[GOAL]
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
[PROOFSTEP]
haveI : IsScalarTower F Fx K := IsScalarTower.of_ring_hom (AdjoinRoot.liftHom _ x hx)
[GOAL]
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
[PROOFSTEP]
haveI : Fact (Irreducible <| minpoly F x) := ⟨minpoly.irreducible <| hFK x⟩
[GOAL]
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
[PROOFSTEP]
let ψ₀ : K →ₐ[Fx] A := IsAlgClosed.lift (Algebra.isAlgebraic_of_larger_base Fx hK)
[GOAL]
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
[PROOFSTEP]
exact
  ⟨ψ₀.restrictScalars F,
    (congr_arg ψ₀ (AdjoinRoot.lift_root hx).symm).trans <| (ψ₀.commutes _).trans <| AdjoinRoot.lift_root ha⟩