-- Mathlib/FieldTheory/KrullTopology.lean
lemma krullTopology_mem_nhds_one_iff_of_normal (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Normal K L] (s : Set (L ≃ₐ[K] L)) : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L,
    FiniteDimensional K E ∧ Normal K E ∧ (E.fixingSubgroup : Set (L ≃ₐ[K] L)) ⊆ s

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
x✝ : ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
E : IntermediateField K L
left✝ : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ ↑(IntermediateField.normalClosure K (↥E) L).fixingSubgroup ⊆ s

Tactic:
exact le_trans (E.fixingSubgroup_anti E.le_normalClosure) hE

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
⊢ (∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s) ↔
    ∃ E, FiniteDimensional K ↥E ∧ Normal K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
refine ⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
x✝ : ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
E : IntermediateField K L
left✝ : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ ∃ E, FiniteDimensional K ↥E ∧ Normal K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
x✝ : ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
E : IntermediateField K L
left✝ : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ FiniteDimensional K ↥(IntermediateField.normalClosure K (↥E) L) ∧
    Normal K ↥(IntermediateField.normalClosure K (↥E) L) ∧
      ↑(IntermediateField.normalClosure K (↥E) L).fixingSubgroup ⊆ s

Tactic:
simp only [normalClosure.is_finiteDimensional K E L, normalClosure.normal K E L, true_and]

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
x✝ : ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
E : IntermediateField K L
left✝ : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ ↑(IntermediateField.normalClosure K (↥E) L).fixingSubgroup ⊆ s

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
⊢ s ∈ 𝓝 1 ↔ ∃ E, FiniteDimensional K ↥E ∧ Normal K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
rw [krullTopology_mem_nhds_one_iff]

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
⊢ (∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s) ↔
    ∃ E, FiniteDimensional K ↥E ∧ Normal K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
x✝ : ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
E : IntermediateField K L
left✝ : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ ∃ E, FiniteDimensional K ↥E ∧ Normal K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
use (IntermediateField.normalClosure K E L)

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set (L ≃ₐ[K] L)
x✝ : ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
E : IntermediateField K L
left✝ : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ FiniteDimensional K ↥(IntermediateField.normalClosure K (↥E) L) ∧
    Normal K ↥(IntermediateField.normalClosure K (↥E) L) ∧
      ↑(IntermediateField.normalClosure K (↥E) L).fixingSubgroup ⊆ s