-- 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 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) σ
y : K
hy : y ∈ ↑L'.toIntermediateField
⊢ (σ⁻¹ * h) • y = y

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

Result:
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) σ
y : K
hy : y ∈ ↑L'.toIntermediateField
⊢ σ⁻¹ (h 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
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) σ ∈ Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H

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

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

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) σ
⊢ h ∈ σ • L'.fixingSubgroup.carrier

Tactic:
use σ⁻¹ * h

Result:
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) σ
⊢ σ⁻¹ * h ∈ L'.fixingSubgroup.carrier ∧ (fun x => σ • x) (σ⁻¹ * h) = h

Proof state:
case 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
φ τ : K ≃ₐ[k] K
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun x => σ • x) τ = φ
sub' : σ • b ⊆ (↑H).carrierᶜ
⊢ φ ∈ (↑H).carrierᶜ

Tactic:
apply sub'

Result:
case intro.intro.a
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
φ τ : K ≃ₐ[k] K
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun x => σ • x) τ = φ
sub' : σ • b ⊆ (↑H).carrierᶜ
⊢ φ ∈ σ • b