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
L : IntermediateField k K
inst_3 : IsGalois k K
x : K
hx : x ∈ IntermediateField.fixedField L.fixingSubgroup
⊢ ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x

Tactic:
rw [IntermediateField.mem_fixedField_iff] at hx

Premises used: IntermediateField.mem_fixedField_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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
⊢ Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x

Tactic:
have mem : x ∈ (adjoin L {x}).1 := subset_adjoin _ _ 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
⊢ IsGalois.{u_2, u_2} ↥L ↥(toIntermediateField (adjoin ↥L {x}))

Tactic:
infer_instance
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
⊢ Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥

Tactic:
have : IntermediateField.fixedField (⊤ : Subgroup ((adjoin L {x}) ≃ₐ[L] (adjoin L {x}))) = ⊥ :=
      (IsGalois.tfae.out 0 1).mp (by infer_instance)
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
rw :
  ∀ (f : Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)),
    Membership.mem (γ := Subgroup Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)) ⊤ f →
      (f : (a : ↥(adjoin ↥L {x}).toIntermediateField) → ↥(adjoin ↥L {x}).toIntermediateField)
          (Subtype.mk (p := fun (x_1 : K) ↦
            Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) =
        Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem
⊢ Membership.mem (γ := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) ⊥
    (Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem)

Tactic:
rw [← this, IntermediateField.mem_fixedField_iff]

Premises used: IntermediateField.mem_fixedField_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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
f : Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)
_ :
  Membership.mem (γ := Subgroup Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)) ⊤ f →
    (f : (a : ↥(adjoin ↥L {x}).toIntermediateField) → ↥(adjoin ↥L {x}).toIntermediateField)
        (Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) =
      Subtype.mk (p := fun (x_1 : K) ↦
        Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem
⊢ Membership.mem (γ := Subgroup Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)) ⊤ f →
    (f : (a : ↥(adjoin ↥L {x}).toIntermediateField) → ↥(adjoin ↥L {x}).toIntermediateField)
        (Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) =
      Subtype.mk (p := fun (x_1 : K) ↦
        Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem

Tactic:
_
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
f : Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)
h : Membership.mem (γ := Subgroup Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)) ⊤ f
rcases :
  ∀ (σ : Gal(K/↥L))
    (hσ :
      (restrictNormalHom ↥(toIntermediateField (adjoin ↥L {x})) :
            (a : Gal(K/↥L)) → Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L))
          σ =
        f),
    (f : (a : ↥(adjoin ↥L {x}).toIntermediateField) → ↥(adjoin ↥L {x}).toIntermediateField)
        (Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) =
      Subtype.mk (p := fun (x_1 : K) ↦
        Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem
⊢ (f : (a : ↥(adjoin ↥L {x}).toIntermediateField) → ↥(adjoin ↥L {x}).toIntermediateField)
      (Subtype.mk (p := fun (x_1 : K) ↦
        Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) =
    Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem

Tactic:
rcases restrictNormalHom_surjective K f with ⟨σ, hσ⟩

Premises used: AlgEquiv.restrictNormalHom_surjective
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
f : Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)
h : Membership.mem (γ := Subgroup Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)) ⊤ f
σ : Gal(K/↥L)
hσ :
  (restrictNormalHom ↥(toIntermediateField (adjoin ↥L {x})) :
        (a : Gal(K/↥L)) → Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L))
      σ =
    f
a :
  (↑((f : (a : ↥(adjoin ↥L {x}).toIntermediateField) → ↥(adjoin ↥L {x}).toIntermediateField)
          (Subtype.mk (p := fun (x_1 : K) ↦
            Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem)) :
      K) =
    (↑(Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) :
      K)
⊢ (f : (a : ↥(adjoin ↥L {x}).toIntermediateField) → ↥(adjoin ↥L {x}).toIntermediateField)
      (Subtype.mk (p := fun (x_1 : K) ↦
        Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) =
    Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem

Tactic:
apply Subtype.val_injective

Premises used: Subtype.val_injective
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
f : Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)
h : Membership.mem (γ := Subgroup Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)) ⊤ f
σ : Gal(K/↥L)
hσ :
  (restrictNormalHom ↥(toIntermediateField (adjoin ↥L {x})) :
        (a : Gal(K/↥L)) → Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L))
      σ =
    f
a :
  (σ : (a : K) → K)
      (↑(Subtype.mk (p := fun (x_1 : K) ↦
            Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) :
        K) =
    (↑(Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) :
      K)
⊢ (↑((f : (a : ↥(adjoin ↥L {x}).toIntermediateField) → ↥(adjoin ↥L {x}).toIntermediateField)
          (Subtype.mk (p := fun (x_1 : K) ↦
            Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem)) :
      K) =
    (↑(Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) :
      K)

Tactic:
rw [← hσ, restrictNormalHom_apply (adjoin L {x}).1 σ ⟨x, mem⟩]

Premises used: Membership.mem, Subtype, Subtype.mk, FiniteGaloisIntermediateField.adjoin, FiniteGaloisIntermediateField.toIntermediateField, AlgEquiv.restrictNormalHom_apply, 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
f : Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)
h : Membership.mem (γ := Subgroup Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)) ⊤ f
σ : Gal(K/↥L)
hσ :
  (restrictNormalHom ↥(toIntermediateField (adjoin ↥L {x})) :
        (a : Gal(K/↥L)) → Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L))
      σ =
    f
