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
K : IntermediateField F E
σ : Gal(E/F)
⊢ σ ∈ K.fixingSubgroup ↔ ∀ x ∈ K, (σ : (a : E) → E) x = x

Tactic:
_root_.mem_fixingSubgroup_iff _

Premises used: Set.Mem, mem_fixingSubgroup_iff
-- 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 : Gal(E/F)),
    Membership.mem (γ := Subgroup Gal(E/F)) (fixingSubgroup ⊤) x ↔ Membership.mem (γ := Subgroup Gal(E/F)) ⊥ x
⊢ Eq.{u_2 + 1} (α := Subgroup Gal(E/F)) (fixingSubgroup ⊤) ⊥

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 : Gal(E/F)
⊢ Membership.mem (γ := Subgroup Gal(E/F)) (fixingSubgroup ⊤) x ↔ Membership.mem (γ := Subgroup Gal(E/F)) ⊥ x

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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 : Gal(E/F)),
    Membership.mem (γ := Subgroup Gal(E/F)) (fixingSubgroup ⊥) x ↔ Membership.mem (γ := Subgroup Gal(E/F)) ⊤ x
⊢ Eq.{u_2 + 1} (α := Subgroup Gal(E/F)) (fixingSubgroup ⊥) ⊤

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 : Gal(E/F)
⊢ Membership.mem (γ := Subgroup Gal(E/F)) (fixingSubgroup ⊥) x ↔ Membership.mem (γ := Subgroup Gal(E/F)) ⊤ x

Tactic:
simp [mem_bot]

Premises used: IntermediateField.mem_bot
-- 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
K L : IntermediateField F E
h : ∀ (φ : Gal(E/F)), φ ∈ (K ⊔ L).fixingSubgroup ↔ φ ∈ K.fixingSubgroup ⊓ L.fixingSubgroup
⊢ (K ⊔ L).fixingSubgroup = K.fixingSubgroup ⊓ L.fixingSubgroup

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
K L : IntermediateField F E
φ : Gal(E/F)
⊢ φ ∈ K.fixingSubgroup ⊓ L.fixingSubgroup → φ ∈ (K ⊔ L).fixingSubgroup

Tactic:
simp [← Subgroup.zpowers_le, ← IntermediateField.le_iff_le]

Premises used: Subgroup.zpowers_le, IntermediateField.le_iff_le
-- 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
K L : IntermediateField F E
φ : Gal(E/F)
⊢ φ ∈ (K ⊔ L).fixingSubgroup ↔ φ ∈ K.fixingSubgroup ⊓ L.fixingSubgroup

Tactic:
exact ⟨fun h ↦ ⟨fixingSubgroup_antitone le_sup_left h, fixingSubgroup_antitone le_sup_right h⟩,
    by simp [← Subgroup.zpowers_le, ← IntermediateField.le_iff_le]⟩
-- 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
x x_1 : ↥K.fixingSubgroup
h :
  ∀ (a : E),
    Eq (α := E)
      ((let __src := (↑(x * x_1) : Gal(E/F)).toRingEquiv;
            { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ } :
            (a : E) → E)
          a :
        E)
      ((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) }) :
            (a : E) → E)
          a :
        E)
⊢ (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) })

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
H : Subgroup Gal(E/F)
K : IntermediateField F E
x x_1 : ↥K.fixingSubgroup
a : E
⊢ Eq (α := E)
    ((let __src := (↑(x * x_1) : Gal(E/F)).toRingEquiv;
          { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ } :
          (a : E) → E)
        a :
      E)
    ((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) }) :
          (a : E) → E)
        a :
      E)

Tactic:
rfl
-- 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
⊢ H ≤ (fixedField H).fixingSubgroup

Tactic:
have H_le : H ≤ fixingSubgroup (fixedField H) := (le_iff_le _ _).mp le_rfl
-- 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
H_le : H ≤ (fixedField H).fixingSubgroup
this : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Tactic:
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

