-- 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
g :
  (↑((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)
x : K
L : FiniteGaloisIntermediateField k K
hx' : toAlgEquivAux g x ∈ L.toIntermediateField
hx : x ∈ L.toIntermediateField
rw :
  (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) (toAlgEquivAux g x) hx') : K) =
    (↑((((proj L :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L.toIntermediateField/k))
                g :
              Gal(↥L.toIntermediateField/k)) :
            (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
      K)
rw₁ :
  toAlgEquivAux g x =
    (↑((((proj L :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L.toIntermediateField/k))
                g :
              Gal(↥L.toIntermediateField/k)) :
            (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
      K)
rw₂ :
  Eq.{u_4 + 1} (α := K)
    (↑((((proj L :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L.toIntermediateField/k))
                g :
              Gal(↥L.toIntermediateField/k)) :
            (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
      K)
    (↑((((proj L :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L.toIntermediateField/k))
                g :
              Gal(↥L.toIntermediateField/k)) :
            (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
      K)
L₁ : FiniteGaloisIntermediateField k K
hx₁ : x ∈ L.toIntermediateField
rw₃ :
  Eq.{u_4 + 1} (α := K)
    (↑((((proj L :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L.toIntermediateField/k))
                g :
              Gal(↥L.toIntermediateField/k)) :
            (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
      K)
    (↑((((proj L :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L.toIntermediateField/k))
                g :
              Gal(↥L.toIntermediateField/k)) :
            (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
      K)
L₂ : FiniteGaloisIntermediateField k K
hx₂ : x ∈ L.toIntermediateField
⊢ Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) (toAlgEquivAux g x) hx' =
    (((proj L :
              (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                Gal(↥L.toIntermediateField/k))
            g :
          Gal(↥L.toIntermediateField/k)) :
        (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
      (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)

Tactic:
rw [Subtype.ext_iff, Subtype.coe_mk, toAlgEquivAux_eq_proj_of_mem]

Premises used: Subtype.coe_mk, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, Subtype.ext_iff