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

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)]

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

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

Tactic:
have nhd : H.carrierᶜ ∈ nhds σ := H.isClosed'.isOpen_compl.mem_nhds h

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ᶜ ∈ nhds σ
⊢ False

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

Tactic:
by_contra h

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