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

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
⊢ (restrictNormalHom ↥L'.toIntermediateField) σ ∈
    (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)).fixingSubgroup

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

Result:
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
⊢ ∀ y ∈ ↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)),
    (restrictNormalHom ↥L'.toIntermediateField) σ • y = y

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
nhd : (↑H).carrierᶜ ∈ nhds σ
⊢ False

Tactic:
rw [GroupFilterBasis.nhds_eq (x₀ := σ) (galGroupBasis k K)] at nhd

Result:
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
nhd : (↑H).carrierᶜ ∈ (galGroupBasis k K).N σ
⊢ False

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)
eq : (fun g => g.carrier) gp = b
L : IntermediateField k K
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
⊢ False

Tactic:
rw [← eq'] at eq

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
⊢ False

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 ∈ fixedField ↑H ⊓ L'.toIntermediateField, σ x = x
⊢ False

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

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ᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
⊢ False

Proof state:
case h
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
⊢ h ∈ σ • L'.fixingSubgroup.carrier ∧ h ∉ (↑H).carrierᶜ

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

Result:
no goals