[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
⊢ Fintype.card ({ x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ }) = finrank F { x // x ∈ F⟮α⟯ }
[PROOFSTEP]
letI : Fintype (F⟮α⟯ →ₐ[F] F⟮α⟯) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
this : Fintype ({ x // x ∈ F⟮α⟯ } →ₐ[F] { x // x ∈ F⟮α⟯ }) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card ({ x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ }) = finrank F { x // x ∈ F⟮α⟯ }
[PROOFSTEP]
rw [IntermediateField.adjoin.finrank hα]
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
this : Fintype ({ x // x ∈ F⟮α⟯ } →ₐ[F] { x // x ∈ F⟮α⟯ }) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card ({ x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ }) = Polynomial.natDegree (minpoly F α)
[PROOFSTEP]
rw [← IntermediateField.card_algHom_adjoin_integral F hα h_sep h_splits]
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
this : Fintype ({ x // x ∈ F⟮α⟯ } →ₐ[F] { x // x ∈ F⟮α⟯ }) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card ({ x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ }) = Fintype.card ({ x // x ∈ F⟮α⟯ } →ₐ[F] { x // x ∈ F⟮α⟯ })
[PROOFSTEP]
exact Fintype.card_congr (algEquivEquivAlgHom F F⟮α⟯)
[GOAL]
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
cases' Field.exists_primitive_element F E with α hα
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
let iso : F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e => e.val
    invFun := fun e => ⟨e, by rw [hα]; exact IntermediateField.mem_top⟩
    left_inv := fun _ => by ext; rfl
    right_inv := fun _ => rfl
    map_mul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl
    commutes' := fun _ => rfl }
[GOAL]
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
e : E
⊢ e ∈ F⟮α⟯
[PROOFSTEP]
rw [hα]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
e : E
⊢ e ∈ ⊤
[PROOFSTEP]
exact IntermediateField.mem_top
[GOAL]
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
x✝ : { x // x ∈ F⟮α⟯ }
⊢ (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
x✝ : { x // x ∈ F⟮α⟯ }
⊢ ↑((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x✝)) = ↑x✝
[PROOFSTEP]
rfl
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
have H : IsIntegral F α := IsGalois.integral F α
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
have h_sep : (minpoly F α).Separable := IsGalois.separable F α
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
have h_splits : (minpoly F α).Splits (algebraMap F E) := IsGalois.splits F α
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F E) (minpoly F α)
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
replace h_splits : Polynomial.Splits (algebraMap F F⟮α⟯) (minpoly F α)
[GOAL]
case h_splits
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F E) (minpoly F α)
⊢ Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
[PROOFSTEP]
simpa using Polynomial.splits_comp_of_splits (algebraMap F E) iso.symm.toAlgHom.toRingHom h_splits
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
rw [← LinearEquiv.finrank_eq iso.toLinearEquiv]
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F { x // x ∈ F⟮α⟯ }
[PROOFSTEP]
rw [← IntermediateField.AdjoinSimple.card_aut_eq_finrank F E H h_sep h_splits]
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
⊢ Fintype.card (E ≃ₐ[F] E) = Fintype.card ({ x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ })
[PROOFSTEP]
apply Fintype.card_congr
[GOAL]
case intro.f
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
⊢ (E ≃ₐ[F] E) ≃ { x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ }
[PROOFSTEP]
apply Equiv.mk (fun ϕ => iso.trans (ϕ.trans iso.symm)) fun ϕ => iso.symm.trans (ϕ.trans iso)
[GOAL]
case intro.f.left_inv
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
⊢ Function.LeftInverse (fun ϕ => AlgEquiv.trans (AlgEquiv.symm iso) (AlgEquiv.trans ϕ iso)) fun ϕ =>
    AlgEquiv.trans iso (AlgEquiv.trans ϕ (AlgEquiv.symm iso))
[PROOFSTEP]
intro ϕ
[GOAL]
case intro.f.left_inv
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
ϕ : E ≃ₐ[F] E
⊢ (fun ϕ => AlgEquiv.trans (AlgEquiv.symm iso) (AlgEquiv.trans ϕ iso))
      ((fun ϕ => AlgEquiv.trans iso (AlgEquiv.trans ϕ (AlgEquiv.symm iso))) ϕ) =
    ϕ
[PROOFSTEP]
ext1
[GOAL]
case intro.f.left_inv.h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
ϕ : E ≃ₐ[F] E
a✝ : E
⊢ ↑((fun ϕ => AlgEquiv.trans (AlgEquiv.symm iso) (AlgEquiv.trans ϕ iso))
          ((fun ϕ => AlgEquiv.trans iso (AlgEquiv.trans ϕ (AlgEquiv.symm iso))) ϕ))
      a✝ =
    ↑ϕ a✝
[PROOFSTEP]
simp only [trans_apply, apply_symm_apply]
[GOAL]
case intro.f.right_inv
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
⊢ Function.RightInverse (fun ϕ => AlgEquiv.trans (AlgEquiv.symm iso) (AlgEquiv.trans ϕ iso)) fun ϕ =>
    AlgEquiv.trans iso (AlgEquiv.trans ϕ (AlgEquiv.symm iso))
[PROOFSTEP]
intro ϕ
[GOAL]
case intro.f.right_inv
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
ϕ : { x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ }
⊢ (fun ϕ => AlgEquiv.trans iso (AlgEquiv.trans ϕ (AlgEquiv.symm iso)))
      ((fun ϕ => AlgEquiv.trans (AlgEquiv.symm iso) (AlgEquiv.trans ϕ iso)) ϕ) =
    ϕ
[PROOFSTEP]
ext1
[GOAL]
case intro.f.right_inv.h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : { x // x ∈ F⟮α⟯ } ≃ₐ[F] E :=
  {
    toEquiv :=
      { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
        left_inv :=
          (_ : ∀ (x : { x // x ∈ F⟮α⟯ }), (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
        right_inv :=
          (_ :
            ∀ (x : E),
              (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) },
    map_mul' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x * x_1)),
    map_add' :=
      (_ :
        ∀ (x x_1 : { x // x ∈ F⟮α⟯ }),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (x + x_1)),
    commutes' :=
      (_ :
        ∀ (x : F),
          Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x) =
            Equiv.toFun
              { toFun := fun e => ↑e, invFun := fun e => { val := e, property := (_ : e ∈ F⟮α⟯) },
                left_inv :=
                  (_ :
                    ∀ (x : { x // x ∈ F⟮α⟯ }),
                      (fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) ((fun e => ↑e) x) = x),
                right_inv :=
                  (_ :
                    ∀ (x : E),
                      (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x) =
                        (fun e => ↑e) ((fun e => { val := e, property := (_ : e ∈ F⟮α⟯) }) x)) }
              (↑(algebraMap F { x // x ∈ F⟮α⟯ }) x)) }
H : IsIntegral F α
h_sep : Polynomial.Separable (minpoly F α)
h_splits : Polynomial.Splits (algebraMap F { x // x ∈ F⟮α⟯ }) (minpoly F α)
ϕ : { x // x ∈ F⟮α⟯ } ≃ₐ[F] { x // x ∈ F⟮α⟯ }
a✝ : { x // x ∈ F⟮α⟯ }
⊢ ↑((fun ϕ => AlgEquiv.trans iso (AlgEquiv.trans ϕ (AlgEquiv.symm iso)))
          ((fun ϕ => AlgEquiv.trans (AlgEquiv.symm iso) (AlgEquiv.trans ϕ iso)) ϕ))
      a✝ =
    ↑ϕ a✝
[PROOFSTEP]
simp only [trans_apply, symm_apply_apply]
[GOAL]
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Field E
E' : Type u_4
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E'
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
⊢ IsGalois { x // x ∈ ⊥ } E ↔ IsGalois F E
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Field E
E' : Type u_4
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E'
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
⊢ IsGalois { x // x ∈ ⊥ } E → IsGalois F E
[PROOFSTEP]
intro h
[GOAL]
case mp
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Field E
E' : Type u_4
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E'
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsGalois { x // x ∈ ⊥ } E
⊢ IsGalois F E
[PROOFSTEP]
exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E
[GOAL]
case mpr
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Field E
E' : Type u_4
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E'
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
⊢ IsGalois F E → IsGalois { x // x ∈ ⊥ } E
[PROOFSTEP]
intro h
[GOAL]
case mpr
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field K
inst✝⁶ : Field E
E' : Type u_4
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E'
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsGalois F E
⊢ IsGalois { x // x ∈ ⊥ } E
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulSemiringAction M E
inst✝ : SMulCommClass M F E
src✝ : Subfield E := subfield M E
a : F
g : M
⊢ g • ↑(algebraMap F E) a = ↑(algebraMap F E) a
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, smul_comm, smul_one]
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
x✝ : { x // x ∈ fixingSubgroup K }
⊢ (fun ϕ =>
        { val := AlgEquiv.restrictScalars F ϕ,
          property :=
            (_ : ∀ (r : { x // x ∈ K }), ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
      ((fun ϕ =>
          let src := toRingEquiv ↑ϕ;
          { toEquiv := src.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : E), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : E), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
            commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
        x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case a.h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
x✝ : { x // x ∈ fixingSubgroup K }
a✝ : E
⊢ ↑↑((fun ϕ =>
              { val := AlgEquiv.restrictScalars F ϕ,
                property :=
                  (_ :
                    ∀ (r : { x // x ∈ K }), ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
            ((fun ϕ =>
                let src := toRingEquiv ↑ϕ;
                { toEquiv := src.toEquiv,
                  map_mul' :=
                    (_ :
                      ∀ (x y : E),
                        Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                  map_add' :=
                    (_ :
                      ∀ (x y : E),
                        Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                  commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
              x✝))
      a✝ =
    ↑↑x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
x✝ : E ≃ₐ[{ x // x ∈ K }] E
⊢ (fun ϕ =>
        let src := toRingEquiv ↑ϕ;
        { toEquiv := src.toEquiv,
          map_mul' :=
            (_ : ∀ (x y : E), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
          map_add' :=
            (_ : ∀ (x y : E), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
          commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
      ((fun ϕ =>
          { val := AlgEquiv.restrictScalars F ϕ,
            property :=
              (_ : ∀ (r : { x // x ∈ K }), ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
        x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
x✝ : E ≃ₐ[{ x // x ∈ K }] E
a✝ : E
⊢ ↑((fun ϕ =>
            let src := toRingEquiv ↑ϕ;
            { toEquiv := src.toEquiv,
              map_mul' :=
                (_ :
                  ∀ (x y : E), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
              map_add' :=
                (_ :
                  ∀ (x y : E), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
              commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
          ((fun ϕ =>
              { val := AlgEquiv.restrictScalars F ϕ,
                property :=
                  (_ :
                    ∀ (r : { x // x ∈ K }), ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
            x✝))
      a✝ =
    ↑x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
x✝¹ x✝ : { x // x ∈ fixingSubgroup K }
⊢ Equiv.toFun
      {
        toFun := fun ϕ =>
          let src := toRingEquiv ↑ϕ;
          { toEquiv := src.toEquiv,
            map_mul' :=
              (_ :
                ∀ (x y : E), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
            map_add' :=
              (_ :
                ∀ (x y : E), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
            commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) },
        invFun := fun ϕ =>
          { val := AlgEquiv.restrictScalars F ϕ,
            property :=
              (_ : ∀ (r : { x // x ∈ K }), ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) },
        left_inv :=
          (_ :
            ∀ (x : { x // x ∈ fixingSubgroup K }),
              (fun ϕ =>
                    { val := AlgEquiv.restrictScalars F ϕ,
                      property :=
                        (_ :
                          ∀ (r : { x // x ∈ K }),
                            ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                  ((fun ϕ =>
                      let src := toRingEquiv ↑ϕ;
                      { toEquiv := src.toEquiv,
                        map_mul' :=
                          (_ :
                            ∀ (x y : E),
                              Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                        map_add' :=
                          (_ :
                            ∀ (x y : E),
                              Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                        commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : E ≃ₐ[{ x // x ∈ K }] E),
              (fun ϕ =>
                    let src := toRingEquiv ↑ϕ;
                    { toEquiv := src.toEquiv,
                      map_mul' :=
                        (_ :
                          ∀ (x y : E),
                            Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                      map_add' :=
                        (_ :
                          ∀ (x y : E),
                            Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                      commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                  ((fun ϕ =>
                      { val := AlgEquiv.restrictScalars F ϕ,
                        property :=
                          (_ :
                            ∀ (r : { x // x ∈ K }),
                              ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                    x) =
                x) }
      (x✝¹ * x✝) =
    Equiv.toFun
        {
          toFun := fun ϕ =>
            let src := toRingEquiv ↑ϕ;
            { toEquiv := src.toEquiv,
              map_mul' :=
                (_ :
                  ∀ (x y : E), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
              map_add' :=
                (_ :
                  ∀ (x y : E), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
              commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) },
          invFun := fun ϕ =>
            { val := AlgEquiv.restrictScalars F ϕ,
              property :=
                (_ :
                  ∀ (r : { x // x ∈ K }), ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) },
          left_inv :=
            (_ :
              ∀ (x : { x // x ∈ fixingSubgroup K }),
                (fun ϕ =>
                      { val := AlgEquiv.restrictScalars F ϕ,
                        property :=
                          (_ :
                            ∀ (r : { x // x ∈ K }),
                              ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                    ((fun ϕ =>
                        let src := toRingEquiv ↑ϕ;
                        { toEquiv := src.toEquiv,
                          map_mul' :=
                            (_ :
                              ∀ (x y : E),
                                Equiv.toFun src.toEquiv (x * y) =
                                  Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                          map_add' :=
                            (_ :
                              ∀ (x y : E),
                                Equiv.toFun src.toEquiv (x + y) =
                                  Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                          commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : E ≃ₐ[{ x // x ∈ K }] E),
                (fun ϕ =>
                      let src := toRingEquiv ↑ϕ;
                      { toEquiv := src.toEquiv,
                        map_mul' :=
                          (_ :
                            ∀ (x y : E),
                              Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                        map_add' :=
                          (_ :
                            ∀ (x y : E),
                              Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                        commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                    ((fun ϕ =>
                        { val := AlgEquiv.restrictScalars F ϕ,
                          property :=
                            (_ :
                              ∀ (r : { x // x ∈ K }),
                                ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                      x) =
                  x) }
        x✝¹ *
      Equiv.toFun
        {
          toFun := fun ϕ =>
            let src := toRingEquiv ↑ϕ;
            { toEquiv := src.toEquiv,
              map_mul' :=
                (_ :
                  ∀ (x y : E), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
              map_add' :=
                (_ :
                  ∀ (x y : E), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
              commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) },
          invFun := fun ϕ =>
            { val := AlgEquiv.restrictScalars F ϕ,
              property :=
                (_ :
                  ∀ (r : { x // x ∈ K }), ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) },
          left_inv :=
            (_ :
              ∀ (x : { x // x ∈ fixingSubgroup K }),
                (fun ϕ =>
                      { val := AlgEquiv.restrictScalars F ϕ,
                        property :=
                          (_ :
                            ∀ (r : { x // x ∈ K }),
                              ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                    ((fun ϕ =>
                        let src := toRingEquiv ↑ϕ;
                        { toEquiv := src.toEquiv,
                          map_mul' :=
                            (_ :
                              ∀ (x y : E),
                                Equiv.toFun src.toEquiv (x * y) =
                                  Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                          map_add' :=
                            (_ :
                              ∀ (x y : E),
                                Equiv.toFun src.toEquiv (x + y) =
                                  Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                          commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : E ≃ₐ[{ x // x ∈ K }] E),
                (fun ϕ =>
                      let src := toRingEquiv ↑ϕ;
                      { toEquiv := src.toEquiv,
                        map_mul' :=
                          (_ :
                            ∀ (x y : E),
                              Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                        map_add' :=
                          (_ :
                            ∀ (x y : E),
                              Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                        commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                    ((fun ϕ =>
                        { val := AlgEquiv.restrictScalars F ϕ,
                          property :=
                            (_ :
                              ∀ (r : { x // x ∈ K }),
                                ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                      x) =
                  x) }
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
x✝¹ x✝ : { x // x ∈ fixingSubgroup K }
a✝ : E
⊢ ↑(Equiv.toFun
          {
            toFun := fun ϕ =>
              let src := toRingEquiv ↑ϕ;
              { toEquiv := src.toEquiv,
                map_mul' :=
                  (_ :
                    ∀ (x y : E),
                      Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                map_add' :=
                  (_ :
                    ∀ (x y : E),
                      Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) },
            invFun := fun ϕ =>
              { val := AlgEquiv.restrictScalars F ϕ,
                property :=
                  (_ :
                    ∀ (r : { x // x ∈ K }), ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) },
            left_inv :=
              (_ :
                ∀ (x : { x // x ∈ fixingSubgroup K }),
                  (fun ϕ =>
                        { val := AlgEquiv.restrictScalars F ϕ,
                          property :=
                            (_ :
                              ∀ (r : { x // x ∈ K }),
                                ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                      ((fun ϕ =>
                          let src := toRingEquiv ↑ϕ;
                          { toEquiv := src.toEquiv,
                            map_mul' :=
                              (_ :
                                ∀ (x y : E),
                                  Equiv.toFun src.toEquiv (x * y) =
                                    Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                            map_add' :=
                              (_ :
                                ∀ (x y : E),
                                  Equiv.toFun src.toEquiv (x + y) =
                                    Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                            commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : E ≃ₐ[{ x // x ∈ K }] E),
                  (fun ϕ =>
                        let src := toRingEquiv ↑ϕ;
                        { toEquiv := src.toEquiv,
                          map_mul' :=
                            (_ :
                              ∀ (x y : E),
                                Equiv.toFun src.toEquiv (x * y) =
                                  Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                          map_add' :=
                            (_ :
                              ∀ (x y : E),
                                Equiv.toFun src.toEquiv (x + y) =
                                  Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                          commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                      ((fun ϕ =>
                          { val := AlgEquiv.restrictScalars F ϕ,
                            property :=
                              (_ :
                                ∀ (r : { x // x ∈ K }),
                                  ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                        x) =
                    x) }
          (x✝¹ * x✝))
      a✝ =
    ↑(Equiv.toFun
            {
              toFun := fun ϕ =>
                let src := toRingEquiv ↑ϕ;
                { toEquiv := src.toEquiv,
                  map_mul' :=
                    (_ :
                      ∀ (x y : E),
                        Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                  map_add' :=
                    (_ :
                      ∀ (x y : E),
                        Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                  commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) },
              invFun := fun ϕ =>
                { val := AlgEquiv.restrictScalars F ϕ,
                  property :=
                    (_ :
                      ∀ (r : { x // x ∈ K }),
                        ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) },
              left_inv :=
                (_ :
                  ∀ (x : { x // x ∈ fixingSubgroup K }),
                    (fun ϕ =>
                          { val := AlgEquiv.restrictScalars F ϕ,
                            property :=
                              (_ :
                                ∀ (r : { x // x ∈ K }),
                                  ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                        ((fun ϕ =>
                            let src := toRingEquiv ↑ϕ;
                            { toEquiv := src.toEquiv,
                              map_mul' :=
                                (_ :
                                  ∀ (x y : E),
                                    Equiv.toFun src.toEquiv (x * y) =
                                      Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                              map_add' :=
                                (_ :
                                  ∀ (x y : E),
                                    Equiv.toFun src.toEquiv (x + y) =
                                      Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                              commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                          x) =
                      x),
              right_inv :=
                (_ :
                  ∀ (x : E ≃ₐ[{ x // x ∈ K }] E),
                    (fun ϕ =>
                          let src := toRingEquiv ↑ϕ;
                          { toEquiv := src.toEquiv,
                            map_mul' :=
                              (_ :
                                ∀ (x y : E),
                                  Equiv.toFun src.toEquiv (x * y) =
                                    Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                            map_add' :=
                              (_ :
                                ∀ (x y : E),
                                  Equiv.toFun src.toEquiv (x + y) =
                                    Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                            commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                        ((fun ϕ =>
                            { val := AlgEquiv.restrictScalars F ϕ,
                              property :=
                                (_ :
                                  ∀ (r : { x // x ∈ K }),
                                    ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                          x) =
                      x) }
            x✝¹ *
          Equiv.toFun
            {
              toFun := fun ϕ =>
                let src := toRingEquiv ↑ϕ;
                { toEquiv := src.toEquiv,
                  map_mul' :=
                    (_ :
                      ∀ (x y : E),
                        Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                  map_add' :=
                    (_ :
                      ∀ (x y : E),
                        Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                  commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) },
              invFun := fun ϕ =>
                { val := AlgEquiv.restrictScalars F ϕ,
                  property :=
                    (_ :
                      ∀ (r : { x // x ∈ K }),
                        ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) },
              left_inv :=
                (_ :
                  ∀ (x : { x // x ∈ fixingSubgroup K }),
                    (fun ϕ =>
                          { val := AlgEquiv.restrictScalars F ϕ,
                            property :=
                              (_ :
                                ∀ (r : { x // x ∈ K }),
                                  ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                        ((fun ϕ =>
                            let src := toRingEquiv ↑ϕ;
                            { toEquiv := src.toEquiv,
                              map_mul' :=
                                (_ :
                                  ∀ (x y : E),
                                    Equiv.toFun src.toEquiv (x * y) =
                                      Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                              map_add' :=
                                (_ :
                                  ∀ (x y : E),
                                    Equiv.toFun src.toEquiv (x + y) =
                                      Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                              commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                          x) =
                      x),
              right_inv :=
                (_ :
                  ∀ (x : E ≃ₐ[{ x // x ∈ K }] E),
                    (fun ϕ =>
                          let src := toRingEquiv ↑ϕ;
                          { toEquiv := src.toEquiv,
                            map_mul' :=
                              (_ :
                                ∀ (x y : E),
                                  Equiv.toFun src.toEquiv (x * y) =
                                    Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
                            map_add' :=
                              (_ :
                                ∀ (x y : E),
                                  Equiv.toFun src.toEquiv (x + y) =
                                    Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
                            commutes' := (_ : ↑ϕ ∈ ↑(fixingSubgroup K)) })
                        ((fun ϕ =>
                            { val := AlgEquiv.restrictScalars F ϕ,
                              property :=
                                (_ :
                                  ∀ (r : { x // x ∈ K }),
                                    ↑ϕ (↑(algebraMap { x // x ∈ K } E) r) = ↑(algebraMap { x // x ∈ K } E) r) })
                          x) =
                      x) }
            x✝)
      a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
⊢ fixingSubgroup (fixedField H) = H
[PROOFSTEP]
have H_le : H ≤ fixingSubgroup (fixedField H) := (le_iff_le _ _).mp le_rfl
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
H_le : H ≤ fixingSubgroup (fixedField H)
⊢ fixingSubgroup (fixedField H) = H
[PROOFSTEP]
classical
suffices Fintype.card H = Fintype.card (fixingSubgroup (fixedField H)) by
  exact
    SetLike.coe_injective
      (Set.eq_of_inclusion_surjective
          ((Fintype.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
              ⟨Set.inclusion_injective H_le, this⟩).2).symm
apply Fintype.card_congr
refine' (FixedPoints.toAlgHomEquiv H E).trans _
refine' (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans _
exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
H_le : H ≤ fixingSubgroup (fixedField H)
⊢ fixingSubgroup (fixedField H) = H
[PROOFSTEP]
suffices Fintype.card H = Fintype.card (fixingSubgroup (fixedField H)) by
  exact
    SetLike.coe_injective
      (Set.eq_of_inclusion_surjective
          ((Fintype.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
              ⟨Set.inclusion_injective H_le, this⟩).2).symm
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
H_le : H ≤ fixingSubgroup (fixedField H)
this : Fintype.card { x // x ∈ H } = Fintype.card { x // x ∈ fixingSubgroup (fixedField H) }
⊢ fixingSubgroup (fixedField H) = H
[PROOFSTEP]
exact
  SetLike.coe_injective
    (Set.eq_of_inclusion_surjective
        ((Fintype.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
            ⟨Set.inclusion_injective H_le, this⟩).2).symm
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
H_le : H ≤ fixingSubgroup (fixedField H)
⊢ Fintype.card { x // x ∈ H } = Fintype.card { x // x ∈ fixingSubgroup (fixedField H) }
[PROOFSTEP]
apply Fintype.card_congr
[GOAL]
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
H_le : H ≤ fixingSubgroup (fixedField H)
⊢ { x // x ∈ H } ≃ { x // x ∈ fixingSubgroup (fixedField H) }
[PROOFSTEP]
refine' (FixedPoints.toAlgHomEquiv H E).trans _
[GOAL]
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
H_le : H ≤ fixingSubgroup (fixedField H)
⊢ (E →ₐ[{ x // x ∈ FixedPoints.subfield { x // x ∈ H } E }] E) ≃ { x // x ∈ fixingSubgroup (fixedField H) }
[PROOFSTEP]
refine' (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans _
[GOAL]
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
H_le : H ≤ fixingSubgroup (fixedField H)
⊢ (E ≃ₐ[{ x // x ∈ fixedField H }] E) ≃ { x // x ∈ fixingSubgroup (fixedField H) }
[PROOFSTEP]
exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
x : { x // x ∈ K }
y : { x // x ∈ fixedField (fixingSubgroup K) }
ϕ : { x // x ∈ fixingSubgroup K }
⊢ ϕ • (↑x * ↑y) = ↑x * ↑y
[PROOFSTEP]
rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
⊢ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K
[PROOFSTEP]
have K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) :=
  (IntermediateField.le_iff_le _ _).mpr le_rfl
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K)
⊢ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K
[PROOFSTEP]
suffices finrank K E = finrank (IntermediateField.fixedField (IntermediateField.fixingSubgroup K)) E by
  exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K)
this :
  finrank { x // x ∈ K } E = finrank { x // x ∈ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) } E
⊢ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K
[PROOFSTEP]
exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K)
⊢ finrank { x // x ∈ K } E = finrank { x // x ∈ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) } E
[PROOFSTEP]
classical
rw [IntermediateField.finrank_fixedField_eq_card, Fintype.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
exact (card_aut_eq_finrank K E).symm
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K)
⊢ finrank { x // x ∈ K } E = finrank { x // x ∈ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) } E
[PROOFSTEP]
rw [IntermediateField.finrank_fixedField_eq_card, Fintype.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K)
⊢ finrank { x // x ∈ K } E = Fintype.card (E ≃ₐ[{ x // x ∈ K }] E)
[PROOFSTEP]
exact (card_aut_eq_finrank K E).symm
[GOAL]
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝² : DecidablePred fun x => x ∈ IntermediateField.fixingSubgroup K
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
⊢ Fintype.card { x // x ∈ IntermediateField.fixingSubgroup K } = finrank { x // x ∈ K } E
[PROOFSTEP]
conv_rhs => rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]
[GOAL]
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝² : DecidablePred fun x => x ∈ IntermediateField.fixingSubgroup K
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| finrank { x // x ∈ K } E
[PROOFSTEP]
rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]
[GOAL]
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝² : DecidablePred fun x => x ∈ IntermediateField.fixingSubgroup K
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| finrank { x // x ∈ K } E
[PROOFSTEP]
rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]
[GOAL]
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K : IntermediateField F E
inst✝² : DecidablePred fun x => x ∈ IntermediateField.fixingSubgroup K
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| finrank { x // x ∈ K } E
[PROOFSTEP]
rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K✝ : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ ↑{ toFun := IntermediateField.fixingSubgroup, invFun := IntermediateField.fixedField,
            left_inv :=
              (_ :
                ∀ (K : IntermediateField F E), IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K),
            right_inv :=
              (_ :
                ∀ (H : (Subgroup (E ≃ₐ[F] E))ᵒᵈ),
                  IntermediateField.fixingSubgroup (IntermediateField.fixedField H) = H) }
        K ≤
      ↑{ toFun := IntermediateField.fixingSubgroup, invFun := IntermediateField.fixedField,
            left_inv :=
              (_ :
                ∀ (K : IntermediateField F E), IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K),
            right_inv :=
              (_ :
                ∀ (H : (Subgroup (E ≃ₐ[F] E))ᵒᵈ),
                  IntermediateField.fixingSubgroup (IntermediateField.fixedField H) = H) }
        L ↔
    K ≤ L
[PROOFSTEP]
rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
K✝ : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ ↑{ toFun := IntermediateField.fixingSubgroup, invFun := IntermediateField.fixedField,
            left_inv :=
              (_ :
                ∀ (K : IntermediateField F E), IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K),
            right_inv :=
              (_ :
                ∀ (H : (Subgroup (E ≃ₐ[F] E))ᵒᵈ),
                  IntermediateField.fixingSubgroup (IntermediateField.fixedField H) = H) }
        K ≤
      ↑{ toFun := IntermediateField.fixingSubgroup, invFun := IntermediateField.fixedField,
            left_inv :=
              (_ :
                ∀ (K : IntermediateField F E), IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K),
            right_inv :=
              (_ :
                ∀ (H : (Subgroup (E ≃ₐ[F] E))ᵒᵈ),
                  IntermediateField.fixingSubgroup (IntermediateField.fixedField H) = H) }
        L ↔
    IntermediateField.fixingSubgroup L ≤ IntermediateField.fixingSubgroup K
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
⊢ ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
[PROOFSTEP]
cases' Field.exists_primitive_element F E with α h1
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
[PROOFSTEP]
use minpoly F α, separable F α, IsGalois.splits F α
[GOAL]
case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ Algebra.adjoin F (Polynomial.rootSet (minpoly F α) E) = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← h1]
[GOAL]
case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ F⟮α⟯.toSubalgebra ≤ Algebra.adjoin F (Polynomial.rootSet (minpoly F α) E)
[PROOFSTEP]
rw [IntermediateField.adjoin_simple_toSubalgebra_of_integral (integral F α)]
[GOAL]
case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ Algebra.adjoin F {α} ≤ Algebra.adjoin F (Polynomial.rootSet (minpoly F α) E)
[PROOFSTEP]
apply Algebra.adjoin_mono
[GOAL]
case adjoin_rootSet'.H
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ {α} ⊆ Polynomial.rootSet (minpoly F α) E
[PROOFSTEP]
rw [Set.singleton_subset_iff, Polynomial.mem_rootSet]
[GOAL]
case adjoin_rootSet'.H
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ minpoly F α ≠ 0 ∧ ↑(Polynomial.aeval α) (minpoly F α) = 0
[PROOFSTEP]
exact ⟨minpoly.ne_zero (integral F α), minpoly.aeval _ _⟩
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : IntermediateField.fixedField ⊤ = ⊥
⊢ IsGalois F E
[PROOFSTEP]
rw [← isGalois_iff_isGalois_bot, ← h]
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : IntermediateField.fixedField ⊤ = ⊥
⊢ IsGalois { x // x ∈ IntermediateField.fixedField ⊤ } E
[PROOFSTEP]
classical exact IsGalois.of_fixed_field E (⊤ : Subgroup (E ≃ₐ[F] E))
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : IntermediateField.fixedField ⊤ = ⊥
⊢ IsGalois { x // x ∈ IntermediateField.fixedField ⊤ } E
[PROOFSTEP]
exact IsGalois.of_fixed_field E (⊤ : Subgroup (E ≃ₐ[F] E))
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ IsGalois F E
[PROOFSTEP]
apply of_fixedField_eq_bot
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ IntermediateField.fixedField ⊤ = ⊥
[PROOFSTEP]
have p : 0 < finrank (IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E))) E := finrank_pos
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank { x // x ∈ IntermediateField.fixedField ⊤ } E
⊢ IntermediateField.fixedField ⊤ = ⊥
[PROOFSTEP]
classical
rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm, finrank_mul_finrank, ← h, one_mul,
  IntermediateField.finrank_fixedField_eq_card]
apply Fintype.card_congr
exact
  { toFun := fun g => ⟨g, Subgroup.mem_top g⟩
    invFun := (↑)
    left_inv := fun g => rfl
    right_inv := fun _ => by ext; rfl }
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank { x // x ∈ IntermediateField.fixedField ⊤ } E
⊢ IntermediateField.fixedField ⊤ = ⊥
[PROOFSTEP]
rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm, finrank_mul_finrank, ← h, one_mul,
  IntermediateField.finrank_fixedField_eq_card]
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank { x // x ∈ IntermediateField.fixedField ⊤ } E
⊢ Fintype.card (E ≃ₐ[F] E) = Fintype.card { x // x ∈ ⊤ }
[PROOFSTEP]
apply Fintype.card_congr
[GOAL]
case h.f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank { x // x ∈ IntermediateField.fixedField ⊤ } E
⊢ (E ≃ₐ[F] E) ≃ { x // x ∈ ⊤ }
[PROOFSTEP]
exact
  { toFun := fun g => ⟨g, Subgroup.mem_top g⟩
    invFun := (↑)
    left_inv := fun g => rfl
    right_inv := fun _ => by ext; rfl }
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank { x // x ∈ IntermediateField.fixedField ⊤ } E
x✝ : { x // x ∈ ⊤ }
⊢ (fun g => { val := g, property := (_ : g ∈ ⊤) }) ↑x✝ = x✝
[PROOFSTEP]
ext
[GOAL]
case a.h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank { x // x ∈ IntermediateField.fixedField ⊤ } E
x✝ : { x // x ∈ ⊤ }
a✝ : E
⊢ ↑↑((fun g => { val := g, property := (_ : g ∈ ⊤) }) ↑x✝) a✝ = ↑↑x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
⊢ Fintype.card ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) =
    Fintype.card (K →ₐ[F] E) * finrank K { x_1 // x_1 ∈ K⟮x⟯ }
[PROOFSTEP]
have h : IsIntegral K x := isIntegral_of_isScalarTower (isIntegral_of_noetherian (IsNoetherian.iff_fg.2 hFE) x)
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
⊢ Fintype.card ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) =
    Fintype.card (K →ₐ[F] E) * finrank K { x_1 // x_1 ∈ K⟮x⟯ }
[PROOFSTEP]
have h1 : p ≠ 0 := fun hp => by
  rw [hp, Polynomial.map_zero, Polynomial.roots_zero] at hx
  exact Multiset.not_mem_zero x hx
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp✝ : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
hp : p = 0
⊢ False
[PROOFSTEP]
rw [hp, Polynomial.map_zero, Polynomial.roots_zero] at hx
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp✝ : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ 0
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
hp : p = 0
⊢ False
[PROOFSTEP]
exact Multiset.not_mem_zero x hx
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
⊢ Fintype.card ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) =
    Fintype.card (K →ₐ[F] E) * finrank K { x_1 // x_1 ∈ K⟮x⟯ }
[PROOFSTEP]
have h2 : minpoly K x ∣ p.map (algebraMap F K) := by
  apply minpoly.dvd
  rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ← IsScalarTower.algebraMap_eq]
  exact (Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
⊢ minpoly K x ∣ Polynomial.map (algebraMap F K) p
[PROOFSTEP]
apply minpoly.dvd
[GOAL]
case hp
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
⊢ ↑(Polynomial.aeval x) (Polynomial.map (algebraMap F K) p) = 0
[PROOFSTEP]
rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ← IsScalarTower.algebraMap_eq]
[GOAL]
case hp
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
⊢ Polynomial.eval x (Polynomial.map (algebraMap F E) p) = 0
[PROOFSTEP]
exact (Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ Fintype.card ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) =
    Fintype.card (K →ₐ[F] E) * finrank K { x_1 // x_1 ∈ K⟮x⟯ }
[PROOFSTEP]
let key_equiv : (K⟮x⟯.restrictScalars F →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, @AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f) :=
  by
  change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, _
  exact algHomEquivSigma
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
    (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
[PROOFSTEP]
change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, _
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[F] E) ≃ (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
[PROOFSTEP]
exact algHomEquivSigma
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
⊢ Fintype.card ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) =
    Fintype.card (K →ₐ[F] E) * finrank K { x_1 // x_1 ∈ K⟮x⟯ }
[PROOFSTEP]
haveI : ∀ f : K →ₐ[F] E, Fintype (@AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f)) := fun f =>
  by
  have := Fintype.ofEquiv _ key_equiv
  apply Fintype.ofInjective (Sigma.mk f) fun _ _ H => eq_of_heq (Sigma.ext_iff.mp H).2
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
f : K →ₐ[F] E
⊢ Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
[PROOFSTEP]
have := Fintype.ofEquiv _ key_equiv
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
f : K →ₐ[F] E
this : Fintype ((f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E))
⊢ Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
[PROOFSTEP]
apply Fintype.ofInjective (Sigma.mk f) fun _ _ H => eq_of_heq (Sigma.ext_iff.mp H).2
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
⊢ Fintype.card ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) =
    Fintype.card (K →ₐ[F] E) * finrank K { x_1 // x_1 ∈ K⟮x⟯ }
[PROOFSTEP]
rw [Fintype.card_congr key_equiv, Fintype.card_sigma, IntermediateField.adjoin.finrank h]
[GOAL]
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
⊢ (Finset.sum Finset.univ fun a => Fintype.card ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)) =
    Fintype.card (K →ₐ[F] E) * Polynomial.natDegree (minpoly K x)
[PROOFSTEP]
apply Finset.sum_const_nat
[GOAL]
case h₁
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
⊢ ∀ (x_1 : K →ₐ[F] E),
    x_1 ∈ Finset.univ → Fintype.card ({ x_2 // x_2 ∈ K⟮x⟯ } →ₐ[K] E) = Polynomial.natDegree (minpoly K x)
[PROOFSTEP]
intro f _
[GOAL]
case h₁
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Fintype.card ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) = Polynomial.natDegree (minpoly K x)
[PROOFSTEP]
rw [← @IntermediateField.card_algHom_adjoin_integral K _ E _ _ x E _ (RingHom.toAlgebra f) h]
[GOAL]
case h₁
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Fintype.card ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) = Fintype.card ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
[PROOFSTEP]
congr!
[GOAL]
case h₁.h_sep
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.Separable (minpoly K x)
[PROOFSTEP]
exact Polynomial.Separable.of_dvd ((Polynomial.separable_map (algebraMap F K)).mpr hp) h2
[GOAL]
case h₁.h_splits
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.Splits (algebraMap K E) (minpoly K x)
[PROOFSTEP]
refine' Polynomial.splits_of_splits_of_dvd _ (Polynomial.map_ne_zero h1) _ h2
[GOAL]
case h₁.h_splits
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.Splits (algebraMap K E) (Polynomial.map (algebraMap F K) p)
[PROOFSTEP]
rw [Polynomial.splits_map_iff, ← @IsScalarTower.algebraMap_eq _ _ _ _ _ _ _ (_) _ _]
[GOAL]
case h₁.h_splits
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ Polynomial.roots (Polynomial.map (algebraMap F E) p)
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F K⟮x⟯ } →ₐ[F] E) ≃
  (f : K →ₐ[F] E) × ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E) :=
  let_fun this := algHomEquivSigma;
  this
this : (f : K →ₐ[F] E) → Fintype ({ x_1 // x_1 ∈ K⟮x⟯ } →ₐ[K] E)
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.Splits (algebraMap F E) p
[PROOFSTEP]
exact sp.splits
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
⊢ IsGalois F E
[PROOFSTEP]
haveI hFE : FiniteDimensional F E := Polynomial.IsSplittingField.finiteDimensional E p
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
⊢ IsGalois F E
[PROOFSTEP]
letI := Classical.decEq E
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
⊢ IsGalois F E
[PROOFSTEP]
let s := (p.map (algebraMap F E)).roots.toFinset
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
⊢ IsGalois F E
[PROOFSTEP]
have adjoin_root : IntermediateField.adjoin F (s : Set E) = ⊤ :=
  by
  apply IntermediateField.toSubalgebra_injective
  rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]
  apply IntermediateField.algebra_adjoin_le_adjoin
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
⊢ IntermediateField.adjoin F ↑s = ⊤
[PROOFSTEP]
apply IntermediateField.toSubalgebra_injective
[GOAL]
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
⊢ (IntermediateField.adjoin F ↑s).toSubalgebra = ⊤.toSubalgebra
[PROOFSTEP]
rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]
[GOAL]
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
⊢ Algebra.adjoin F (Polynomial.rootSet p E) ≤ (IntermediateField.adjoin F ↑s).toSubalgebra
[PROOFSTEP]
apply IntermediateField.algebra_adjoin_le_adjoin
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
⊢ IsGalois F E
[PROOFSTEP]
let P : IntermediateField F E → Prop := fun K => Fintype.card (K →ₐ[F] E) = finrank F K
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
⊢ IsGalois F E
[PROOFSTEP]
suffices P (IntermediateField.adjoin F ↑s) by
  rw [adjoin_root] at this
  apply of_card_aut_eq_finrank
  rw [← Eq.trans this (LinearEquiv.finrank_eq IntermediateField.topEquiv.toLinearEquiv)]
  exact
    Fintype.card_congr
      ((algEquivEquivAlgHom F E).toEquiv.trans (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this✝ : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
this : P (IntermediateField.adjoin F ↑s)
⊢ IsGalois F E
[PROOFSTEP]
rw [adjoin_root] at this
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this✝ : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
this : P ⊤
⊢ IsGalois F E
[PROOFSTEP]
apply of_card_aut_eq_finrank
[GOAL]
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this✝ : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
this : P ⊤
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
rw [← Eq.trans this (LinearEquiv.finrank_eq IntermediateField.topEquiv.toLinearEquiv)]
[GOAL]
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this✝ : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
this : P ⊤
⊢ Fintype.card (E ≃ₐ[F] E) = Fintype.card ({ x // x ∈ ⊤ } →ₐ[F] E)
[PROOFSTEP]
exact
  Fintype.card_congr
    ((algEquivEquivAlgHom F E).toEquiv.trans (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
⊢ P (IntermediateField.adjoin F ↑s)
[PROOFSTEP]
apply IntermediateField.induction_on_adjoin_finset s P
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
⊢ P ⊥
[PROOFSTEP]
have key := IntermediateField.card_algHom_adjoin_integral F (K := E) (show IsIntegral F (0 : E) from isIntegral_zero)
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
key :
  Polynomial.Separable (minpoly F 0) →
    Polynomial.Splits (algebraMap F E) (minpoly F 0) →
      Fintype.card ({ x // x ∈ F⟮0⟯ } →ₐ[F] E) = Polynomial.natDegree (minpoly F 0)
⊢ P ⊥
[PROOFSTEP]
rw [minpoly.zero, Polynomial.natDegree_X] at key
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
key :
  Polynomial.Separable Polynomial.X →
    Polynomial.Splits (algebraMap F E) Polynomial.X → Fintype.card ({ x // x ∈ F⟮0⟯ } →ₐ[F] E) = 1
⊢ P ⊥
[PROOFSTEP]
specialize key Polynomial.separable_X (Polynomial.splits_X (algebraMap F E))
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
key : Fintype.card ({ x // x ∈ F⟮0⟯ } →ₐ[F] E) = 1
⊢ P ⊥
[PROOFSTEP]
rw [← @Subalgebra.finrank_bot F E _ _ _, ← IntermediateField.bot_toSubalgebra] at key
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
key : Fintype.card ({ x // x ∈ F⟮0⟯ } →ₐ[F] E) = finrank F { x // x ∈ ⊥.toSubalgebra }
⊢ P ⊥
[PROOFSTEP]
refine' Eq.trans _ key
[GOAL]
case base
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
key : Fintype.card ({ x // x ∈ F⟮0⟯ } →ₐ[F] E) = finrank F { x // x ∈ ⊥.toSubalgebra }
⊢ Fintype.card ({ x // x ∈ ⊥ } →ₐ[F] E) = Fintype.card ({ x // x ∈ F⟮0⟯ } →ₐ[F] E)
[PROOFSTEP]
apply @Fintype.card_congr _ _ _ (_) _
[GOAL]
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
key : Fintype.card ({ x // x ∈ F⟮0⟯ } →ₐ[F] E) = finrank F { x // x ∈ ⊥.toSubalgebra }
⊢ ({ x // x ∈ ⊥ } →ₐ[F] E) ≃ ({ x // x ∈ F⟮0⟯ } →ₐ[F] E)
[PROOFSTEP]
rw [IntermediateField.adjoin_zero]
[GOAL]
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
⊢ ∀ (K : IntermediateField F E) (x : E), x ∈ s → P K → P (IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯)
[PROOFSTEP]
intro K x hx hK
[GOAL]
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
K : IntermediateField F E
x : E
hx : x ∈ s
hK : P K
⊢ P (IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯)
[PROOFSTEP]
simp only at *
  -- Porting note: need to specify two implicit arguments of `finrank_mul_finrank`
[GOAL]
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑(Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))) = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
K : IntermediateField F E
x : E
hx : x ∈ Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
hK : Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
⊢ Fintype.card ({ x_1 // x_1 ∈ IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯ } →ₐ[F] E) =
    finrank F { x_1 // x_1 ∈ IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯ }
[PROOFSTEP]
rw [of_separable_splitting_field_aux hp K (Multiset.mem_toFinset.mp hx), hK,
  @finrank_mul_finrank _ _ _ _ _ _ _ K⟮x⟯.module _ K⟮x⟯.isScalarTower _]
[GOAL]
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑(Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))) = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
K : IntermediateField F E
x : E
hx : x ∈ Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
hK : Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
⊢ finrank F { x_1 // x_1 ∈ { x // x ∈ K }⟮x⟯ } =
    finrank F { x_1 // x_1 ∈ IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯ }
[PROOFSTEP]
symm
[GOAL]
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑(Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))) = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
K : IntermediateField F E
x : E
hx : x ∈ Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
hK : Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
⊢ finrank F { x_1 // x_1 ∈ IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯ } =
    finrank F { x_1 // x_1 ∈ { x // x ∈ K }⟮x⟯ }
[PROOFSTEP]
refine' LinearEquiv.finrank_eq _
[GOAL]
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : Polynomial.Separable p
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Finset E := Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
adjoin_root : IntermediateField.adjoin F ↑(Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))) = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
K : IntermediateField F E
x : E
hx : x ∈ Multiset.toFinset (Polynomial.roots (Polynomial.map (algebraMap F E) p))
hK : Fintype.card ({ x // x ∈ K } →ₐ[F] E) = finrank F { x // x ∈ K }
⊢ { x_1 // x_1 ∈ IntermediateField.restrictScalars F { x // x ∈ K }⟮x⟯ } ≃ₗ[F] { x_1 // x_1 ∈ { x // x ∈ K }⟮x⟯ }
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
⊢ List.TFAE
    [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
⊢ IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
[PROOFSTEP]
exact fun h => OrderIso.map_bot (@intermediateFieldEquivSubgroup F _ E _ _ _ h).symm
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
⊢ List.TFAE
    [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p]
[PROOFSTEP]
tfae_have 1 → 3
[GOAL]
case tfae_1_to_3
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
⊢ IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
intro
[GOAL]
case tfae_1_to_3
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
✝ : IsGalois F E
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E
[PROOFSTEP]
exact card_aut_eq_finrank F E
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ List.TFAE
    [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p]
[PROOFSTEP]
tfae_have 1 → 4
[GOAL]
case tfae_1_to_4
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
[PROOFSTEP]
intro
[GOAL]
case tfae_1_to_4
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
✝ : IsGalois F E
⊢ ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
[PROOFSTEP]
exact is_separable_splitting_field F E
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
⊢ List.TFAE
    [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p]
[PROOFSTEP]
tfae_have 2 → 1
[GOAL]
case tfae_2_to_1
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
⊢ IntermediateField.fixedField ⊤ = ⊥ → IsGalois F E
[PROOFSTEP]
exact of_fixedField_eq_bot F E
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : IntermediateField.fixedField ⊤ = ⊥ → IsGalois F E
⊢ List.TFAE
    [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p]
[PROOFSTEP]
tfae_have 3 → 1
[GOAL]
case tfae_3_to_1
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : IntermediateField.fixedField ⊤ = ⊥ → IsGalois F E
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
[PROOFSTEP]
exact of_card_aut_eq_finrank F E
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : IntermediateField.fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
⊢ List.TFAE
    [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p]
[PROOFSTEP]
tfae_have 4 → 1
[GOAL]
case tfae_4_to_1
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : IntermediateField.fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
⊢ (∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p) → IsGalois F E
[PROOFSTEP]
rintro ⟨h, hp1, _⟩
[GOAL]
case tfae_4_to_1.intro.intro
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : IntermediateField.fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
h : F[X]
hp1 : Polynomial.Separable h
right✝ : Polynomial.IsSplittingField F E h
⊢ IsGalois F E
[PROOFSTEP]
exact of_separable_splitting_field hp1
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
p : F[X]
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → IntermediateField.fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : IntermediateField.fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
tfae_4_to_1 : (∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p) → IsGalois F E
⊢ List.TFAE
    [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, Polynomial.Separable p ∧ Polynomial.IsSplittingField F E p]
[PROOFSTEP]
tfae_finish