awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f_1 : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f_1.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f_1)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
⊢ ∀
    (hq :
      Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
        (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
              (a : Q) → Gal(F/↥(subfield Q F)))
            q :
          Gal(F/↥(subfield Q F)))
        (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))),
    ∃ (a : G),
      ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
            (a : G) → Gal(F/↥(subfield G F)))
          a =
        f
have refine : ∀ (g : G)
  (hg :
    Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
      (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
            (a : Q) → Gal(F/↥(subfield Q F)))
          (↑g : G ⧸ f_1.ker) :
        Gal(F/↥(subfield Q F)))
      (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) sorry : Gal(F/↥(subfield Q F)))),
  ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
        (a : G) → Gal(F/↥(subfield G F)))
      g =
    f
Tactic: refine QuotientGroup.induction_on q (fun g hg ↦ ⟨g, ?_⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f_1 : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f_1.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f_1)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
g : G
hg :
  Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
    (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
          (a : Q) → Gal(F/↥(subfield Q F)))
        (↑g : G ⧸ f_1.ker) :
      Gal(F/↥(subfield Q F)))
    (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))
⊢ ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
        (a : G) → Gal(F/↥(subfield G F)))
      g =
    f
have rwa : ∀
  (hg :
    ∀ (a : F),
      Eq (α := F)
        (((((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
                    (a : Q) → Gal(F/↥(subfield Q F)))
                  (↑g : G ⧸ f_1.ker) :
                Gal(F/↥(subfield Q F))) :
              (a : F) → F)
            a :
          F)
        ((AlgEquiv.ofRingEquiv (f := f.toRingEquiv) sorry : (a : F) → F) a : F))
  (a : F),
  Eq (α := F)
    (((((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
                (a : G) → Gal(F/↥(subfield G F)))
              g :
            Gal(F/↥(subfield G F))) :
          (a : F) → F)
        a :
      F)
    ((f : (a : F) → F) a : F)
Tactic: rwa [AlgEquiv.ext_iff] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Abelian (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(L/K)
⊢ x * y = y * x
have obtain : ∀ (x : Gal(M/K)),
  HMul.hMul (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K)) y =
    HMul.hMul (β := Gal(L/K)) y ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
Tactic: obtain ⟨x, rfl⟩ := AlgEquiv.restrictNormalHom_surjective M x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Abelian (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
this : IsGalois K L
y : Gal(L/K)
x : Gal(M/K)
⊢ HMul.hMul (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K)) y =
    HMul.hMul (β := Gal(L/K)) y ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
have obtain : ∀ (y : Gal(M/K)),
  HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K)) =
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
Tactic: obtain ⟨y, rfl⟩ := AlgEquiv.restrictNormalHom_surjective M y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Abelian (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
⊢ HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K)) =
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
have rw : (AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (x * y) =
  HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
    ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
Tactic: rw [← map_mul, ← map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Abelian (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
rw :
  (AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (x * y) =
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
⊢ HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K)) =
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
have rw₁ : Eq.{u_2 + 1} (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (x * y) : Gal(L/K))
  ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (y * x) : Gal(L/K))
Tactic: rw [← map_mul, ← map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Abelian (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
rw :
  (AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (x * y) =
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
rw₁ :
  Eq.{u_2 + 1} (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (x * y) : Gal(L/K))
    ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (y * x) : Gal(L/K))
⊢ HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K)) =
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
have rw₂ : Eq.{u_2 + 1} (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (y * x) : Gal(L/K))
  ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (y * x) : Gal(L/K))
Tactic: rw [← map_mul, ← map_mul, mul_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits.{u_2} (R := ↥F⟮α⟯) (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α))
⊢ Nat.card.{u_2} Gal(↥F⟮α⟯/F) = finrank.{u_1, u_2} F ↥F⟮α⟯
have rw : Nat.card.{u_2} Gal(↥F⟮α⟯/F) = Polynomial.natDegree (minpoly F α)
Tactic: rw [IntermediateField.adjoin.finrank hα]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits.{u_2} (R := ↥F⟮α⟯) (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α))
⊢ Nat.card.{u_2} Gal(↥F⟮α⟯/F) = Polynomial.natDegree (minpoly F α)
have rw : Nat.card.{u_2} Gal(↥F⟮α⟯/F) = Nat.card.{u_2} (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯)
Tactic: rw [← IntermediateField.card_algHom_adjoin_integral F hα h_sep h_splits]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E
have obtain : ∀ (α : E) (hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤), Nat.card.{u_2} Gal(E/F) = finrank F E
Tactic: obtain ⟨α, hα⟩ := Field.exists_primitive_element F E
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
α : E
hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
e : E
⊢ Membership.mem (γ := IntermediateField F E) F⟮α⟯ e
have rw : Membership.mem (γ := IntermediateField F E) ⊤ e
Tactic: rw [hα]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
α : E
hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun (e : ↥F⟮α⟯) ↦ (↑e : E),
    invFun := fun (e : E) ↦ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮α⟯ x) e ⋯,
    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E
