awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
⊢ Eq.{u_4 + 1} (α := ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
    (Subtype.mk (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)
      (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦ 1) ⋯)
    1

Tactic:
rfl
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
apply :
  ∀ (A : Set Gal(↥L/k)),
    Membership.mem (γ := Filter Gal(↥L/k))
        (nhds ((AlgEquiv.restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) 1) : Filter Gal(↥L/k)) A →
      Membership.mem (γ := Filter Gal(K/k)) (nhds 1)
        ((⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' A)
⊢ Continuous.{u_4, u_4} (X := Gal(K/k)) (Y := Gal(↥L/k)) (⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k))

Tactic:
apply continuous_of_continuousAt_one _ (continuousAt_def.mpr _)

Premises used: Iff.mpr, continuous_of_continuousAt_one, continuousAt_def
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
hN :
  Membership.mem (γ := Filter Gal(↥L/k))
    (nhds ((AlgEquiv.restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) 1) : Filter Gal(↥L/k)) N
⊢ ∃ (E : IntermediateField k ↥L), FiniteDimensional.{u_3, u_4} k ↥E ∧ (↑E.fixingSubgroup : Set Gal(↥L/k)) ⊆ N

Tactic:
rw [map_one, krullTopology_mem_nhds_one_iff] at hN

Premises used: map_one, krullTopology_mem_nhds_one_iff
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
hN : ∃ (E : IntermediateField k ↥L), FiniteDimensional.{u_3, u_4} k ↥E ∧ (↑E.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
obtain :
  ∀ (L' : IntermediateField k ↥L),
    FiniteDimensional.{u_3, u_4} k ↥L' →
      ∀ (hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N),
        Membership.mem (γ := Filter Gal(K/k)) (nhds 1)
          ((⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N)
⊢ Membership.mem (γ := Filter Gal(K/k)) (nhds 1) ((⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N)

Tactic:
obtain ⟨L', _, hO⟩ := hN
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
⊢ Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')

Tactic:
have := Module.Finite.equiv <| AlgEquiv.toLinearEquiv <| IntermediateField.liftAlgEquiv L'
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
apply : ∃ t ⊆ (⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N, IsOpen t ∧ 1 ∈ t
⊢ Membership.mem (γ := Filter Gal(K/k)) (nhds 1) ((⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N)

Tactic:
apply mem_nhds_iff.mpr

Premises used: Iff.mpr, mem_nhds_iff
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
h :
  (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k)) ⊆
      (⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N ∧
    IsOpen (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k)) ∧
      1 ∈ (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k))
⊢ ∃ t ⊆ (⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N, IsOpen t ∧ 1 ∈ t

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

Premises used: IntermediateField.lift, IntermediateField.fixingSubgroup
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
h :
  (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k)) ⊆
    (⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N
h₁ :
  IsOpen (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k)) ∧
    1 ∈ (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k))
⊢ (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k)) ⊆
      (⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N ∧
    IsOpen (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k)) ∧
      1 ∈ (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k))

Tactic:
constructor
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : x ∈ (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k))
h :
  Membership.mem (α := Gal(↥L/k)) (↑L'.fixingSubgroup : Set Gal(↥L/k))
    ((AlgEquiv.restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) x : Gal(↥L/k))
⊢ Membership.mem (γ := Set Gal(K/k)) ((⇑(AlgEquiv.restrictNormalHom ↥L) : (a : Gal(K/k)) → Gal(↥L/k)) ⁻¹' N) x

Tactic:
apply hO
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : x ∈ (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k))
h :
  ∀ (hx : ∀ x_1 ∈ IntermediateField.lift L', (x : (a : K) → K) x_1 = x_1),
    ∀ x_1 ∈ L', (((AlgEquiv.restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) x : Gal(↥L/k)) : (a : ↥L) → ↥L) x_1 = x_1
⊢ Membership.mem (α := Gal(↥L/k)) (↑L'.fixingSubgroup : Set Gal(↥L/k))
    ((AlgEquiv.restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) x : Gal(↥L/k))

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

Premises used: SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : ∀ x_1 ∈ IntermediateField.lift L', (x : (a : K) → K) x_1 = x_1
y : ↥L
hy : y ∈ L'
⊢ Eq (α := K) ((algebraMap (↥L) K : (a : ↥L) → K) ((x.restrictNormal ↥L : (a : ↥L) → ↥L) y : ↥L) : K)
    ((x : (a : K) → K) ((algebraMap (↥L) K : (a : ↥L) → K) y : K) : K)

Tactic:
have := AlgEquiv.restrictNormal_commutes x L y
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this_1 : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : ∀ x_1 ∈ IntermediateField.lift L', (x : (a : K) → K) x_1 = x_1
y : ↥L
hy : y ∈ L'
this : Eq (α := K) ((↑((x.restrictNormal ↥L : (a : ↥L) → ↥L) y) : K) : K) ((x : (a : K) → K) (↑y : K) : K)
⊢ (↑((x.restrictNormal ↥L : (a : ↥L) → ↥L) y) : K) = (↑y : K)

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

Premises used: Iff.mpr, IntermediateField.mem_lift, Subtype.val
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this_1 : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : ∀ x_1 ∈ IntermediateField.lift L', (x : (a : K) → K) x_1 = x_1
y : ↥L
hy : y ∈ L'
this : (↑((x.restrictNormal ↥L : (a : ↥L) → ↥L) y) : K) = (↑y : K)
⊢ (((AlgEquiv.restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) x : Gal(↥L/k)) : (a : ↥L) → ↥L) y = y

Tactic:
SetLike.coe_eq_coe.mp this

Premises used: SetLike.coe_eq_coe, Iff.mp
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this_1 : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : ∀ x_1 ∈ IntermediateField.lift L', (x : (a : K) → K) x_1 = x_1
y : ↥L
hy : y ∈ L'
this : (↑((x.restrictNormal ↥L : (a : ↥L) → ↥L) y) : K) = (↑y : K)
⊢ (((AlgEquiv.restrictNormalHom ↥L : (a : Gal(K/k)) → Gal(↥L/k)) x : Gal(↥L/k)) : (a : ↥L) → ↥L) y = y

Tactic:
exact SetLike.coe_eq_coe.mp this

Premises used: SetLike.coe_eq_coe, Iff.mp
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
⊢ IsOpen (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k)) ∧
    1 ∈ (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k))

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

Premises used: IntermediateField.lift, congrFun, And.intro, IntermediateField.fixingSubgroup_isOpen, rfl
-- 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
L : IntermediateField k K
inst_3 : Normal.{u_3, u_4} k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left : FiniteDimensional.{u_3, u_4} k ↥L'
hO : (↑L'.fixingSubgroup : Set Gal(↥L/k)) ⊆ N
this : Module.Finite.{u_3, u_4} k ↥(IntermediateField.lift L')
⊢ IsOpen (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k)) ∧
    1 ∈ (↑(IntermediateField.lift L').fixingSubgroup : Set Gal(K/k))

Tactic:
exact ⟨IntermediateField.fixingSubgroup_isOpen (IntermediateField.lift L'), congrFun rfl⟩
-- 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
rw :
  Continuous (X := Gal(K/k)) (Y :=
    (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))
    (Function.comp (β :=
      (↑((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))
      (⇑(algEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)))
⊢ Continuous (X := Gal(K/k)) (Y :=
    (↑((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))
    (⇑(algEquivToLimit k K) :
      (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))

Tactic:
rw [continuous_induced_rng]

Premises used: continuous_induced_rng
-- 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
⊢ Continuous (X := Gal(K/k)) (Y :=
    (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))
    (Function.comp (β :=
      (↑((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))
      (⇑(algEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)))

Tactic:
continuous_pi (fun L ↦ ?_)

Premises used: continuous_pi
-- 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
refine :
  ∀ (L : (FiniteGaloisIntermediateField k K)ᵒᵖ),
    Continuous (Y :=
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
      fun (a : Gal(K/k)) ↦
      Function.comp (β :=
        (↑((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))
        (⇑(algEquivToLimit k K) :
          (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))
        a L
⊢ Continuous (X := Gal(K/k)) (Y :=
    (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))
    (Function.comp (β :=
      (↑((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))
      (⇑(algEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)))

Tactic:
refine continuous_pi (fun L ↦ ?_)

Premises used: continuous_pi
-- 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
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
⊢ Continuous.{u_4, u_4} (X := Gal(K/k)) (Y := Gal(↥(unop L).toIntermediateField/k))
    (⇑(AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField) :
      (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))

Tactic:
restrictNormalHom_continuous L.unop.1

Premises used: InfiniteGalois.restrictNormalHom_continuous, FiniteGaloisIntermediateField.toIntermediateField, Opposite.unop
-- 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
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
h :
  (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4) =
      Gal(↥(unop L).toIntermediateField/k) →
    Eq.{u_4 + 1} (α :=
      TopologicalSpace
        (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
              TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
          Type u_4))
      (Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4)).str
      (krullTopology k ↥(unop L).toIntermediateField)
⊢ Continuous (Y :=
    (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
    fun (a : Gal(K/k)) ↦
    Function.comp (β :=
      (↑((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))
      (⇑(algEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))
      a L

Tactic:
convert! restrictNormalHom_continuous L.unop.1

Premises used: InfiniteGalois.restrictNormalHom_continuous, FiniteGaloisIntermediateField.toIntermediateField, Opposite.unop
-- 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
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
e_2 :
  (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4) =
    Gal(↥(unop L).toIntermediateField/k)
⊢ Eq.{u_4 + 1} (α :=
    TopologicalSpace
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
    (Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
        TotallyDisconnectedSpace.{u_4} (↑X : Type u_4)).str
    (krullTopology k ↥(unop L).toIntermediateField)

Tactic:
(DiscreteTopology.eq_bot (α := L.unop ≃ₐ[k] L.unop)).symm

Premises used: DiscreteTopology.eq_bot, Eq.symm
-- 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
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
e_2 :
  (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4) =
    Gal(↥(unop L).toIntermediateField/k)
⊢ Eq.{u_4 + 1} (α :=
    TopologicalSpace
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
    (Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
        TotallyDisconnectedSpace.{u_4} (↑X : Type u_4)).str
    (krullTopology k ↥(unop L).toIntermediateField)

Tactic:
exact (DiscreteTopology.eq_bot (α := L.unop ≃ₐ[k] L.unop)).symm

Premises used: DiscreteTopology.eq_bot, Eq.symm