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

Proof state:
case a.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 ⊤ = ⊥
this : ⟨x, mem⟩ ∈ ⊥
y : ↥L
hy : (algebraMap ↥L ↥(adjoin ↥L {x}).toIntermediateField) y = ⟨x, mem⟩
⊢ x ∈ L

Tactic:
obtain ⟨rfl⟩ : y = x := congrArg Subtype.val hy

Result:
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

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
⊢ IntermediateField.fixedField L.fixingSubgroup ≤ L

Tactic:
intro x hx

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 : x ∈ IntermediateField.fixedField L.fixingSubgroup
⊢ x ∈ 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 ∈ ⊤, f ⟨x, mem⟩ = ⟨x, mem⟩

Tactic:
intro f _

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 : ↥(adjoin ↥L {x}).toIntermediateField ≃ₐ[↥L] ↥(adjoin ↥L {x}).toIntermediateField
a✝ : 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
⊢ L ≤ IntermediateField.fixedField L.fixingSubgroup

Tactic:
exact (IntermediateField.le_iff_le L.fixingSubgroup L).mpr le_rfl

Result:
no goals

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
⊢ IntermediateField.fixedField L.fixingSubgroup = L

Tactic:
apply le_antisymm

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
⊢ IntermediateField.fixedField L.fixingSubgroup ≤ L

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
⊢ L ≤ IntermediateField.fixedField L.fixingSubgroup

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
⊢ IsGalois ↥L ↥(adjoin ↥L {x}).toIntermediateField

Tactic:
infer_instance

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
this : IntermediateField.fixedField ⊤ = ⊥
⊢ x ∈ L

Tactic:
have : ⟨x, mem⟩ ∈ (⊥ : IntermediateField L (adjoin L {x})) := by
  rw [← this, IntermediateField.mem_fixedField_iff]
  intro f _
  rcases restrictNormalHom_surjective K f with ⟨σ,hσ⟩
  apply Subtype.val_injective
  rw [← hσ, restrictNormalHom_apply (adjoin L {x}).1 σ ⟨x, mem⟩]
  have := hx ((IntermediateField.fixingSubgroupEquiv L).symm σ)
  simpa only [SetLike.coe_mem, true_implies]

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 ⊤ = ⊥
this : ⟨x, mem⟩ ∈ ⊥
⊢ x ∈ L

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 : x ∈ IntermediateField.fixedField L.fixingSubgroup
⊢ x ∈ L

Tactic:
rw [IntermediateField.mem_fixedField_iff] at hx

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
⊢ x ∈ L

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
this✝ : IntermediateField.fixedField ⊤ = ⊥
this : ⟨x, mem⟩ ∈ ⊥
⊢ x ∈ L

Tactic:
rcases IntermediateField.mem_bot.mp this with ⟨y, hy⟩

Result:
case a.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 ⊤ = ⊥
this : ⟨x, mem⟩ ∈ ⊥
y : ↥L
hy : (algebraMap ↥L ↥(adjoin ↥L {x}).toIntermediateField) y = ⟨x, mem⟩
⊢ x ∈ L