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 : σ ∉ (↑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 : (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 := ⋯ }
φ τ : Gal(K/k)
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun (x : Gal(K/k)) ↦ σ • x) τ = φ
sub' : σ • b ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
⊢ τ ∈ L.fixingSubgroup.carrier

Tactic:
exact (L.fixingSubgroup_le (IntermediateField.le_normalClosure L) hτ)

Premises used: IntermediateField.fixingSubgroup_le, IntermediateField.le_normalClosure
-- 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 : σ ∉ (↑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 : (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 := ⋯ }
⊢ σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ

Tactic:
have compl : σ • L'.1.fixingSubgroup.carrier ⊆ H.carrierᶜ := by
    rintro φ ⟨τ, hτ, muleq⟩
    have sub' : σ • b ⊆ H.carrierᶜ := Set.smul_set_subset_iff.mpr sub
    apply sub'
    simp only [← muleq, ← eq]
    apply Set.smul_mem_smul_set
    exact (L.fixingSubgroup_le (IntermediateField.le_normalClosure L) 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 : σ ∉ (↑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 : (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ᶜ
⊢ ∀ x ∈ fixedField (↑H : Subgroup Gal(K/k)) ⊓ L'.toIntermediateField, (σ : (a : K) → K) x = x

Tactic:
have fix : ∀ x ∈ IntermediateField.fixedField H.toSubgroup ⊓ ↑L', σ x = x :=
    fun x hx ↦ ((mem_fixingSubgroup_iff Gal(K/k)).mp hσ) x hx.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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑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 : (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 ∈ fixedField (↑H : Subgroup Gal(K/k)) ⊓ L'.toIntermediateField, (σ : (a : K) → K) x = x
⊢ ∀ (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

Tactic:
rw [restrict_fixedField H.1 L'.1] at fix

Premises used: ClosedSubgroup.toSubgroup, InfiniteGalois.restrict_fixedField, FiniteGaloisIntermediateField.toIntermediateField
-- 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 : σ ∉ (↑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 : (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
rw :
  Membership.mem (α := Gal(↥L'.toIntermediateField/k)) (γ := Subgroup Gal(↥L'.toIntermediateField/k))
    (IntermediateField.fixingSubgroup
      (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
⊢ Membership.mem (α := Gal(↥L'.toIntermediateField/k)) (γ := Subgroup Gal(↥L'.toIntermediateField/k))
    (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))

Tactic:
rw [← IntermediateField.fixingSubgroup_fixedField (Subgroup.map (restrictNormalHom L') H.1)]

Premises used: ClosedSubgroup.toSubgroup, Subgroup.map, IntermediateField.fixingSubgroup_fixedField, Membership.mem, Subtype, AlgEquiv.restrictNormalHom, FiniteGaloisIntermediateField.toIntermediateField
-- 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 : σ ∉ (↑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 : (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
apply :
  ∀
    y ∈
      (↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))) :
        Set ↥L'.toIntermediateField),
    HSMul.hSMul (α := Gal(↥L'.toIntermediateField/k))
        ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
          Gal(↥L'.toIntermediateField/k))
        y =
      y
⊢ Membership.mem (α := Gal(↥L'.toIntermediateField/k)) (γ := Subgroup Gal(↥L'.toIntermediateField/k))
    (IntermediateField.fixingSubgroup
      (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))

Tactic:
apply (mem_fixingSubgroup_iff (L' ≃ₐ[k] L')).mpr

Premises used: Iff.mpr, Membership.mem, Subtype, AlgEquiv, FiniteGaloisIntermediateField.toIntermediateField, 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑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 : (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
y : ↥L'.toIntermediateField
hy :
  y ∈
    (↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))) :
      Set ↥L'.toIntermediateField)
a :
  (↑(HSMul.hSMul (α := Gal(↥L'.toIntermediateField/k))
          ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
            Gal(↥L'.toIntermediateField/k))
          y) :
      K) =
    (↑y : K)
⊢ HSMul.hSMul (α := Gal(↥L'.toIntermediateField/k))
      ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
        Gal(↥L'.toIntermediateField/k))
      y =
    y

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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑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 : (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
y : ↥L'.toIntermediateField
hy :
  y ∈
    (↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))) :
      Set ↥L'.toIntermediateField)
⊢ (↑(HSMul.hSMul (α := Gal(↥L'.toIntermediateField/k))
          ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
            Gal(↥L'.toIntermediateField/k))
          y) :
      K) =
    (↑y : K)

Tactic:
simp only [AlgEquiv.smul_def, restrictNormalHom_apply L'.1 σ y,
      fix y.1 ((IntermediateField.mem_lift y).mpr hy)]

Premises used: Iff.mpr, AlgEquiv.smul_def, IntermediateField.mem_lift, FiniteGaloisIntermediateField.toIntermediateField, AlgEquiv.restrictNormalHom_apply, 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
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑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 : (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
⊢ Membership.mem (α := Gal(↥L'.toIntermediateField/k)) (γ := Subgroup Gal(↥L'.toIntermediateField/k))
    (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))

Tactic:
have : (restrictNormalHom L') σ ∈ (Subgroup.map (restrictNormalHom L') H.1) := by
    rw [← IntermediateField.fixingSubgroup_fixedField (Subgroup.map (restrictNormalHom L') H.1)]
    apply (mem_fixingSubgroup_iff (L' ≃ₐ[k] L')).mpr
    intro y hy
    apply Subtype.val_injective
    simp only [AlgEquiv.smul_def, restrictNormalHom_apply L'.1 σ y,
      fix y.1 ((IntermediateField.mem_lift y).mpr hy)]
-- 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 : σ ∉ (↑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 : (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
this :
  Membership.mem (α := Gal(↥L'.toIntermediateField/k)) (γ := Subgroup Gal(↥L'.toIntermediateField/k))
    (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
rcases :
  ∀ (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))),
    False
⊢ False

Tactic:
rcases this with ⟨h, mem, 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))
h₁ : σ⁻¹ * h ∈ L'.fixingSubgroup.carrier ∧ (fun (x : Gal(K/k)) ↦ σ • x) (σ⁻¹ * h) = h
⊢ h ∈ σ • L'.fixingSubgroup.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 : 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₁ : σ⁻¹ * h ∈ L'.fixingSubgroup
⊢ σ⁻¹ * h ∈ L'.fixingSubgroup.carrier ∧ (fun (x : Gal(K/k)) ↦ σ • x) (σ⁻¹ * h) = h

Tactic:
simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid,
      smul_eq_mul, mul_inv_cancel_left, and_true]

Premises used: Submonoid.mem_toSubsemigroup, and_true, Subgroup.mem_toSubmonoid, smul_eq_mul, mul_inv_cancel_left, 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
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₁ : ∀ y ∈ (↑L'.toIntermediateField : Set K), (σ⁻¹ * h) • y = y
⊢ σ⁻¹ * h ∈ L'.fixingSubgroup

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

Premises used: Iff.mpr, 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
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)
h₁ : (σ⁻¹ : (a : K) → K) ((h : (a : K) → K) y : K) = y
⊢ (σ⁻¹ * h) • y = y

Tactic:
simp only [AlgEquiv.smul_def, AlgEquiv.mul_apply]

Premises used: AlgEquiv.smul_def, AlgEquiv.mul_apply