have H : IsIntegral F α
Tactic: have H : IsIntegral F α := IsGalois.integral F α
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
α : E
hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun (e : ↥F⟮α⟯) ↦ (↑e : E),
    invFun := fun (e : E) ↦ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮α⟯ x) e ⋯,
    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
H : IsIntegral F α
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E
have h_sep : IsSeparable F α
Tactic: have h_sep : IsSeparable F α := IsGalois.separable F α
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
α : E
hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun (e : ↥F⟮α⟯) ↦ (↑e : E),
    invFun := fun (e : E) ↦ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮α⟯ x) e ⋯,
    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E
have h_splits : Polynomial.Splits (Polynomial.map (algebraMap F E) (minpoly F α))
Tactic: have h_splits : ((minpoly F α).map (algebraMap F E)).Splits := IsGalois.splits F α
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
α : E
hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun (e : ↥F⟮α⟯) ↦ (↑e : E),
    invFun := fun (e : E) ↦ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮α⟯ x) e ⋯,
    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (Polynomial.map (algebraMap F E) (minpoly F α))
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E
have h_splits₁ : Polynomial.Splits.{u_2} (R := ↥F⟮α⟯) (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α))
Tactic: replace h_splits : ((minpoly F α).map (algebraMap F F⟮α⟯)).Splits := by
    simpa [Polynomial.map_map] using h_splits.map iso.symm.toRingHom
Cleared hypotheses: h_splits
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
α : E
hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun (e : ↥F⟮α⟯) ↦ (↑e : E),
    invFun := fun (e : E) ↦ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮α⟯ x) e ⋯,
    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits.{u_2} (R := ↥F⟮α⟯) (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α))
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E
have rw : Nat.card.{u_2} Gal(E/F) = finrank.{u_1, u_2} F ↥F⟮α⟯
Tactic: rw [← LinearEquiv.finrank_eq iso.toLinearEquiv]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
α : E
hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun (e : ↥F⟮α⟯) ↦ (↑e : E),
    invFun := fun (e : E) ↦ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮α⟯ x) e ⋯,
    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits.{u_2} (R := ↥F⟮α⟯) (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α))
⊢ Nat.card.{u_2} Gal(E/F) = finrank.{u_1, u_2} F ↥F⟮α⟯
have rw : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} Gal(↥F⟮α⟯/F)
Tactic: rw [← IntermediateField.AdjoinSimple.card_aut_eq_finrank F E H h_sep h_splits]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
α : E
hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun (e : ↥F⟮α⟯) ↦ (↑e : E),
    invFun := fun (e : E) ↦ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮α⟯ x) e ⋯,
    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits.{u_2} (R := ↥F⟮α⟯) (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α))
⊢ Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} Gal(↥F⟮α⟯/F)
have f : Gal(E/F) ≃ Gal(↥F⟮α⟯/F)
Tactic: apply Nat.card_congr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
inst_4 : Finite.{u_2 + 1} Gal(E/F)
⊢ FiniteDimensional F E
have by_contra : ∀ (H : ¬FiniteDimensional F E), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
inst_4 : Finite.{u_2 + 1} Gal(E/F)
H : ¬FiniteDimensional F E
⊢ False
have obtain : ∀ (K : IntermediateField F E) (h₁ : FiniteDimensional.{u_1, u_2} F ↥K)
  (h₂ : Nat.card.{u_2} Gal(E/F) < finrank.{u_1, u_2} F ↥K), False
