-- Mathlib/FieldTheory/Galois/Infinite.lean
lemma fixingSubgroup_isClosed (L : IntermediateField k K) [IsGalois k K] :
    IsClosed (L.fixingSubgroup : Set (K ≃ₐ[k] K)) where
  isOpen_compl := isOpen_iff_mem_nhds.mpr fun σ h => by
    apply mem_nhds_iff.mpr
    rcases Set.not_subset.mp ((mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mp h) with ⟨y, yL, ne⟩
    use σ • ((adjoin k {y}).1.fixingSubgroup : Set (K ≃ₐ[k] K))
    constructor
    · intro f hf
      rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩
      simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]
      apply (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mpr
      push_neg
      use y
      simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and]
      have : g y = y := (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).mp hg y <|
        adjoin_simple_le_iff.mp le_rfl
      simpa only [this, ne_eq, AlgEquiv.smul_def] using ne
    · simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and]
      use 1
      simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]

Proof state:
case h.left.intro.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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : K ≃ₐ[k] K
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ σ • g ∉ L.fixingSubgroup

Tactic:
apply (mem_fixingSubgroup_iff (K ≃ₐ[k] K)).not.mpr

Result:
case h.left.intro.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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : K ≃ₐ[k] K
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ ¬∀ y ∈ ↑L, (σ • g) • y = y

Proof state:
case h
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : K ≃ₐ[k] K
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
this : g y = y
⊢ ¬σ (g y) = y

Tactic:
simpa only [this, ne_eq, AlgEquiv.smul_def] using ne

Result:
no goals

Proof state:
case h.left
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
⊢ f ∈ (↑L.fixingSubgroup)ᶜ

Tactic:
rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩

Result:
case h.left.intro.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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : K ≃ₐ[k] K
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ f ∈ (↑L.fixingSubgroup)ᶜ

Proof state:
case h
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
⊢ 1 ∈ ↑(adjoin k {y}).fixingSubgroup ∧ (fun x => σ • x) 1 = σ

Tactic:
simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]

Result:
no goals

Proof state:
case h.right
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
⊢ σ ∈ σ • ↑(adjoin k {y}).fixingSubgroup

Tactic:
use 1

Result:
case h
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
⊢ 1 ∈ ↑(adjoin k {y}).fixingSubgroup ∧ (fun x => σ • x) 1 = σ

Proof state:
case h.left
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
⊢ σ • ↑(adjoin k {y}).fixingSubgroup ⊆ (↑L.fixingSubgroup)ᶜ

Tactic:
intro f hf

Result:
case h.left
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
⊢ f ∈ (↑L.fixingSubgroup)ᶜ

Proof state:
case h
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : K ≃ₐ[k] K
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ y ∈ ↑L ∧ (σ • g) • y ≠ y

Tactic:
simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and]

Result:
case h
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : K ≃ₐ[k] K
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ ¬σ (g y) = y

Proof state:
case h.right
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
⊢ IsOpen (σ • ↑(adjoin k {y}).fixingSubgroup) ∧ σ ∈ σ • ↑(adjoin k {y}).fixingSubgroup

Tactic:
simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and]

Result:
case h.right
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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
⊢ σ ∈ σ • ↑(adjoin k {y}).fixingSubgroup

Proof state:
case h.left.intro.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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : K ≃ₐ[k] K
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ f ∈ (↑L.fixingSubgroup)ᶜ

Tactic:
simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]

Result:
case h.left.intro.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
σ : K ≃ₐ[k] K
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a => σ • a = a
f : K ≃ₐ[k] K
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : K ≃ₐ[k] K
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ σ • g ∉ L.fixingSubgroup