awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x : ↥K
z : F
hy : Membership.mem (α := E) L ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E)
hx₁ :
  Membership.mem (α := E) K
    ((algebraMap (↥L) E : (a : ↥L) → E)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L) :
      E)
hx₂ :
  Membership.mem (α := ↥K) (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
        ((algebraMap (↥L) E : (a : ↥L) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L))
        hx₁ :
      ↥K)
⊢ Membership.mem (α := ↥K) (γ := IntermediateField F ↥K) ⊥
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
        ((algebraMap (↥L) E : (a : ↥L) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L))
        hx₁ :
      ↥K)

Tactic:
exact mem_bot.mp ⟨z, rfl⟩

Premises used: Exists.intro, Iff.mp, IntermediateField.mem_bot, rfl
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
⊢ Fintype.card.{u_2} Gal(K/F) ≤ 2

Tactic:
have := finrank_eq_two F K ▸ AlgEquiv.card_le
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
this : Fintype.card.{u_2} Gal(K/F) ≤ 2
⊢ Nat.card.{u_2} Gal(K/F) ≤ 2

Tactic:
rw [← Nat.card_eq_fintype_card] at this

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
this : Nat.card.{u_2} Gal(K/F) ≤ 2
0 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 0) (this : LE.le (α := ℕ) 0 2), IsCyclic.{u_2} Gal(K/F)
1 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 1) (this : LE.le (α := ℕ) 1 2), IsCyclic.{u_2} Gal(K/F)
2 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 2) (this : LE.le (α := ℕ) 2 2), IsCyclic.{u_2} Gal(K/F)
⊢ IsCyclic.{u_2} Gal(K/F)

Tactic:
interval_cases h : Nat.card Gal(K/F)

Premises used: Nat.card, AlgEquiv
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
h : Nat.card.{u_2} Gal(K/F) = 0
this : LE.le (α := ℕ) 0 2
⊢ IsCyclic.{u_2} Gal(K/F)

Tactic:
simp_all
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
h : Nat.card.{u_2} Gal(K/F) = 1
this : LE.le (α := ℕ) 1 2
⊢ IsCyclic.{u_2} Gal(K/F)

Tactic:
@isCyclic_of_subsingleton _ _ (Finite.card_le_one_iff_subsingleton.mp h.le)

Premises used: isCyclic_of_subsingleton
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
h : Nat.card.{u_2} Gal(K/F) = 1
this : LE.le (α := ℕ) 1 2
⊢ IsCyclic.{u_2} Gal(K/F)

Tactic:
exact @isCyclic_of_subsingleton _ _ (Finite.card_le_one_iff_subsingleton.mp h.le)

Premises used: isCyclic_of_subsingleton
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
h : Nat.card.{u_2} Gal(K/F) = 2
this : LE.le (α := ℕ) 2 2
⊢ IsCyclic.{u_2} Gal(K/F)

Tactic:
isCyclic_of_prime_card h

Premises used: isCyclic_of_prime_card
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
h : Nat.card.{u_2} Gal(K/F) = 2
this : LE.le (α := ℕ) 2 2
⊢ IsCyclic.{u_2} Gal(K/F)

Tactic:
exact isCyclic_of_prime_card h

Premises used: isCyclic_of_prime_card
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
⊢ IsMulCommutative.{u_2} Gal(K/F)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : FiniteGaloisIntermediateField k K
⊢ FiniteDimensional.{u_1, u_2} k ↥L.toIntermediateField

Tactic:
L.finiteDimensional

Premises used: FiniteGaloisIntermediateField.finiteDimensional
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : FiniteGaloisIntermediateField k K
⊢ IsGalois.{u_1, u_2} k ↥L.toIntermediateField

Tactic:
L.isGalois

Premises used: FiniteGaloisIntermediateField.isGalois
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
toIntermediateField : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥toIntermediateField
isGalois : IsGalois.{u_1, u_2} k ↥toIntermediateField
toIntermediateField_1 : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥toIntermediateField_1
isGalois_1 : IsGalois.{u_1, u_2} k ↥toIntermediateField_1
eq :
  { toIntermediateField := toIntermediateField, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K }.toIntermediateField =
    { toIntermediateField := toIntermediateField_1, finiteDimensional := finiteDimensional_1,
        isGalois := isGalois_1 }.toIntermediateField
