-- Mathlib/FieldTheory/Galois/Infinite.lean
lemma fixingSubgroup_fixedField (H : ClosedSubgroup (K ≃ₐ[k] K)) [IsGalois k K] :
    (IntermediateField.fixedField H).fixingSubgroup = H.1

Proof state:
case intro.intro.intro.intro.intro.intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup (K ≃ₐ[k] K)
inst✝ : IsGalois k K
σ : K ≃ₐ[k] K
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set (K ≃ₐ[k] K)
sub : b ⊆ (fun y => σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
eq : (fun g => g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  FiniteGaloisIntermediateField.mk __src
⊢ False

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 (IntermediateField.fixingSubgroup.antimono (IntermediateField.le_normalClosure L) hτ)

Result:
case intro.intro.intro.intro.intro.intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup (K ≃ₐ[k] K)
inst✝ : IsGalois k K
σ : K ≃ₐ[k] K
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set (K ≃ₐ[k] K)
sub : b ⊆ (fun y => σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
eq : (fun g => g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  FiniteGaloisIntermediateField.mk __src
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup (K ≃ₐ[k] K)
inst✝ : IsGalois k K
σ : K ≃ₐ[k] K
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set (K ≃ₐ[k] K)
sub : b ⊆ (fun y => σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
eq✝ : (fun g => g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  FiniteGaloisIntermediateField.mk __src
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : K ≃ₐ[k] K
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
this : h ∈ σ • L'.fixingSubgroup.carrier
⊢ ¬σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ

Tactic:
apply Set.not_subset.mpr

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup (K ≃ₐ[k] K)
inst✝ : IsGalois k K
σ : K ≃ₐ[k] K
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set (K ≃ₐ[k] K)
sub : b ⊆ (fun y => σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
eq✝ : (fun g => g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  FiniteGaloisIntermediateField.mk __src
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : K ≃ₐ[k] K
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
this : h ∈ σ • L'.fixingSubgroup.carrier
⊢ ∃ a ∈ σ • L'.fixingSubgroup.carrier, a ∉ (↑H).carrierᶜ

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup (K ≃ₐ[k] K)
inst✝ : IsGalois k K
σ : K ≃ₐ[k] K
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set (K ≃ₐ[k] K)
sub : b ⊆ (fun y => σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
eq✝ : (fun g => g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  FiniteGaloisIntermediateField.mk __src
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : K ≃ₐ[k] K
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
y : K
hy : y ∈ ↑L'.toIntermediateField
⊢ ↑(((restrictNormalHom ↥L'.toIntermediateField) h) ⟨y, hy⟩) =
    ↑(((restrictNormalHom ↥L'.toIntermediateField) σ) ⟨y, hy⟩)

Tactic:
rw [eq]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup (K ≃ₐ[k] K)
inst✝ : IsGalois k K
σ : K ≃ₐ[k] K
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set (K ≃ₐ[k] K)
sub : b ⊆ (fun y => σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
eq : (fun g => g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  FiniteGaloisIntermediateField.mk __src
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
this : (restrictNormalHom ↥L'.toIntermediateField) σ ∈ Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H
⊢ False

Tactic:
rcases this with ⟨h, mem, eq⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup (K ≃ₐ[k] K)
inst✝ : IsGalois k K
σ : K ≃ₐ[k] K
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set (K ≃ₐ[k] K)
sub : b ⊆ (fun y => σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
eq✝ : (fun g => g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  FiniteGaloisIntermediateField.mk __src
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : K ≃ₐ[k] K
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
⊢ False