-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
    (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4)) :=
  {f :
    (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4) |
    Eq.{u_4 + 1} (α :=
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) (op L)).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
      (f (op L)) 1}
this :
  Eq (α :=
    Set
      (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
            (P := fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
    ((⇑(mulEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
      (↑L.fixingSubgroup : Set Gal(K/k)))
    (Subtype.val (p :=
        fun
          (x :
            (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)) ↦
        Membership.mem (γ :=
          Subgroup
            ((j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)))
          (limitConePtAux (asProfiniteGaloisGroupFunctor k K)) x) ⁻¹'
      fix1)
⊢ IsOpen (X :=
    (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
          fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
    (Subtype.val (p :=
        fun
          (x :
            (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)) ↦
        Membership.mem (γ :=
          Subgroup
            ((j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
              (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                    TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
                Type u_4)))
          (limitConePtAux (asProfiniteGaloisGroupFunctor k K)) x) ⁻¹'
      fix1)

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

Premises used: trivial, isOpen_induced, Opposite.op, continuous_apply, Singleton.singleton, OfNat.ofNat, Continuous.isOpen_preimage