Premises used: Iff.mpr, Nat.bijective_iff_injective_and_card, SetLike.coe_injective, Set.eq_of_inclusion_surjective, And.right, Set.inclusion_injective, And.intro, Set.inclusion, Eq.symm
-- 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
H_le : H ≤ (fixedField H).fixingSubgroup
this : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Tactic:
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

Premises used: Iff.mpr, Nat.bijective_iff_injective_and_card, SetLike.coe_injective, Set.eq_of_inclusion_surjective, And.right, Set.inclusion_injective, And.intro, Set.inclusion, Eq.symm
-- 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
H_le : H ≤ (fixedField H).fixingSubgroup
suffices : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

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
-- 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
H_le : H ≤ (fixedField H).fixingSubgroup
f : ↥H ≃ ↥(fixedField H).fixingSubgroup
⊢ Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup

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
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
f : (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup
⊢ ↥H ≃ ↥(fixedField H).fixingSubgroup

Tactic:
refine (FixedPoints.toAlgHomEquiv H E).trans ?_

Premises used: Equiv.trans, Membership.mem, Subtype, FixedPoints.toAlgHomEquiv
-- 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
H_le : H ≤ (fixedField H).fixingSubgroup
f : Gal(E/↥(fixedField H)) ≃ ↥(fixedField H).fixingSubgroup
⊢ (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup

Tactic:
refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_

Premises used: Equiv.trans, Membership.mem, IntermediateField.fixedField, Subtype, MulEquiv.toEquiv, algEquivEquivAlgHom, Equiv.symm
-- 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
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ Gal(E/↥(fixedField H)) ≃ ↥(fixedField H).fixingSubgroup

Tactic:
exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm

Premises used: IntermediateField.fixedField, IntermediateField.fixingSubgroupEquiv, MulEquiv.toEquiv, Equiv.symm
-- 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
H_le : H ≤ (fixedField H).fixingSubgroup
suffices suffices₁ suffices₂ : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
f : ↥H ≃ ↥(fixedField H).fixingSubgroup
f₁ : (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup
f₂ : Gal(E/↥(fixedField H)) ≃ ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Tactic:
classical
  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
  apply Nat.card_congr
  refine (FixedPoints.toAlgHomEquiv H E).trans ?_
  refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
  exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm

Premises used: Equiv.trans, Membership.mem, IntermediateField.fixedField, IntermediateField.fixingSubgroupEquiv, Subtype, MulEquiv.toEquiv, algEquivEquivAlgHom, Nat.card_congr, Equiv.symm, FixedPoints.toAlgHomEquiv
-- 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
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
rw : ϕ • (↑x : E) * ϕ • (↑y : E) = (↑x : E) * (↑y : E)
rw₁ : (↑x : E) * ϕ • (↑y : E) = (↑x : E) * (↑y : E)
rw₂ rw₃ : (↑x : E) * (↑y : E) = (↑x : E) * (↑y : E)
⊢ ϕ • ((↑x : E) * (↑y : E)) = (↑x : E) * (↑y : E)

Tactic:
rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]

Premises used: Subtype.property, smul_mul'
-- 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
⊢ IsScalarTower (↥K) (↥(fixedField K.fixingSubgroup)) E

Tactic:
⟨fun _ _ _ => mul_assoc _ _ _⟩

Premises used: mul_assoc, IsScalarTower.mk, Subtype.val
-- 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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
⊢ K ≤ fixedField K.fixingSubgroup

Tactic:
have K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) :=
    (IntermediateField.le_iff_le _ _).mpr le_rfl
-- 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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
this : finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
⊢ fixedField K.fixingSubgroup = K

Tactic:
(IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm

Premises used: IntermediateField.eq_of_le_of_finrank_eq', Eq.symm
-- 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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
this : finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
⊢ fixedField K.fixingSubgroup = K

Tactic:
exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm

Premises used: IntermediateField.eq_of_le_of_finrank_eq', Eq.symm
-- 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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
finrank : Module.finrank (↥K) E = Module.finrank (↥(fixedField K.fixingSubgroup)) E
⊢ fixedField K.fixingSubgroup = K

Tactic:
suffices
    finrank K E = finrank (IntermediateField.fixedField (IntermediateField.fixingSubgroup K)) E by
    exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm
-- 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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
rw : finrank (↥K) E = Nat.card.{u_2} Gal(E/↥K)
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E

Tactic:
rw [IntermediateField.finrank_fixedField_eq_card,
    Nat.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]

Premises used: IntermediateField.fixingSubgroupEquiv, MulEquiv.toEquiv, Nat.card_congr, IntermediateField.finrank_fixedField_eq_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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = Nat.card.{u_2} Gal(E/↥K)

Tactic:
(card_aut_eq_finrank K E).symm

Premises used: IsGalois.card_aut_eq_finrank, Set.Mem, Membership.mem, Subtype, Eq.symm
-- 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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = Nat.card.{u_2} Gal(E/↥K)

Tactic:
exact (card_aut_eq_finrank K E).symm

Premises used: IsGalois.card_aut_eq_finrank, Membership.mem, Subtype, Eq.symm
-- 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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
rw : finrank (↥K) E = Nat.card.{u_2} ↥K.fixingSubgroup
rw₁ rw₂ rw₃ : finrank (↥K) E = Nat.card.{u_2} Gal(E/↥K)
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E

Tactic:
classical
  rw [IntermediateField.finrank_fixedField_eq_card,
    Nat.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
  exact (card_aut_eq_finrank K E).symm

Premises used: IsGalois.card_aut_eq_finrank, Membership.mem, IntermediateField.fixingSubgroupEquiv, Subtype, MulEquiv.toEquiv, Nat.card_congr, IntermediateField.finrank_fixedField_eq_card, Eq.symm
-- 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 : FiniteDimensional F E
rw : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField (IntermediateField.fixingSubgroup ⊥)) ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊥
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥

Tactic:
rw [← fixingSubgroup_bot, fixedField_fixingSubgroup]

Premises used: IsGalois.fixedField_fixingSubgroup, IntermediateField.fixingSubgroup_bot
-- 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 : FiniteDimensional F E
x : E
rw :
  (∀ (f : Gal(E/F)), Membership.mem (γ := Subgroup Gal(E/F)) ⊤ f → (f : (a : E) → E) x = x) ↔
    ∀ (f : Gal(E/F)), (f : (a : E) → E) x = x
⊢ Membership.mem (γ := IntermediateField F E) ⊥ x ↔ ∀ (f : Gal(E/F)), (f : (a : E) → E) x = x

Tactic:
rw [← fixedField_top, mem_fixedField_iff]

Premises used: IntermediateField.mem_fixedField_iff, IsGalois.fixedField_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 : IsGalois F E
inst_4 : FiniteDimensional F E
x : E
⊢ (∀ (f : Gal(E/F)), Membership.mem (γ := Subgroup Gal(E/F)) ⊤ f → (f : (a : E) → E) x = x) ↔
    ∀ (f : Gal(E/F)), (f : (a : E) → E) x = x

Tactic:
simp only [Subgroup.mem_top, forall_const]

Premises used: Subgroup.mem_top, forall_const
-- 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 : FiniteDimensional F E
x : E
⊢ Membership.mem (γ := Set E) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x ↔
    ∀ (f : Gal(E/F)), (f : (a : E) → E) x = x

Tactic:
mem_bot_iff_fixed x

Premises used: Set.Mem, setOf, Set.range, IsGalois.mem_bot_iff_fixed
-- 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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
rw : Nat.card.{u_2} ↥K.fixingSubgroup
| finrank (↥K) E

Tactic:
rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]

Premises used: IsGalois.fixedField_fixingSubgroup, IntermediateField.finrank_fixedField_eq_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
K : IntermediateField F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
conv_rhs : Nat.card.{u_2} ↥K.fixingSubgroup = finrank (↥K) E
conv_rhs₁ : Nat.card.{u_2} ↥K.fixingSubgroup = Nat.card.{u_2} ↥K.fixingSubgroup
⊢ Nat.card.{u_2} ↥K.fixingSubgroup = finrank (↥K) E

Tactic:
conv_rhs => rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]

