-- 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:
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
⊢ Continuous ⇑(AlgEquiv.restrictNormalHom ↥L)

Tactic:
apply continuous_of_continuousAt_one _ (continuousAt_def.mpr _ )

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
⊢ ∀ A ∈ nhds ((AlgEquiv.restrictNormalHom ↥L) 1), ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' A ∈ nhds 1

Proof state:
case h.right
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
⊢ IsOpen ↑(IntermediateField.lift L').fixingSubgroup ∧ 1 ∈ ↑(IntermediateField.lift L').fixingSubgroup

Tactic:
exact ⟨IntermediateField.fixingSubgroup_isOpen (IntermediateField.lift L') , congrFun rfl⟩

Result:
no goals

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 : (algebraMap (↥L) K) ((x.restrictNormal ↥L) y) = x ((algebraMap (↥L) K) y)
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

Tactic:
dsimp 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) = x ↑y
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

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'
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

Tactic:
have := AlgEquiv.restrictNormal_commutes x L y

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 : (algebraMap (↥L) K) ((x.restrictNormal ↥L) y) = x ((algebraMap (↥L) K) 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
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1

Tactic:
let _ : FiniteDimensional k L' :=
  Module.Finite.equiv <| AlgEquiv.toLinearEquiv <| IntermediateField.liftAlgEquiv L'

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
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1

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 ∈ ↑(IntermediateField.lift L').fixingSubgroup
⊢ (AlgEquiv.restrictNormalHom ↥L) x ∈ ↑L'.fixingSubgroup

Tactic:
simp only [SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff] at hx ⊢

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
⊢ ∀ x_1 ∈ L', ((AlgEquiv.restrictNormalHom ↥L) x) x_1 = x_1

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 : N ∈ nhds ((AlgEquiv.restrictNormalHom ↥L) 1)
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1

Tactic:
rw [map_one, krullTopology_mem_nhds_one_iff] at 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 : ∃ E, FiniteDimensional k ↥E ∧ ↑E.fixingSubgroup ⊆ N
⊢ ⇑(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
x : K ≃ₐ[k] K
hx : x ∈ ↑(IntermediateField.lift L').fixingSubgroup
⊢ x ∈ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N

Tactic:
apply hO

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 ∈ ↑(IntermediateField.lift L').fixingSubgroup
⊢ (AlgEquiv.restrictNormalHom ↥L) x ∈ ↑L'.fixingSubgroup