Tactic: obtain ⟨K, h₁, h₂⟩ := exists_lt_finrank_of_infinite_dimensional H (Nat.card Gal(E/F))
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
inst_4 : Finite.{u_2 + 1} Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional.{u_1, u_2} F ↥K
h₂ : Nat.card.{u_2} Gal(E/F) < finrank.{u_1, u_2} F ↥K
K' : IntermediateField F E := normalClosure F (↥K) E
⊢ False
have this : IsGalois.{u_1, u_2} F ↥K'
Tactic: have : IsGalois F K' := ⟨⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
inst_4 : Finite.{u_2 + 1} Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional.{u_1, u_2} F ↥K
h₂ : Nat.card.{u_2} Gal(E/F) < finrank.{u_1, u_2} F ↥K
K' : IntermediateField F E := normalClosure F (↥K) E
this : IsGalois.{u_1, u_2} F ↥K'
⊢ False
have this₁ : Nat.card.{u_2} Gal(↥K'/F) ≤ Nat.card.{u_2} Gal(E/F)
Tactic: have := Nat.card_le_card_of_surjective _
    (AlgEquiv.restrictNormalHom_surjective (F := F) (K₁ := K') (E := E))
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
inst_4 : Finite.{u_2 + 1} Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional.{u_1, u_2} F ↥K
h₂ : Nat.card.{u_2} Gal(E/F) < finrank.{u_1, u_2} F ↥K
K' : IntermediateField F E := normalClosure F (↥K) E
this_1 : IsGalois.{u_1, u_2} F ↥K'
this : Nat.card.{u_2} Gal(↥K'/F) ≤ Nat.card.{u_2} Gal(E/F)
⊢ False
have this₁ : finrank.{u_1, u_2} F ↥K' ≤ Nat.card.{u_2} Gal(E/F)
Tactic: rw [IsGalois.card_aut_eq_finrank] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ IsGalois (↥⊥) E ↔ IsGalois F E
have mp : IsGalois (↥⊥) E → IsGalois F E
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
mp : IsGalois (↥⊥) E → IsGalois F E
⊢ IsGalois (↥⊥) E ↔ IsGalois F E
have mpr : IsGalois F E → IsGalois (↥⊥) E
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
x : E
⊢ x ∈ fixedField H ↔ ∀ f ∈ H, (f : (a : E) → E) x = x
have change : x ∈ MulAction.fixedPoints (↥H) E ↔ ∀ f ∈ H, (f : (a : E) → E) x = x
Tactic: change x ∈ MulAction.fixedPoints H E ↔ _
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊥) ⊤
have h : ∀ (x : E),
  Membership.mem (γ := IntermediateField F E) (fixedField ⊥) x ↔ Membership.mem (γ := IntermediateField F E) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
⊢ finrank (↥(fixedField H)) E = Nat.card.{u_2} ↥H
have have : ∀ (this : Fintype ↥H), finrank (↥(fixedField H)) E = Nat.card.{u_2} ↥H
Tactic: have := Fintype.ofFinite H
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
this : Fintype ↥H
⊢ finrank (↥(fixedField H)) E = Nat.card.{u_2} ↥H
have rw : finrank (↥(fixedField H)) E = Fintype.card.{u_2} ↥H
Tactic: rw [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_2 + 1} (α := Subgroup Gal(E/F)) (fixingSubgroup ⊤) ⊥
have h : ∀ (x : Gal(E/F)),
  Membership.mem (γ := Subgroup Gal(E/F)) (fixingSubgroup ⊤) x ↔ Membership.mem (γ := Subgroup Gal(E/F)) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_2 + 1} (α := Subgroup Gal(E/F)) (fixingSubgroup ⊥) ⊤
have h : ∀ (x : Gal(E/F)),
  Membership.mem (γ := Subgroup Gal(E/F)) (fixingSubgroup ⊥) x ↔ Membership.mem (γ := Subgroup Gal(E/F)) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
⊢ (K ⊔ L).fixingSubgroup = K.fixingSubgroup ⊓ L.fixingSubgroup
have h : ∀ (φ : Gal(E/F)), φ ∈ (K ⊔ L).fixingSubgroup ↔ φ ∈ K.fixingSubgroup ⊓ L.fixingSubgroup
Tactic: ext φ
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
K : IntermediateField F E
x x_1 : ↥K.fixingSubgroup
⊢ (let __src := (↑(x * x_1) : Gal(E/F)).toRingEquiv;
    { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) =
    HMul.hMul (α := Gal(E/↥K))
      (let __src := (↑x : Gal(E/F)).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ : Gal(E/↥K) })
      (let __src := (↑x_1 : Gal(E/F)).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ : Gal(E/↥K) })
have h : ∀ (a : E),
  Eq (α := E)
    ((let __src := (↑(x * x_1) : Gal(E/F)).toRingEquiv;
          { toEquiv := __src.toEquiv, map_mul' := sorry, map_add' := sorry, commutes' := sorry } :
          (a : E) → E)
        a :
      E)
    ((HMul.hMul (α := Gal(E/↥K))
            (let __src := (↑x : Gal(E/F)).toRingEquiv;
            { toEquiv := __src.toEquiv, map_mul' := sorry, map_add' := sorry, commutes' := sorry : Gal(E/↥K) })
            (let __src := (↑x_1 : Gal(E/F)).toRingEquiv;
            { toEquiv := __src.toEquiv, map_mul' := sorry, map_add' := sorry, commutes' := sorry : Gal(E/↥K) }) :
          (a : E) → E)
        a :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
⊢ (fixedField H).fixingSubgroup = H
have H_le : H ≤ (fixedField H).fixingSubgroup
Tactic: have H_le : H ≤ fixingSubgroup (fixedField H) := (le_iff_le _ _).mp le_rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H
have suffices : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
Tactic: suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by
    exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
      ((Nat.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
        ⟨Set.inclusion_injective H_le, this⟩).2).symm