⊢ (↑((L.fixingSubgroupEquiv.symm : (a : Gal(K/↥L)) → ↥L.fixingSubgroup) σ) : Gal(K/k)) ∈ L.fixingSubgroup →
    ((↑((L.fixingSubgroupEquiv.symm : (a : Gal(K/↥L)) → ↥L.fixingSubgroup) σ) : Gal(K/k)) : (a : K) → K) x = x

Tactic:
have := hx ((IntermediateField.fixingSubgroupEquiv L).symm σ)
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this_1 :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
f : Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)
h : Membership.mem (γ := Subgroup Gal(↥(toIntermediateField (adjoin ↥L {x}))/↥L)) ⊤ f
σ : Gal(K/↥L)
hσ :
  (restrictNormalHom ↥(toIntermediateField (adjoin ↥L {x})) :
        (a : Gal(K/↥L)) → Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L))
      σ =
    f
this :
  (↑((L.fixingSubgroupEquiv.symm : (a : Gal(K/↥L)) → ↥L.fixingSubgroup) σ) : Gal(K/k)) ∈ L.fixingSubgroup →
    ((↑((L.fixingSubgroupEquiv.symm : (a : Gal(K/↥L)) → ↥L.fixingSubgroup) σ) : Gal(K/k)) : (a : K) → K) x = x
⊢ (σ : (a : K) → K)
      (↑(Subtype.mk (p := fun (x_1 : K) ↦
            Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) :
        K) =
    (↑(Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem) :
      K)

Tactic:
simpa only [SetLike.coe_mem, true_implies]

Premises used: SetLike.coe_mem, true_implies
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
⊢ Membership.mem (γ := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) ⊥
    (Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem)

Tactic:
have : ⟨x, mem⟩ ∈ (⊥ : IntermediateField L (adjoin L {x})) := by
      rw [← this, IntermediateField.mem_fixedField_iff]
      intro f _
      rcases restrictNormalHom_surjective K f with ⟨σ, hσ⟩
      apply Subtype.val_injective
      rw [← hσ, restrictNormalHom_apply (adjoin L {x}).1 σ ⟨x, mem⟩]
      have := hx ((IntermediateField.fixingSubgroupEquiv L).symm σ)
      simpa only [SetLike.coe_mem, true_implies]
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this_1 :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
this :
  Membership.mem (γ := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) ⊥
    (Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem)
a :
  ∀ (y : ↥L)
    (hy :
      (algebraMap ↥L ↥(toIntermediateField (adjoin ↥L {x})) : (a : ↥L) → ↥(adjoin ↥L {x}).toIntermediateField) y =
        Subtype.mk (p := fun (x_1 : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem),
    x ∈ L
⊢ x ∈ L

Tactic:
rcases IntermediateField.mem_bot.mp this with ⟨y, hy⟩

Premises used: Iff.mp, IntermediateField.mem_bot
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this_1 :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
this :
  Membership.mem (γ := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) ⊥
    (Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem)
y : ↥L
hy :
  (algebraMap ↥L ↥(toIntermediateField (adjoin ↥L {x})) : (a : ↥L) → ↥(adjoin ↥L {x}).toIntermediateField) y =
    Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem
⊢ (↑y : K) = x

Tactic:
congrArg Subtype.val hy

Premises used: iInf, congrArg, Set.Mem, Set.iInter, setOf, Subtype.val
-- 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) x = x
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x
this_1 :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) (IntermediateField.fixedField ⊤) ⊥
this :
  Membership.mem (γ := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {x}))) ⊥
    (Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem)
y : ↥L
hy :
  (algebraMap ↥L ↥(toIntermediateField (adjoin ↥L {x})) : (a : ↥L) → ↥(adjoin ↥L {x}).toIntermediateField) y =
    Subtype.mk (p := fun (x_1 : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {x})) x_1) x mem
a :
  ∀ (hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) (↑y : K) = (↑y : K))
    (mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) (↑y : K))
    (this :
      Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)})))
        (IntermediateField.fixedField ⊤) ⊥)
    (this :
      Membership.mem (γ := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)}))) ⊥
        (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) x) (↑y : K) mem))
    (hy :
      (algebraMap ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)})) :
            (a : ↥L) → ↥(adjoin ↥L {(↑y : K)}).toIntermediateField)
          y =
        Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) x) (↑y : K) mem),
    (↑y : K) ∈ L
⊢ x ∈ L

Tactic:
obtain ⟨rfl⟩ : y = x := congrArg Subtype.val hy

Premises used: congrArg, Subtype.val, 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
y : ↥L
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) (↑y : K) = (↑y : K)
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) (↑y : K)
this_1 :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)})))
    (IntermediateField.fixedField ⊤) ⊥
