awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G E
⊢ IsGalois (↥(FixedPoints.subfield G E)) E

Tactic:
⟨⟩

Premises used: IsGalois.mk
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α))
rw : Nat.card.{u_2} Gal(↥F⟮α⟯/F) = Polynomial.natDegree (minpoly F α)
⊢ Nat.card.{u_2} Gal(↥F⟮α⟯/F) = finrank.{u_1, u_2} F ↥F⟮α⟯

Tactic:
rw [IntermediateField.adjoin.finrank hα]

Premises used: IntermediateField.adjoin.finrank
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α))
rw : Nat.card.{u_2} Gal(↥F⟮α⟯/F) = Nat.card.{u_2} (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯)
⊢ Nat.card.{u_2} Gal(↥F⟮α⟯/F) = Polynomial.natDegree (minpoly F α)

Tactic:
rw [← IntermediateField.card_algHom_adjoin_integral F hα h_sep h_splits]

Premises used: IntermediateField.card_algHom_adjoin_integral
-- Module: Mathlib.FieldTheory.Galois.Basic
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) = Nat.card.{u_2} (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯)

Tactic:
Nat.card_congr (algEquivEquivAlgHom F F⟮α⟯)

Premises used: Membership.mem, Subtype, algEquivEquivAlgHom, Nat.card_congr, IntermediateField.adjoin, Singleton.singleton, EquivLike.toEquiv
-- Module: Mathlib.FieldTheory.Galois.Basic
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) = Nat.card.{u_2} (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯)

Tactic:
exact Nat.card_congr (algEquivEquivAlgHom F F⟮α⟯)

Premises used: Nat.card_congr
-- Module: Mathlib.FieldTheory.Galois.Basic
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
obtain : ∀ (α : E) (hα : Eq (α := IntermediateField F E) F⟮α⟯ ⊤), Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E

Tactic:
obtain ⟨α, hα⟩ := Field.exists_primitive_element F E

Premises used: Field.exists_primitive_element
-- Module: Mathlib.FieldTheory.Galois.Basic
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
rw : Membership.mem (γ := IntermediateField F E) ⊤ e
⊢ Membership.mem (γ := IntermediateField F E) F⟮α⟯ e

Tactic:
rw [hα]
-- Module: Mathlib.FieldTheory.Galois.Basic
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) ⊤ e

Tactic:
IntermediateField.mem_top

Premises used: IntermediateField.mem_top
-- Module: Mathlib.FieldTheory.Galois.Basic
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) ⊤ e

Tactic:
exact IntermediateField.mem_top

Premises used: IntermediateField.mem_top
-- Module: Mathlib.FieldTheory.Galois.Basic
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' := ⋯ }
⊢ IsIntegral F α

Tactic:
have H : IsIntegral F α := IsGalois.integral F α
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α
⊢ IsSeparable F α

Tactic:
have h_sep : IsSeparable F α := IsGalois.separable F α
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α
⊢ Polynomial.Splits (Polynomial.map (algebraMap F E) (minpoly F α))

Tactic:
have h_splits : ((minpoly F α).map (algebraMap F E)).Splits := IsGalois.splits F α
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α))
⊢ Polynomial.Splits.{u_2} (R := ↥F⟮α⟯) (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α))

Tactic:
simpa [Polynomial.map_map] using h_splits.map iso.symm.toRingHom

Premises used: AlgEquiv.symm, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Polynomial.Splits.map, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α))
⊢ 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
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α))
rw : Nat.card.{u_2} Gal(E/F) = finrank.{u_1, u_2} F ↥F⟮α⟯
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E

Tactic:
rw [← LinearEquiv.finrank_eq iso.toLinearEquiv]

Premises used: LinearEquiv.finrank_eq, AlgEquiv.toLinearEquiv
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α))
rw : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} Gal(↥F⟮α⟯/F)
⊢ Nat.card.{u_2} Gal(E/F) = finrank.{u_1, u_2} F ↥F⟮α⟯

Tactic:
rw [← IntermediateField.AdjoinSimple.card_aut_eq_finrank F E H h_sep h_splits]

Premises used: IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α))
f : Gal(E/F) ≃ Gal(↥F⟮α⟯/F)
⊢ Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} Gal(↥F⟮α⟯/F)

Tactic:
apply Nat.card_congr

Premises used: Nat.card_congr
-- Module: Mathlib.FieldTheory.Galois.Basic
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 α))
⊢ Gal(E/F) ≃ Gal(↥F⟮α⟯/F)

Tactic:
exact Equiv.mk (fun ϕ => iso.trans (ϕ.trans iso.symm)) fun ϕ => iso.symm.trans (ϕ.trans iso)

Premises used: AlgEquiv.symm, Equiv.mk, AlgEquiv.trans
-- Module: Mathlib.FieldTheory.Galois.Basic
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)
by_contra : ∀ (H : ¬FiniteDimensional F E), False
⊢ FiniteDimensional F E

Tactic:
by_contra H
-- Module: Mathlib.FieldTheory.Galois.Basic
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
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
⊢ False

