Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case op.op.op.mk.mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ : IntermediateField k K
finiteDimensional✝² : FiniteDimensional k ↥L₁
isGalois✝² : IsGalois k ↥L₁
L₂ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L₂
isGalois✝¹ : IsGalois k ↥L₂
f :
  op { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝², isGalois := isGalois✝² } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g :
  op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
algInst✝² : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹,
            isGalois := isGalois✝¹ })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝¹ : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹,
            isGalois := isGalois✝¹ })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝²,
            isGalois := isGalois✝² })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝ : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝²,
            isGalois := isGalois✝² })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this✝ : IsScalarTower k ↥L₂ ↥L₁
this : IsScalarTower k ↥L₃ ↥L₁
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
have : IsScalarTower k L₃ L₂ := IsScalarTower.of_algebraMap_eq' rfl

Goal state after:
case op.op.op.mk.mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ : IntermediateField k K
finiteDimensional✝² : FiniteDimensional k ↥L₁
isGalois✝² : IsGalois k ↥L₁
L₂ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L₂
isGalois✝¹ : IsGalois k ↥L₂
f :
  op { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝², isGalois := isGalois✝² } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g :
  op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
algInst✝² : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹,
            isGalois := isGalois✝¹ })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝¹ : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹,
            isGalois := isGalois✝¹ })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝²,
            isGalois := isGalois✝² })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝ : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝²,
            isGalois := isGalois✝² })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower k ↥L₂ ↥L₁
this✝ : IsScalarTower k ↥L₃ ↥L₁
this : IsScalarTower k ↥L₃ ↥L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g