Premises used: IsGalois.fixedField_fixingSubgroup, IntermediateField.finrank_fixedField_eq_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)
K_1 : IntermediateField F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
K L : IntermediateField F E
rw :
  LE.le (α := (Subgroup Gal(E/F))ᵒᵈ)
      (({
              toFun :=
                (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘
                  IntermediateField.fixingSubgroup,
              invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
          K :
        (Subgroup Gal(E/F))ᵒᵈ)
      (({
              toFun :=
                (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘
                  IntermediateField.fixingSubgroup,
              invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
          L :
        (Subgroup Gal(E/F))ᵒᵈ) ↔
    L.fixingSubgroup ≤ K.fixingSubgroup
⊢ LE.le (α := (Subgroup Gal(E/F))ᵒᵈ)
      (({
              toFun :=
                (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘
                  IntermediateField.fixingSubgroup,
              invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
          K :
        (Subgroup Gal(E/F))ᵒᵈ)
      (({
              toFun :=
                (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘
                  IntermediateField.fixingSubgroup,
              invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
          L :
        (Subgroup Gal(E/F))ᵒᵈ) ↔
    K ≤ L

Tactic:
rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]

Premises used: IsGalois.fixedField_fixingSubgroup, IntermediateField.le_iff_le
-- 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_1 : IntermediateField F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
K L : IntermediateField F E
⊢ LE.le (α := (Subgroup Gal(E/F))ᵒᵈ)
      (({
              toFun :=
                (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘
                  IntermediateField.fixingSubgroup,
              invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
          K :
        (Subgroup Gal(E/F))ᵒᵈ)
      (({
              toFun :=
                (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘
                  IntermediateField.fixingSubgroup,
              invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
          L :
        (Subgroup Gal(E/F))ᵒᵈ) ↔
    L.fixingSubgroup ≤ K.fixingSubgroup

Tactic:
rfl
-- 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
K : IntermediateField F E
⊢ (OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F))
      ((intermediateFieldEquivSubgroup : (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ) K) =
    K.fixingSubgroup

Tactic:
rfl

Premises used: fixingSubgroup, IntermediateField.fixingSubgroup, rfl
-- 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
H : (Subgroup Gal(E/F))ᵒᵈ
⊢ Eq (α := IntermediateField F E)
    ((OrderIso.symm intermediateFieldEquivSubgroup : (a : (Subgroup Gal(E/F))ᵒᵈ) → IntermediateField F E) H :
      IntermediateField F E)
    (fixedField ((OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)) H) : IntermediateField F E)

Tactic:
rfl

Premises used: FixedPoints.intermediateField, IntermediateField.fixedField, rfl
-- 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
H : Subgroup Gal(E/F)
⊢ (OrderIso.symm intermediateFieldEquivSubgroup : (a : (Subgroup Gal(E/F))ᵒᵈ) → IntermediateField F E)
      ((OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) H : (Subgroup Gal(E/F))ᵒᵈ) =
    fixedField H

Tactic:
rfl

Premises used: FixedPoints.intermediateField, Set.Mem, IntermediateField.fixedField, rfl
-- 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
K : IntermediateField F E
H : Subgroup Gal(E/F)
⊢ fixedField H = K ↔ K.fixingSubgroup = H

Tactic:
simp [← OrderIso.apply_eq_iff_eq intermediateFieldEquivSubgroup, fixingSubgroup_fixedField,
    eq_comm]

Premises used: IntermediateField.fixingSubgroup_fixedField, eq_comm, OrderIso.apply_eq_iff_eq, IsGalois.intermediateFieldEquivSubgroup