Tactic:
obtain ⟨K, h₁, h₂⟩ := exists_lt_finrank_of_infinite_dimensional H (Nat.card Gal(E/F))

Premises used: Nat.card, AlgEquiv, IntermediateField.exists_lt_finrank_of_infinite_dimensional
-- Module: Mathlib.FieldTheory.Galois.Basic
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
⊢ IsGalois.{u_1, u_2} F ↥K'

Tactic:
have : IsGalois F K' := ⟨⟩
-- Module: Mathlib.FieldTheory.Galois.Basic
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'
⊢ 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))
-- Module: Mathlib.FieldTheory.Galois.Basic
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)
⊢ finrank.{u_1, u_2} F ↥K' ≤ Nat.card.{u_2} Gal(E/F)

Tactic:
rw [IsGalois.card_aut_eq_finrank] at this

Premises used: IsGalois.card_aut_eq_finrank
-- Module: Mathlib.FieldTheory.Galois.Basic
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 : finrank.{u_1, u_2} F ↥K' ≤ Nat.card.{u_2} Gal(E/F)
⊢ False

Tactic:
(this.trans_lt h₂).not_ge (finrank_le_of_le_right K.le_normalClosure)

Premises used: LT.lt.not_ge, LE.le.trans_lt, IntermediateField.le_normalClosure, IntermediateField.finrank_le_of_le_right
-- Module: Mathlib.FieldTheory.Galois.Basic
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 : finrank.{u_1, u_2} F ↥K' ≤ Nat.card.{u_2} Gal(E/F)
⊢ False

Tactic:
exact (this.trans_lt h₂).not_ge (finrank_le_of_le_right K.le_normalClosure)

Premises used: LT.lt.not_ge, LE.le.trans_lt, IntermediateField.le_normalClosure, IntermediateField.finrank_le_of_le_right
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field E
inst_3 : Algebra F K
inst_4 : Algebra F E
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
inst_7 : IsGalois F E
⊢ IsGalois K E

Tactic:
{ to_isSeparable := Algebra.isSeparable_tower_top_of_isSeparable F K E
    to_normal := Normal.tower_top_of_normal F K E }

Premises used: IsGalois.mk
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K_1 : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field K_1
inst_2 : Field E
E' : Type u_4
inst_3 : Field E'
inst_4 : Algebra F E'
inst_5 : Algebra F K_1
inst_6 : Algebra F E
inst_7 : Algebra K_1 E
inst_8 : IsScalarTower F K_1 E
K : IntermediateField F E
inst_9 : IsGalois F E
⊢ IsGalois (↥K) E

Tactic:
IsGalois.tower_top_of_isGalois F K E

Premises used: Membership.mem, IsGalois.tower_top_of_isGalois, Subtype
-- Module: Mathlib.FieldTheory.Galois.Basic
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
mpr : IsGalois F E → IsGalois (↥⊥) E
⊢ IsGalois (↥⊥) E ↔ IsGalois F E

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : IsGalois (↥⊥) E
⊢ IsGalois F E

Tactic:
IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E

Premises used: Membership.mem, IsGalois.tower_top_of_isGalois, Subtype, Bot.bot
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : IsGalois (↥⊥) E
⊢ IsGalois F E

Tactic:
exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E

Premises used: Membership.mem, IsGalois.tower_top_of_isGalois, Subtype, Bot.bot
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : IsGalois F E
⊢ IsGalois (↥⊥) E

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
E' : Type u_4
inst_2 : Field E'
inst_3 : Algebra F E'
inst_4 : Algebra F E
inst_5 : IsGalois F E
f : E ≃ₐ[F] E'
⊢ IsGalois F E'

Tactic:
{ to_isSeparable := Algebra.IsSeparable.of_algHom F E f.symm
    to_normal := Normal.of_algEquiv f }

Premises used: IsGalois.mk
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
E' : Type u_4
inst_2 : Field E'
inst_3 : Algebra F E'
inst_4 : Algebra F E
f : E ≃ₐ[F] E'
⊢ IsGalois F E ↔ IsGalois F E'

Tactic:
⟨fun _ => IsGalois.of_algEquiv f, fun _ => IsGalois.of_algEquiv f.symm⟩

Premises used: IsGalois.of_algEquiv, AlgEquiv.symm, Iff.intro
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ IsGalois.{u_1, u_3} F ↥⊤ ↔ IsGalois F E

Tactic:
(IntermediateField.topEquiv : (⊤ : IntermediateField F E) ≃ₐ[F] E).transfer_galois

Premises used: AlgEquiv.transfer_galois, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field E
E' : Type u_4
inst_3 : Field E'
inst_4 : Algebra F E'
inst_5 : Algebra F K
inst_6 : Algebra F E
inst_7 : Algebra K E
inst_8 : IsScalarTower F K E
⊢ IsGalois.{u_1, u_3} F ↥⊥

Tactic:
(IntermediateField.botEquiv F E).transfer_galois.mpr (IsGalois.self F)