⊢ { toIntermediateField := toIntermediateField, finiteDimensional := finiteDimensional, isGalois := isGalois :
      FiniteGaloisIntermediateField k K } =
    { toIntermediateField := toIntermediateField_1, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }

Tactic:
simpa only [mk.injEq] using eq

Premises used: FiniteGaloisIntermediateField.mk.injEq
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ L₂ : IntermediateField k K
inst_3 : FiniteDimensional.{u_1, u_2} k ↥L₁
⊢ FiniteDimensional.{u_1, u_2} k ↥(L₁ ⊓ L₂)

Tactic:
.of_injective (IntermediateField.inclusion (E := L₁ ⊓ L₂) (F := L₁) inf_le_left).toLinearMap
    (IntermediateField.inclusion (E := L₁ ⊓ L₂) (F := L₁) inf_le_left).toRingHom.injective

Premises used: AlgHom.toLinearMap, FiniteDimensional.of_injective, RingHom.injective, AlgHom.toRingHom, inf_le_left, IntermediateField.inclusion
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ L₂ : IntermediateField k K
inst_3 : FiniteDimensional.{u_1, u_2} k ↥L₂
⊢ FiniteDimensional.{u_1, u_2} k ↥(L₁ ⊓ L₂)

Tactic:
.of_injective (IntermediateField.inclusion (E := L₁ ⊓ L₂) (F := L₂) inf_le_right).toLinearMap
    (IntermediateField.inclusion (E := L₁ ⊓ L₂) (F := L₂) inf_le_right).injective

Premises used: AlgHom.toLinearMap, inf_le_right, FiniteDimensional.of_injective, RingHom.injective, AlgHom.toRingHom, IntermediateField.inclusion
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ L₂ : IntermediateField k K
inst_3 : Algebra.IsSeparable.{u_1, u_2} k ↥L₁
⊢ Algebra.IsSeparable.{u_1, u_2} k ↥(L₁ ⊓ L₂)

Tactic:
.of_algHom _ _ (IntermediateField.inclusion inf_le_left)

Premises used: inf_le_left, IntermediateField.inclusion, Algebra.IsSeparable.of_algHom
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ L₂ : IntermediateField k K
inst_3 : Algebra.IsSeparable.{u_1, u_2} k ↥L₂
⊢ Algebra.IsSeparable.{u_1, u_2} k ↥(L₁ ⊓ L₂)

Tactic:
.of_algHom _ _ (IntermediateField.inclusion inf_le_right)

Premises used: inf_le_right, IntermediateField.inclusion, Algebra.IsSeparable.of_algHom
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ L₂ : FiniteGaloisIntermediateField k K
⊢ L₁ ≤ L₂ ↔ L₁.toIntermediateField ≤ L₂.toIntermediateField

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
s : Set K
inst_4 : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ Eq (α := IntermediateField k K) (toIntermediateField (adjoin k s))
    (normalClosure k (↥(IntermediateField.adjoin k s)) K)

Tactic:
rfl

Premises used: Set.Mem, iSup, setOf, IntermediateField.normalClosure, rfl
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
s : Set K
inst_4 : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ s ⊆ (↑(toIntermediateField (adjoin k s)) : Set K)

Tactic:
(IntermediateField.subset_adjoin k s).trans (IntermediateField.le_normalClosure _)

Premises used: HasSubset.Subset.trans, IntermediateField.subset_adjoin, IntermediateField.le_normalClosure
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
x : K
L : FiniteGaloisIntermediateField k K
⊢ adjoin k {x} ≤ L ↔ x ∈ L.toIntermediateField

