-- Mathlib/FieldTheory/Galois/Profinite.lean
lemma isOpen_mulEquivToLimit_image_fixingSubgroup [IsGalois k K]
    (L : FiniteGaloisIntermediateField k K) : IsOpen (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
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
x : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
⊢ x ∈ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup ↔ x ∈ Subtype.val ⁻¹' fix1

Tactic:
obtain ⟨σ, rfl⟩ := (mulEquivToLimit k K).surjective x

Result:
case h.intro
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
σ : K ≃ₐ[k] K
⊢ (mulEquivToLimit k K) σ ∈ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup ↔ (mulEquivToLimit k K) σ ∈ Subtype.val ⁻¹' fix1

Proof state:
case h.intro
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
σ : K ≃ₐ[k] K
⊢ (mulEquivToLimit k K) σ ∈ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup ↔ (mulEquivToLimit k K) σ ∈ Subtype.val ⁻¹' fix1

Tactic:
simpa using FiniteGaloisIntermediateField.mem_fixingSubgroup_iff _ _

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
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
⊢ IsOpen (⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup)

Tactic:
suffices mulEquivToLimit k K '' L.1.fixingSubgroup = Set.preimage Subtype.val fix1 by
  rw [this]
  exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial)

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
⊢ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
this : ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1
⊢ IsOpen (Subtype.val ⁻¹' fix1)

Tactic:
exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial)

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
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
this : ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1
⊢ IsOpen (⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup)

Tactic:
rw [this]

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
this : ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1
⊢ IsOpen (Subtype.val ⁻¹' fix1)

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
⊢ IsOpen (⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup)

Tactic:
let fix1 : Set (Π L, (asProfiniteGaloisGroupFunctor k K).obj L) := {f | f (op L) = 1}

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
⊢ IsOpen (⇑(mulEquivToLimit k K) '' ↑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
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
⊢ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1

Tactic:
ext x

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
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
x : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
⊢ x ∈ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup ↔ x ∈ Subtype.val ⁻¹' fix1