F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
⊢ ↑(liftOfSplits x h1 h2).snd u = ↑x.snd t
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
⊢ ↑(liftOfSplits x h1 h2).snd u = ↑x.snd t
let alg : Algebra x.1 x.1⟮s⟯ := x.1⟮s⟯.toSubalgebra.algebra
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
⊢ ↑(liftOfSplits x h1 h2).snd u = ↑x.snd t
rw [← show algebraMap x.1 x.1⟮s⟯ t = u from Subtype.ext htu]
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
letI : Algebra x.1 K := x.2.toRingHom.toAlgebra
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
let I1 : IsIntegral x.1 s := isIntegral_of_isScalarTower h1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
let key : (minpoly x.1 s).Splits x.2.toRingHom :=
  splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero h1))
    ((splits_map_iff _ _).mpr (by convert h2; exact RingHom.ext fun y => x.2.commutes y))
      (minpoly.dvd_map_of_isScalarTower _ _ _)
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
have I2 := (ne_of_gt (minpoly.degree_pos I1))
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
I3 :
  rootOfSplits (↑x.snd) key (_ : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0) ∈
    roots (Polynomial.map (algebraMap { x_1 // x_1 ∈ x.fst } K) (minpoly { x_1 // x_1 ∈ x.fst } s))
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
have I3 : rootOfSplits (AlgHom.toRingHom x.2) key (ne_of_gt (minpoly.degree_pos I1)) ∈
    (Polynomial.map (algebraMap x.1 K) (minpoly x.1 s)).roots := by
  rw [mem_roots (map_ne_zero (minpoly.ne_zero I1)), IsRoot, ← eval₂_eq_eval_map]
  exact map_rootOfSplits x.2.toRingHom key (ne_of_gt (minpoly.degree_pos I1))
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
I3 :
  rootOfSplits (↑x.snd) key (_ : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0) ∈
    roots (Polynomial.map (algebraMap { x_1 // x_1 ∈ x.fst } K) (minpoly { x_1 // x_1 ∈ x.fst } s))
φ : { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } →ₐ[{ x_1 // x_1 ∈ x.fst }] K :=
  Equiv.invFun (algHomAdjoinIntegralEquiv { x_1 // x_1 ∈ x.fst } I1)
    { val := rootOfSplits (↑x.snd) key I2, property := I3 }
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
I3 :
  rootOfSplits (↑x.snd) key (_ : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0) ∈
    roots (Polynomial.map (algebraMap { x_1 // x_1 ∈ x.fst } K) (minpoly { x_1 // x_1 ∈ x.fst } s))
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
let φ : x.1⟮s⟯ →ₐ[x.1] K := ((algHomAdjoinIntegralEquiv x.1 I1).invFun
  ⟨rootOfSplits (AlgHom.toRingHom x.2) key I2, I3⟩)
no goals
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
I3 :
  rootOfSplits (↑x.snd) key (_ : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0) ∈
    roots (Polynomial.map (algebraMap { x_1 // x_1 ∈ x.fst } K) (minpoly { x_1 // x_1 ∈ x.fst } s))
φ : { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } →ₐ[{ x_1 // x_1 ∈ x.fst }] K :=
  Equiv.invFun (algHomAdjoinIntegralEquiv { x_1 // x_1 ∈ x.fst } I1)
    { val := rootOfSplits (↑x.snd) key I2, property := I3 }
⊢ ↑(liftOfSplits x h1 h2).snd (↑(algebraMap { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ }) t) =
    ↑x.snd t
exact AlgHom.commutes φ t
case h.e'_5
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
⊢ RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }) = algebraMap F K
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
⊢ Splits (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst })) (minpoly F s)
convert h2
no goals
case h.e'_5
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
⊢ RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }) = algebraMap F K
exact RingHom.ext fun y => x.2.commutes y
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
⊢ eval₂ (algebraMap { x_1 // x_1 ∈ x.fst } K)
      (rootOfSplits (↑x.snd) key (_ : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0))
      (minpoly { x_1 // x_1 ∈ x.fst } s) =
    0
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
⊢ rootOfSplits (↑x.snd) key (_ : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0) ∈
    roots (Polynomial.map (algebraMap { x_1 // x_1 ∈ x.fst } K) (minpoly { x_1 // x_1 ∈ x.fst } s))
rw [mem_roots (map_ne_zero (minpoly.ne_zero I1)), IsRoot, ← eval₂_eq_eval_map]
no goals
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (algebraMap F K) (minpoly F s)
t : { x_1 // x_1 ∈ x.fst }
u : { x_1 // x_1 ∈ (liftOfSplits x h1 h2).fst }
htu : ↑t = ↑u
alg : Algebra { x_1 // x_1 ∈ x.fst } { x_1 // x_1 ∈ { x_2 // x_2 ∈ x.fst }⟮s⟯ } :=
  Subalgebra.algebra { x_1 // x_1 ∈ x.fst }⟮s⟯.toSubalgebra
this : Algebra { x_1 // x_1 ∈ x.fst } K := RingHom.toAlgebra ↑x.snd
I1 : IsIntegral { x_1 // x_1 ∈ x.fst } s := isIntegral_of_isScalarTower h1
key : Splits (↑x.snd) (minpoly { x_1 // x_1 ∈ x.fst } s) :=
  splits_of_splits_of_dvd (↑x.snd) (Polynomial.map_ne_zero (minpoly.ne_zero h1))
    (Iff.mpr (splits_map_iff (algebraMap F { x_1 // x_1 ∈ x.fst }) ↑x.snd)
      (Eq.mpr
        (eq_of_heq
          ((fun K L inst inst_1 i i' e'_5 f =>
              Eq.casesOn (motive := fun a x => i' = a → HEq e'_5 x → HEq (Splits i f) (Splits i' f)) e'_5
                (fun h =>
                  Eq.ndrec (motive := fun i' => ∀ (e_5 : i = i'), HEq e_5 (Eq.refl i) → HEq (Splits i f) (Splits i' f))
                    (fun e_5 h => Eq.symm (eq_of_heq h) ▸ HEq.refl (Splits i f)) (Eq.symm h) e'_5)
                (Eq.refl i') (HEq.refl e'_5))
            F K EuclideanDomain.toCommRing inst✝² (RingHom.comp (↑x.snd) (algebraMap F { x_1 // x_1 ∈ x.fst }))
            (algebraMap F K) (RingHom.ext fun y => AlgHom.commutes x.snd y) (minpoly F s)))
        h2))
    (minpoly.dvd_map_of_isScalarTower F { x_1 // x_1 ∈ x.fst } s)
I2 : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0
⊢ eval₂ (algebraMap { x_1 // x_1 ∈ x.fst } K)
      (rootOfSplits (↑x.snd) key (_ : degree (minpoly { x_1 // x_1 ∈ x.fst } s) ≠ 0))
      (minpoly { x_1 // x_1 ∈ x.fst } s) =
    0
exact map_rootOfSplits x.2.toRingHom key (ne_of_gt (minpoly.degree_pos I1))