Premises used: Iff.mpr, IsGalois.self, AlgEquiv.transfer_galois, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
M : Type u_5
N : Type u_6
inst_3 : Field N
inst_4 : Field M
inst_5 : Algebra M N
inst_6 : Algebra.IsAlgebraic F E
h : IsGalois F E
f : F ≃+* M
g : E ≃+* N
hcomp :
  Eq (α := F →+* N) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap M N) (↑f : F →+* M))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : E →+* N) (algebraMap F E))
⊢ IsGalois M N

Tactic:
isGalois_iff.mpr ⟨Algebra.IsSeparable.of_equiv_equiv f g hcomp, Normal.of_equiv_equiv hcomp⟩

Premises used: Iff.mpr, Algebra.IsSeparable.of_equiv_equiv, Normal.of_equiv_equiv, isGalois_iff, And.intro
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
M : Type u_3
inst_3 : Monoid M
inst_4 : MulSemiringAction M E
inst_5 : SMulCommClass M F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) (intermediateField M) x ↔ ∀ (m : M), m • x = x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedPoints
-- Module: Mathlib.FieldTheory.Galois.Basic
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
change : x ∈ MulAction.fixedPoints (↥H) E ↔ ∀ f ∈ H, (f : (a : E) → E) x = x
⊢ x ∈ fixedField H ↔ ∀ f ∈ H, (f : (a : E) → E) x = x

Tactic:
change x ∈ MulAction.fixedPoints H E ↔ _

Premises used: Membership.mem, Subtype, MulAction.fixedPoints
-- Module: Mathlib.FieldTheory.Galois.Basic
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 ∈ MulAction.fixedPoints (↥H) E ↔ ∀ f ∈ H, (f : (a : E) → E) x = x

Tactic:
simp only [MulAction.mem_fixedPoints, Subtype.forall, Subgroup.mk_smul, AlgEquiv.smul_def]

Premises used: AlgEquiv.smul_def, Subtype.forall, MulAction.mem_fixedPoints, Subgroup.mk_smul
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h :
  ∀ (x : E),
    Membership.mem (γ := IntermediateField F E) (fixedField ⊥) x ↔ Membership.mem (γ := IntermediateField F E) ⊤ x
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊥) ⊤

Tactic:
ext
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) (fixedField ⊥) x ↔ Membership.mem (γ := IntermediateField F E) ⊤ x

Tactic:
simp
-- Module: Mathlib.FieldTheory.Galois.Basic
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
have : ∀ (this : Fintype ↥H), finrank (↥(fixedField H)) E = Nat.card.{u_2} ↥H
⊢ finrank (↥(fixedField H)) E = Nat.card.{u_2} ↥H

Tactic:
have := Fintype.ofFinite H
-- Module: Mathlib.FieldTheory.Galois.Basic
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
rw : finrank (↥(fixedField H)) E = Fintype.card.{u_2} ↥H
⊢ finrank (↥(fixedField H)) E = Nat.card.{u_2} ↥H

Tactic:
rw [Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Galois.Basic
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 = Fintype.card.{u_2} ↥H

Tactic:
FixedPoints.finrank_eq_card H E

Premises used: FixedPoints.finrank_eq_card, FixedPoints.intermediateField, Set.Mem, Membership.mem, IntermediateField.fixedField, Subtype, Subfield.copy, FixedPoints.subfield
-- Module: Mathlib.FieldTheory.Galois.Basic
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 = Fintype.card.{u_2} ↥H

Tactic:
exact FixedPoints.finrank_eq_card H E

Premises used: FixedPoints.finrank_eq_card, Membership.mem, Subtype
-- Module: Mathlib.FieldTheory.Galois.Basic
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
⊢ K ≤ fixedField H ↔ H ≤ K.fixingSubgroup

Tactic:
⟨fun h g hg x => h (Subtype.mem x) ⟨g, hg⟩, fun h x hx g => h (Subtype.mem g) ⟨x, hx⟩⟩

Premises used: Subtype.mk, Iff.intro, Subtype.mem
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K1 K2 : IntermediateField F E
h12 : K1 ≤ K2
⊢ K2.fixingSubgroup ≤ K1.fixingSubgroup

Tactic:
fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h12 hx⟩

Premises used: Set.Mem, setOf, Subtype.mk, HSMul.hSMul, _private.0.IntermediateField.fixingSubgroup_le.match_1, Subtype.val, Eq
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H1 H2 : Subgroup Gal(E/F)
h12 : H1 ≤ H2
⊢ fixedField H2 ≤ fixedField H1

Tactic:
fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h12 hx⟩

Premises used: Set.Mem, setOf, _private.0.IntermediateField.fixedField_le.match_1, Subtype.mk, HSMul.hSMul, MulAction.fixedPoints, Eq
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Antitone.{u_2, u_2} (α := IntermediateField F E) fixingSubgroup

Tactic:
fun _ _ ↦ fixingSubgroup_le

Premises used: IntermediateField.fixingSubgroup_le, Antitone
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Antitone.{u_2, u_2} (α := Subgroup Gal(E/F)) fixedField

Tactic:
fun _ _ ↦ fixedField_le

Premises used: Antitone, IntermediateField.fixedField_le