-- Mathlib/FieldTheory/Galois/Profinite.lean
theorem restrictNormalHom_continuous (L : IntermediateField k K) [Normal k L] :
    Continuous (AlgEquiv.restrictNormalHom (F := k) (K₁ := K) L)

Proof state:
case intro.intro
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
⊢ ∃ t ⊆ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N, IsOpen t ∧ 1 ∈ t

Tactic:
use (IntermediateField.lift L').fixingSubgroup

Result:
case h
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
⊢ ↑(IntermediateField.lift L').fixingSubgroup ⊆ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∧
    IsOpen ↑(IntermediateField.lift L').fixingSubgroup ∧ 1 ∈ ↑(IntermediateField.lift L').fixingSubgroup

Proof state:
case h.left.a
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
x : K ≃ₐ[k] K
hx : ∀ x_1 ∈ IntermediateField.lift L', x x_1 = x_1
y : ↥L
hy : y ∈ L'
this : ↑((x.restrictNormal ↥L) y) = x ↑y
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

Tactic:
rw [hx y.1 ((IntermediateField.mem_lift y).mpr hy)] at this

Result:
case h.left.a
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
x : K ≃ₐ[k] K
hx : ∀ x_1 ∈ IntermediateField.lift L', x x_1 = x_1
y : ↥L
hy : y ∈ L'
this : ↑((x.restrictNormal ↥L) y) = ↑y
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

Proof state:
case intro.intro
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1

Tactic:
apply mem_nhds_iff.mpr

Result:
case intro.intro
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
⊢ ∃ t ⊆ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N, IsOpen t ∧ 1 ∈ t

Proof state:
case h.left.a
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
x : K ≃ₐ[k] K
hx : ∀ x_1 ∈ IntermediateField.lift L', x x_1 = x_1
⊢ ∀ x_1 ∈ L', ((AlgEquiv.restrictNormalHom ↥L) x) x_1 = x_1

Tactic:
intro y hy

Result:
case h.left.a
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
x : K ≃ₐ[k] K
hx : ∀ x_1 ∈ IntermediateField.lift L', x x_1 = x_1
y : ↥L
hy : y ∈ L'
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
⊢ ∀ A ∈ nhds ((AlgEquiv.restrictNormalHom ↥L) 1), ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' A ∈ nhds 1

Tactic:
intro N hN

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
hN : N ∈ nhds ((AlgEquiv.restrictNormalHom ↥L) 1)
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1

Proof state:
case h.left
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
⊢ ↑(IntermediateField.lift L').fixingSubgroup ⊆ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N

Tactic:
intro x hx

Result:
case h.left
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
x : K ≃ₐ[k] K
hx : x ∈ ↑(IntermediateField.lift L').fixingSubgroup
⊢ x ∈ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N

Proof state:
case h.left.a
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
x : K ≃ₐ[k] K
hx : ∀ x_1 ∈ IntermediateField.lift L', x x_1 = x_1
y : ↥L
hy : y ∈ L'
this : ↑((x.restrictNormal ↥L) y) = ↑y
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

Tactic:
exact SetLike.coe_eq_coe.mp this

Result:
no goals

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
hN : ∃ E, FiniteDimensional k ↥E ∧ ↑E.fixingSubgroup ⊆ N
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1

Tactic:
obtain ⟨L', _, hO⟩ := hN

Result:
case intro.intro
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1