-- Mathlib/FieldTheory/Galois/Infinite.lean
lemma fixedField_fixingSubgroup (L : IntermediateField k K) [IsGalois k K] :
    IntermediateField.fixedField L.fixingSubgroup = L

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
⊢ f ⟨x, mem⟩ = ⟨x, mem⟩

Tactic:
rcases restrictNormalHom_surjective K f with ⟨σ,hσ⟩

Result:
case intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
σ : K ≃ₐ[↥L] K
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ f ⟨x, mem⟩ = ⟨x, mem⟩

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
⊢ ⟨x, mem⟩ ∈ ⊥

Tactic:
rw [← this, IntermediateField.mem_fixedField_iff]

Result:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
⊢ ∀ f ∈ ⊤, f ⟨x, mem⟩ = ⟨x, mem⟩

Proof state:
case intro
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
σ : K ≃ₐ[↥L] K
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ f ⟨x, mem⟩ = ⟨x, mem⟩

Tactic:
apply Subtype.val_injective

Result:
case intro.a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
σ : K ≃ₐ[↥L] K
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ ↑(f ⟨x, mem⟩) = ↑⟨x, mem⟩

Proof state:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
⊢ x ∈ L

Tactic:
have mem : x ∈ (adjoin L {x}).1 := subset_adjoin _ _ rfl

Result:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
⊢ x ∈ L

Proof state:
case a.intro.refl
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
y : ↥L
hx : ∀ f ∈ L.fixingSubgroup, f ↑y = ↑y
mem : ↑y ∈ (adjoin ↥L {↑y}).toIntermediateField
this✝ : IntermediateField.fixedField ⊤ = ⊥
this : ⟨↑y, mem⟩ ∈ ⊥
hy : (algebraMap ↥L ↥(adjoin ↥L {↑y}).toIntermediateField) y = ⟨↑y, mem⟩
⊢ ↑y ∈ L

Tactic:
exact y.2

Result:
no goals

Proof state:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
⊢ x ∈ L

Tactic:
have : IntermediateField.fixedField (⊤ : Subgroup ((adjoin L {x}) ≃ₐ[L] (adjoin L {x}))) = ⊥ :=
  (IsGalois.tfae.out 0 1).mp (by infer_instance)

Result:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
⊢ x ∈ L

Proof state:
case intro.a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this✝ : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
σ : K ≃ₐ[↥L] K
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
this : ↑(L.fixingSubgroupEquiv.symm σ) ∈ L.fixingSubgroup → ↑(L.fixingSubgroupEquiv.symm σ) x = x
⊢ σ ↑⟨x, mem⟩ = ↑⟨x, mem⟩

Tactic:
simpa only [SetLike.coe_mem, true_implies]

Result:
no goals

Proof state:
case intro.a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
σ : K ≃ₐ[↥L] K
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ ↑(f ⟨x, mem⟩) = ↑⟨x, mem⟩

Tactic:
rw [← hσ, restrictNormalHom_apply (adjoin L {x}).1 σ ⟨x, mem⟩]

Result:
case intro.a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
σ : K ≃ₐ[↥L] K
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ σ ↑⟨x, mem⟩ = ↑⟨x, mem⟩

Proof state:
case intro.a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
σ : K ≃ₐ[↥L] K
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ σ ↑⟨x, mem⟩ = ↑⟨x, mem⟩

Tactic:
have := hx ((IntermediateField.fixingSubgroupEquiv L).symm σ)

Result:
case intro.a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this✝ : IntermediateField.fixedField ⊤ = ⊥
f : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : f ∈ ⊤
σ : K ≃ₐ[↥L] K
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
this : ↑(L.fixingSubgroupEquiv.symm σ) ∈ L.fixingSubgroup → ↑(L.fixingSubgroupEquiv.symm σ) x = x
⊢ σ ↑⟨x, mem⟩ = ↑⟨x, mem⟩