-- 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:
have : ((restrictNormalHom L') h ⟨y,hy⟩).1 = ((restrictNormalHom L') σ ⟨y,hy⟩).1 := by rw [eq]

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
this :
  ↑(((restrictNormalHom ↥L'.toIntermediateField) h) ⟨y, hy⟩) =
    ↑(((restrictNormalHom ↥L'.toIntermediateField) σ) ⟨y, hy⟩)
⊢ σ⁻¹ (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
y : ↥L'.toIntermediateField
hy : y ∈ ↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H))
⊢ (restrictNormalHom ↥L'.toIntermediateField) σ • y = y

Tactic:
apply Subtype.val_injective

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

Tactic:
rcases nhd with ⟨b, ⟨gp, ⟨L, hL, eq'⟩, eq⟩, sub⟩

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

Tactic:
rintro φ ⟨τ, hτ, muleq⟩

Result:
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) τ = φ
⊢ φ ∈ (↑H).carrierᶜ