awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
y : K
hy : y ∈ (↑L'.toIntermediateField : Set K)
rw rw₁ :
  Eq.{u_2 + 1} (α := K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
⊢ Eq.{u_2 + 1} (α := K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)

Tactic:
rw [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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
y : K
hy : y ∈ (↑L'.toIntermediateField : Set K)
⊢ Eq.{u_2 + 1} (α := K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)

Tactic:
have : ((restrictNormalHom L') h ⟨y,hy⟩).1 = ((restrictNormalHom L') σ ⟨y,hy⟩).1 := by rw [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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
y : K
hy : y ∈ (↑L'.toIntermediateField : Set K)
this :
  Eq.{u_2 + 1} (α := K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
⊢ Eq (α := K) ((h : (a : K) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy) : K) : K)
    ((σ : (a : K) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy) : K) : K)

Tactic:
rw [restrictNormalHom_apply L'.1 h ⟨y, hy⟩, restrictNormalHom_apply L'.1 σ ⟨y, hy⟩] at this

Premises used: Subtype.mk, FiniteGaloisIntermediateField.toIntermediateField, 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
y : K
hy : y ∈ (↑L'.toIntermediateField : Set K)
this :
  Eq (α := K) ((h : (a : K) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy) : K) : K)
    ((σ : (a : K) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy) : K) : K)
⊢ (σ⁻¹ : (a : K) → K) ((h : (a : K) → K) y : K) = y

Tactic:
simp only [this, ← AlgEquiv.mul_apply, inv_mul_cancel, one_apply]

Premises used: AlgEquiv.one_apply, inv_mul_cancel, AlgEquiv.mul_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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
⊢ h ∈ σ • L'.fixingSubgroup.carrier

Tactic:
have : h ∈ σ • L'.1.fixingSubgroup.carrier := by
    use σ⁻¹ * h
    simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid,
      smul_eq_mul, mul_inv_cancel_left, and_true]
    apply (mem_fixingSubgroup_iff Gal(K/k)).mpr
    intro y hy
    simp only [AlgEquiv.smul_def, AlgEquiv.mul_apply]
    have : ((restrictNormalHom L') h ⟨y,hy⟩).1 = ((restrictNormalHom L') σ ⟨y,hy⟩).1 := by rw [eq]
    rw [restrictNormalHom_apply L'.1 h ⟨y, hy⟩, restrictNormalHom_apply L'.1 σ ⟨y, hy⟩] at this
    simp only [this, ← AlgEquiv.mul_apply, inv_mul_cancel, one_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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
this : h ∈ σ • L'.fixingSubgroup.carrier
⊢ ¬?_mvar.59032

Tactic:
compl
-- 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
this : h ∈ σ • L'.fixingSubgroup.carrier
absurd : ¬σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
⊢ False

Tactic:
absurd compl
-- 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
this : h ∈ σ • L'.fixingSubgroup.carrier
apply : ∃ a ∈ σ • L'.fixingSubgroup.carrier, a ∉ (↑H : Subgroup Gal(K/k)).carrierᶜ
⊢ ¬σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ

Tactic:
apply Set.not_subset.mpr

Premises used: Iff.mpr, Set.not_subset
-- 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
this : h ∈ σ • L'.fixingSubgroup.carrier
h₁ : h ∈ σ • L'.fixingSubgroup.carrier ∧ h ∉ (↑H : Subgroup Gal(K/k)).carrierᶜ
⊢ ∃ a ∈ σ • L'.fixingSubgroup.carrier, a ∉ (↑H : Subgroup Gal(K/k)).carrierᶜ

Tactic:
use h
-- 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
this : h ∈ σ • L'.fixingSubgroup.carrier
⊢ h ∈ σ • L'.fixingSubgroup.carrier ∧ h ∉ (↑H : Subgroup Gal(K/k)).carrierᶜ

Tactic:
simpa only [this, Set.mem_compl_iff, Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup,
    Subgroup.mem_toSubmonoid, not_not, true_and] using mem

Premises used: Submonoid.mem_toSubsemigroup, Classical.not_not, Subgroup.mem_toSubmonoid, Set.mem_compl_iff, true_and, Subsemigroup.mem_carrier
-- 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
inst_3 : IsGalois k K
H : (ClosedSubgroup Gal(K/k))ᵒᵈ
simp_rw : { toSubgroup := (↑H : Subgroup Gal(K/k)), isClosed' := ⋯ : ClosedSubgroup Gal(K/k) } = H
⊢ (fun (L : IntermediateField k K) ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ : ClosedSubgroup Gal(K/k) })
      ((fun (H : (ClosedSubgroup Gal(K/k))ᵒᵈ) ↦ IntermediateField.fixedField (↑H : Subgroup Gal(K/k))) H) =
    H

Tactic:
simp_rw [fixingSubgroup_fixedField H]

Premises used: InfiniteGalois.fixingSubgroup_fixedField
-- 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
inst_3 : IsGalois k K
H : (ClosedSubgroup Gal(K/k))ᵒᵈ
⊢ { toSubgroup := (↑H : Subgroup Gal(K/k)), isClosed' := ⋯ : ClosedSubgroup Gal(K/k) } = H

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Galois.Infinite
Goal:
k : Type u_1
K_1 : Type u_2
inst : Field k
inst_1 : Field K_1
inst_2 : Algebra k K_1
inst_3 : IsGalois k K_1
K L : IntermediateField k K_1
rw :
  LE.le (α := (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
      (({ toFun := fun (L : IntermediateField k K_1) ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
              invFun := fun (H : (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↦
                IntermediateField.fixedField (↑H : Subgroup Gal(K_1/k)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField k K_1) → (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
          K :
        (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
      (({ toFun := fun (L : IntermediateField k K_1) ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
              invFun := fun (H : (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↦
                IntermediateField.fixedField (↑H : Subgroup Gal(K_1/k)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField k K_1) → (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
          L :
        (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↔
    L.fixingSubgroup ≤ K.fixingSubgroup
⊢ LE.le (α := (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
      (({ toFun := fun (L : IntermediateField k K_1) ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
              invFun := fun (H : (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↦
                IntermediateField.fixedField (↑H : Subgroup Gal(K_1/k)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField k K_1) → (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
          K :
        (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
      (({ toFun := fun (L : IntermediateField k K_1) ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
              invFun := fun (H : (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↦
                IntermediateField.fixedField (↑H : Subgroup Gal(K_1/k)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField k K_1) → (ClosedSubgroup Gal(K_1/k))ᵒᵈ)
          L :
        (ClosedSubgroup Gal(K_1/k))ᵒᵈ) ↔
    K ≤ L

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

Premises used: InfiniteGalois.fixedField_fixingSubgroup, IntermediateField.le_iff_le