Tactic:
simp only [le_iff, adjoin_val, IntermediateField.normalClosure_le_iff_of_normal,
    IntermediateField.adjoin_le_iff, Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, IntermediateField.adjoin_le_iff, SetLike.mem_coe, FiniteGaloisIntermediateField.adjoin_val, FiniteGaloisIntermediateField.le_iff, IntermediateField.normalClosure_le_iff_of_normal
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst_4 : Finite.{u_2 + 1} (↑s : Type u_2)
a :
  Eq (α := IntermediateField k K) (toIntermediateField (adjoin k ((⇑f : (a : K) → K) '' s)))
    (toIntermediateField (adjoin k s))
⊢ Eq (α := FiniteGaloisIntermediateField k K) (adjoin k ((⇑f : (a : K) → K) '' s)) (adjoin k s)

Tactic:
apply val_injective

Premises used: FiniteGaloisIntermediateField.val_injective
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst_4 : Finite.{u_2 + 1} (↑s : Type u_2)
a :
  Eq (α := IntermediateField k K) (normalClosure k (↥(map f (IntermediateField.adjoin k s))) K)
    (normalClosure k (↥(IntermediateField.adjoin k s)) K)
a₁ a₂ :
  Eq (α := IntermediateField k K) (normalClosure k (↥(IntermediateField.adjoin k s)) K)
    (normalClosure k (↥(IntermediateField.adjoin k s)) K)
⊢ Eq (α := IntermediateField k K) (normalClosure k (↥(IntermediateField.adjoin k ((⇑f : (a : K) → K) '' s))) K)
    (normalClosure k (↥(IntermediateField.adjoin k s)) K)

Tactic:
rw [← IntermediateField.adjoin_map, IntermediateField.normalClosure_map_eq]

Premises used: IntermediateField.adjoin_map, IntermediateField.normalClosure_map_eq
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
f : K →ₐ[k] K
x : K
⊢ Eq (α := FiniteGaloisIntermediateField k K) (adjoin k (singleton (α := K) ((f : (a : K) → K) x : K))) (adjoin k {x})

Tactic:
simpa only [Set.image_singleton] using adjoin_map f { x }

Premises used: Set.image_singleton, FiniteGaloisIntermediateField.adjoin_map, Singleton.singleton
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
f : Gal(K/k)
x : K
⊢ Eq (α := FiniteGaloisIntermediateField k K) (adjoin k (singleton (α := K) ((f : (a : K) → K) x : K))) (adjoin k {x})

Tactic:
adjoin_simple_map_algHom (f : K →ₐ[k] K) x

Premises used: AlgEquiv.toAlgHom, FiniteGaloisIntermediateField.adjoin_simple_map_algHom
-- Module: Mathlib.FieldTheory.Galois.GaloisClosure
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
α : Gal(K/k)
L : FiniteGaloisIntermediateField k K
⊢ α ∈ L.fixingSubgroup ↔
    Eq (α := Gal(↥L.toIntermediateField/k))
      ((AlgEquiv.restrictNormalHom ↥L.toIntermediateField : (a : Gal(K/k)) → Gal(↥L.toIntermediateField/k)) α :
        Gal(↥L.toIntermediateField/k))
      (1 : Gal(↥L.toIntermediateField/k))

Tactic:
simp [IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff, AlgEquiv.ext_iff, Subtype.ext_iff,
    AlgEquiv.restrictNormalHom_apply]

Premises used: FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, AlgEquiv.ext_iff, IntermediateField.fixingSubgroup, Subtype.ext_iff, AlgEquiv.restrictNormalHom_apply
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
apply : ∃ t ⊆ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ, IsOpen t ∧ σ ∈ t
⊢ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ ∈ nhds σ

Tactic:
apply mem_nhds_iff.mpr

Premises used: Iff.mpr, mem_nhds_iff
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
rcases :
  ∀ (y : K) (yL : y ∈ (↑L : Set K)) (ne : y ∉ fun (a : K) ↦ σ • a = a),
    ∃ t ⊆ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ, IsOpen t ∧ σ ∈ t
⊢ ∃ t ⊆ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ, IsOpen t ∧ σ ∈ t

Tactic:
rcases Set.not_subset.mp ((mem_fixingSubgroup_iff Gal(K/k)).not.mp h) with ⟨y, yL, ne⟩

Premises used: Iff.not, AlgEquiv, Set.not_subset, Iff.mp, mem_fixingSubgroup_iff
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
h₁ :
  σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ⊆
      (↑L.fixingSubgroup : Set Gal(K/k))ᶜ ∧
    IsOpen (σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))) ∧
      σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
⊢ ∃ t ⊆ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ, IsOpen t ∧ σ ∈ t