this :
  Membership.mem (γ := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)}))) ⊥
    (Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) x) (↑y : K) mem)
hy :
  (algebraMap ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)})) : (a : ↥L) → ↥(adjoin ↥L {(↑y : K)}).toIntermediateField)
      y =
    Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) x) (↑y : K) mem
⊢ (↑y : K) ∈ L

Tactic:
y.2

Premises used: Subtype.property
-- 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
y : ↥L
hx : ∀ f ∈ L.fixingSubgroup, (f : (a : K) → K) (↑y : K) = (↑y : K)
mem : Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) (↑y : K)
this_1 :
  Eq.{u_2 + 1} (α := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)})))
    (IntermediateField.fixedField ⊤) ⊥
this :
  Membership.mem (γ := IntermediateField ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)}))) ⊥
    (Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) x) (↑y : K) mem)
hy :
  (algebraMap ↥L ↥(toIntermediateField (adjoin ↥L {(↑y : K)})) : (a : ↥L) → ↥(adjoin ↥L {(↑y : K)}).toIntermediateField)
      y =
    Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := IntermediateField (↥L) K) (toIntermediateField (adjoin ↥L {(↑y : K)})) x) (↑y : K) mem
⊢ (↑y : K) ∈ L

Tactic:
exact y.2

Premises used: Subtype.property
-- 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
⊢ L ≤ IntermediateField.fixedField L.fixingSubgroup

Tactic:
(IntermediateField.le_iff_le L.fixingSubgroup L).mpr le_rfl

Premises used: Iff.mpr, le_rfl, IntermediateField.fixingSubgroup, IntermediateField.le_iff_le
-- 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
⊢ L ≤ IntermediateField.fixedField L.fixingSubgroup

Tactic:
exact (IntermediateField.le_iff_le L.fixingSubgroup L).mpr le_rfl

Premises used: Iff.mpr, le_rfl, IntermediateField.fixingSubgroup, IntermediateField.le_iff_le
-- 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
rw : Eq.{u_2 + 1} (α := IntermediateField k K) (IntermediateField.fixedField (IntermediateField.fixingSubgroup ⊥)) ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := IntermediateField k K) ⊥ ⊥
⊢ Eq.{u_2 + 1} (α := IntermediateField k K) (IntermediateField.fixedField ⊤) ⊥

Tactic:
rw [← IntermediateField.fixingSubgroup_bot, fixedField_fixingSubgroup]

Premises used: InfiniteGalois.fixedField_fixingSubgroup, IntermediateField.fixingSubgroup_bot
-- 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
x : K
⊢ Membership.mem (γ := IntermediateField k K) ⊥ x ↔ ∀ (f : Gal(K/k)), (f : (a : K) → K) x = x

Tactic:
simp [← fixedField_bot, IntermediateField.mem_fixedField_iff]

Premises used: IntermediateField.mem_fixedField_iff, InfiniteGalois.fixedField_bot
-- 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
x : K
⊢ Membership.mem (γ := Set K) (Set.range.{u_2, u_1 + 1} (ι := k) (⇑(algebraMap k K) : (a : k) → K)) x ↔
    ∀ (f : Gal(K/k)), (f : (a : K) → K) x = x

Tactic:
mem_bot_iff_fixed x

Premises used: InfiniteGalois.mem_bot_iff_fixed, Set.Mem, setOf, Set.range
-- 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 : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
h : (↑(fixedField H ⊓ L) : Set K) = (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)
⊢ fixedField H ⊓ L = lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))

Tactic:
apply SetLike.ext'

Premises used: SetLike.ext'
-- 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 : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
h :
  ∀ (x : K),
    x ∈ (↑(fixedField H ⊓ L) : Set K) ↔
      x ∈ (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)
⊢ (↑(fixedField H ⊓ L) : Set K) = (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)

Tactic:
ext x
-- 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 : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
⊢ x ∈ (↑(fixedField H ⊓ L) : Set K) ↔
    x ∈ (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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 : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h :
  ∀ (h : x ∈ (↑(fixedField H ⊓ L) : Set K)),
    x ∈ (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)
h₁ :
  ∀ (h : x ∈ (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)),
    x ∈ (↑(fixedField H ⊓ L) : Set K)
⊢ x ∈ (↑(fixedField H ⊓ L) : Set K) ↔
    x ∈ (↑(lift (F := L) (fixedField (Subgroup.map (restrictNormalHom ↥L) H))) : Set K)

Tactic:
refine ⟨fun h ↦ ?_, fun 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 : Subgroup Gal(K/k)
L : IntermediateField k K
inst_3 : Normal.{u_1, u_2} k ↥L
x : K
h : x ∈ (↑(fixedField H ⊓ L) : Set K)
⊢ Membership.mem (γ := Set K) ((fun (x : IntermediateField k K) ↦ (↑x : Set K)) L) x

Tactic:
have xL := h.out.2