-- Mathlib/FieldTheory/Galois/Profinite.lean
lemma mulEquivToLimit_symm_continuous [IsGalois k K] : Continuous (mulEquivToLimit k K).symm

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
⊢ ∀ A ∈ nhds ((mulEquivToLimit k K).symm 1), ⇑(mulEquivToLimit k K).symm ⁻¹' A ∈ nhds 1

Tactic:
simp only [map_one, krullTopology_mem_nhds_one_iff_of_isGalois, ← MulEquiv.coe_toEquiv_symm,
  ← MulEquiv.toEquiv_eq_coe, ← (mulEquivToLimit k K).image_eq_preimage]

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
⊢ ∀ (A : Set (K ≃ₐ[k] K)), (∃ L, ↑L.fixingSubgroup ⊆ A) → (fun a => (mulEquivToLimit k K).toEquiv a) '' A ∈ nhds 1

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
⊢ Continuous ⇑(mulEquivToLimit k K).symm

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
inst✝ : IsGalois k K
⊢ ∀ A ∈ nhds ((mulEquivToLimit k K).symm 1), ⇑(mulEquivToLimit k K).symm ⁻¹' A ∈ nhds 1

Proof state:
case h
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set (K ≃ₐ[k] K)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup ⊆ (fun a => (mulEquivToLimit k K).toEquiv a) '' H ∧
    IsOpen (⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup) ∧ 1 ∈ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup

Tactic:
simp only [isOpen_mulEquivToLimit_image_fixingSubgroup L]

Result:
case h
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set (K ≃ₐ[k] K)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ (fun a => (mulEquivToLimit k K) a) '' ↑L.fixingSubgroup ⊆ (fun a => (mulEquivToLimit k K).toEquiv a) '' H ∧
    True ∧ 1 ∈ (fun a => (mulEquivToLimit k K) a) '' ↑L.fixingSubgroup

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set (K ≃ₐ[k] K)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ ∃ t ⊆ (fun a => (mulEquivToLimit k K).toEquiv a) '' H, IsOpen t ∧ 1 ∈ t

Tactic:
use mulEquivToLimit k K '' L.1.fixingSubgroup

Result:
case h
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set (K ≃ₐ[k] K)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup ⊆ (fun a => (mulEquivToLimit k K).toEquiv a) '' H ∧
    IsOpen (⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup) ∧ 1 ∈ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup

Proof state:
case h
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set (K ≃ₐ[k] K)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ (fun a => (mulEquivToLimit k K) a) '' ↑L.fixingSubgroup ⊆ (fun a => (mulEquivToLimit k K).toEquiv a) '' H ∧
    True ∧ 1 ∈ (fun a => (mulEquivToLimit k K) a) '' ↑L.fixingSubgroup

Tactic:
simpa [one_mem] using Set.image_subset_iff.mp (Set.image_mono le)

Result:
no goals

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set (K ≃ₐ[k] K)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ (fun a => (mulEquivToLimit k K).toEquiv a) '' H ∈ nhds 1

Tactic:
rw [mem_nhds_iff]

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set (K ≃ₐ[k] K)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ ∃ t ⊆ (fun a => (mulEquivToLimit k K).toEquiv a) '' H, IsOpen t ∧ 1 ∈ t

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
⊢ ∀ (A : Set (K ≃ₐ[k] K)), (∃ L, ↑L.fixingSubgroup ⊆ A) → (fun a => (mulEquivToLimit k K).toEquiv a) '' A ∈ nhds 1

Tactic:
intro H ⟨L, le⟩

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set (K ≃ₐ[k] K)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ (fun a => (mulEquivToLimit k K).toEquiv a) '' H ∈ nhds 1