Tactic:
use σ • ((adjoin k {y}).1.fixingSubgroup : Set Gal(K/k))

Premises used: IntermediateField.fixingSubgroup, SetLike.coe, FiniteGaloisIntermediateField.adjoin, FiniteGaloisIntermediateField.toIntermediateField, Singleton.singleton
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
h₁ :
  σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ⊆
    (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
h₂ :
  IsOpen (σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))) ∧
    σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
⊢ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ⊆
      (↑L.fixingSubgroup : Set Gal(K/k))ᶜ ∧
    IsOpen (σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))) ∧
      σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
h₁ :
  ∀ (g : Gal(K/k)) (hg : g ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)))
    (eq : σ • g = f), f ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
⊢ f ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ

Tactic:
rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩

Premises used: Set.mem_smul_set, Iff.mp
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
g : Gal(K/k)
hg : g ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
eq : σ • g = f
h₁ : σ • g ∉ L.fixingSubgroup
⊢ f ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ

Tactic:
simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]

Premises used: SetLike.mem_coe, Set.mem_compl_iff
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
g : Gal(K/k)
hg : g ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
eq : σ • g = f
h₁ : ¬∀ y ∈ (↑L : Set K), (σ • g) • y = y
⊢ σ • g ∉ L.fixingSubgroup

Tactic:
apply (mem_fixingSubgroup_iff Gal(K/k)).not.mpr

Premises used: Iff.mpr, Iff.not, AlgEquiv, mem_fixingSubgroup_iff
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
g : Gal(K/k)
hg : g ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
eq : σ • g = f
h₁ : ∃ y ∈ (↑L : Set K), (σ • g) • y ≠ y
⊢ ¬∀ y ∈ (↑L : Set K), (σ • g) • y = y

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
g : Gal(K/k)
hg : g ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
eq : σ • g = f
h₁ : y ∈ (↑L : Set K) ∧ (σ • g) • y ≠ y
⊢ ∃ y ∈ (↑L : Set K), (σ • g) • y ≠ y

Tactic:
use y
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
g : Gal(K/k)
hg : g ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
eq : σ • g = f
h₁ : ¬(σ : (a : K) → K) ((g : (a : K) → K) y : K) = y
⊢ y ∈ (↑L : Set K) ∧ (σ • g) • y ≠ y

Tactic:
simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and]

Premises used: AlgEquiv.smul_def, ne_eq, AlgEquiv.mul_apply, smul_eq_mul, true_and
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
g : Gal(K/k)
hg : g ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
eq : σ • g = f
⊢ (g : (a : K) → K) y = y

Tactic:
have : g y = y := (mem_fixingSubgroup_iff Gal(K/k)).mp hg y <|
        adjoin_simple_le_iff.mp le_rfl
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
g : Gal(K/k)
hg : g ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
eq : σ • g = f
this : (g : (a : K) → K) y = y
⊢ ¬(σ : (a : K) → K) ((g : (a : K) → K) y : K) = y

Tactic:
simpa only [this, ne_eq, AlgEquiv.smul_def] using ne

Premises used: AlgEquiv.smul_def, ne_eq
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
h₁ : σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
⊢ IsOpen (σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))) ∧
    σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))

Tactic:
simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and]

Premises used: IsOpen.smul, FiniteGaloisIntermediateField.adjoin, FiniteGaloisIntermediateField.toIntermediateField, IntermediateField.fixingSubgroup_isOpen, Singleton.singleton, true_and
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
h₁ :
  1 ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ∧
    (fun (x : Gal(K/k)) ↦ σ • x) 1 = σ
⊢ σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))

Tactic:
use 1
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
⊢ 1 ∈ (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ∧
    (fun (x : Gal(K/k)) ↦ σ • x) 1 = σ

Tactic:
simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]

Premises used: and_true, Subgroup.one_mem, SetLike.mem_coe, smul_eq_mul, mul_one
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
a : IntermediateField.fixedField L.fixingSubgroup ≤ L
a₁ : L ≤ IntermediateField.fixedField L.fixingSubgroup
⊢ IntermediateField.fixedField L.fixingSubgroup = L

Tactic:
apply le_antisymm

Premises used: le_antisymm