-- 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
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)
L : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_3, u_4} k ↥L
isGalois : IsGalois.{u_3, u_4} k ↥L
x :
  ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K }.toIntermediateField
L' : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_3, u_4} k ↥L'
isGalois_1 : IsGalois.{u_3, u_4} k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional, isGalois := isGalois :
      FiniteGaloisIntermediateField k K } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
this_1 : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower.{u_3, u_4, u_4} k ↥L ↥L' := ⋯
mk :
  Eq (α := K)
    ((algebraMap (↥L') K : (a : ↥L') → K)
        ((algebraMap ↥L ↥L' : (a : ↥L) → ↥L')
            ((AlgEquiv.restrictNormal (K₁ :=
                  ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                        FiniteGaloisIntermediateField k K }.toIntermediateField)
                  (K₂ :=
                  ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                        FiniteGaloisIntermediateField k K }.toIntermediateField)
                  ((proj
                        { toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                          FiniteGaloisIntermediateField k K } :
                      (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                        Gal(↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                                isGalois := isGalois_1 }.toIntermediateField/k))
                    g)
                  ↥L :
                (a : ↥L) → ↥L)
              x) :
          ↥L') :
      K)
    ((↑((((proj
                      { toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                        FiniteGaloisIntermediateField k K } :
                    (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                      Gal(↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                              isGalois := isGalois_1 }.toIntermediateField/k))
                  g :
                Gal(↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                        FiniteGaloisIntermediateField k K }.toIntermediateField/k)) :
              (a :
                  ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                        isGalois := isGalois_1 }.toIntermediateField) →
                ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                      isGalois := isGalois_1 }.toIntermediateField)
            (Subtype.mk (p := fun (x : K) ↦
              x ∈
                { toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                    FiniteGaloisIntermediateField k K }.toIntermediateField)
              (↑x : K) ⋯)) :
        K) :
      K)
⊢ Eq.{u_4 + 1} (α := K)
    (↑((((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u_4}) ↦ (↑x1.toGrp : Type u_4) →* (↑x2.toGrp : Type u_4))
                    (CC := fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4)) (X :=
                    Functor.obj (finGaloisGroupFunctor k K)
                      (op
                        { toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                          FiniteGaloisIntermediateField k K }))
                    (CategoryTheory.Functor.map (finGaloisGroupFunctor k K) h.hom.op) :
                  (a :
                      (fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4))
                        ((finGaloisGroupFunctor k K).obj
                          (op
                            { toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                              isGalois := isGalois_1 }))) →
                    (fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4))
                      ((finGaloisGroupFunctor k K).obj
                        (op
                          { toIntermediateField := L, finiteDimensional := finiteDimensional, isGalois := isGalois })))
                ((proj
                        { toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                          FiniteGaloisIntermediateField k K } :
                      (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                        Gal(↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                                isGalois := isGalois_1 }.toIntermediateField/k))
                    g :
                  Gal(↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                          FiniteGaloisIntermediateField k K }.toIntermediateField/k)) :
              (fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4))
                (Functor.obj (finGaloisGroupFunctor k K)
                  (op
                    { toIntermediateField := L, finiteDimensional := finiteDimensional, isGalois := isGalois :
                      FiniteGaloisIntermediateField k K }))) :
            (a :
                ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional,
                      isGalois := isGalois }.toIntermediateField) →
              ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional,
                    isGalois := isGalois }.toIntermediateField)
          x) :
      K)
    (↑((((proj
                    { toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                      FiniteGaloisIntermediateField k K } :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                            isGalois := isGalois_1 }.toIntermediateField/k))
                g :
              Gal(↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                      FiniteGaloisIntermediateField k K }.toIntermediateField/k)) :
            (a :
                ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                      isGalois := isGalois_1 }.toIntermediateField) →
              ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional_1,
                    isGalois := isGalois_1 }.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦
            x ∈
              { toIntermediateField := L', finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
                  FiniteGaloisIntermediateField k K }.toIntermediateField)
            (↑x : K) ⋯)) :
      K)

Tactic:
change (algebraMap L' K (algebraMap L L' (AlgEquiv.restrictNormal (proj (mk L') g) L x))) = _

Premises used: Algebra.algebraMap, Membership.mem, Subtype, InfiniteGalois.proj, AlgEquiv.restrictNormal, DFunLike.coe, FiniteGaloisIntermediateField.mk