-- Mathlib/FieldTheory/Galois/Profinite.lean
@[simp]
lemma map_comp {L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (f : L₁ ⟶ L₂) (g : L₂ ⟶ L₃) :
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Proof state:
case h.h.h.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 (FiniteGaloisIntermediateField.mk L₁) ⟶ op (FiniteGaloisIntermediateField.mk L₂)
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g : op (FiniteGaloisIntermediateField.mk L₂) ⟶ op (FiniteGaloisIntermediateField.mk L₃)
algInst✝² : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝¹ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

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

Result:
case h.h.h.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 (FiniteGaloisIntermediateField.mk L₁) ⟶ op (FiniteGaloisIntermediateField.mk L₂)
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g : op (FiniteGaloisIntermediateField.mk L₂) ⟶ op (FiniteGaloisIntermediateField.mk L₃)
algInst✝² : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝¹ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this : IsScalarTower k ↥L₂ ↥L₁
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Proof state:
case h.h.h.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 (FiniteGaloisIntermediateField.mk L₁) ⟶ op (FiniteGaloisIntermediateField.mk L₂)
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g : op (FiniteGaloisIntermediateField.mk L₂) ⟶ op (FiniteGaloisIntermediateField.mk L₃)
algInst✝² : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝¹ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this : IsScalarTower k ↥L₂ ↥L₁
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

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

Result:
case h.h.h.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 (FiniteGaloisIntermediateField.mk L₁) ⟶ op (FiniteGaloisIntermediateField.mk L₂)
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g : op (FiniteGaloisIntermediateField.mk L₂) ⟶ op (FiniteGaloisIntermediateField.mk L₃)
algInst✝² : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝¹ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this✝ : IsScalarTower k ↥L₂ ↥L₁
this : IsScalarTower k ↥L₃ ↥L₁
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Proof state:
case h.h.h.mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₃ : FiniteGaloisIntermediateField 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₂
g : op (FiniteGaloisIntermediateField.mk L₂) ⟶ op L₃
f : op (FiniteGaloisIntermediateField.mk L₁) ⟶ op (FiniteGaloisIntermediateField.mk L₂)
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₃ with | _ L₃ => ?_

Result:
case h.h.h.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 (FiniteGaloisIntermediateField.mk L₁) ⟶ op (FiniteGaloisIntermediateField.mk L₂)
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g : op (FiniteGaloisIntermediateField.mk L₂) ⟶ op (FiniteGaloisIntermediateField.mk L₃)
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g