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

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

Result:
case h.h.h.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₂ L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
L₁ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₁
isGalois✝ : IsGalois k ↥L₁
f : op (FiniteGaloisIntermediateField.mk L₁) ⟶ op L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Proof state:
case h.h.h.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₂ L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
L₁ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₁
isGalois✝ : IsGalois k ↥L₁
f : op (FiniteGaloisIntermediateField.mk L₁) ⟶ op L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

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

Result:
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

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₁
this✝ : IsScalarTower k ↥L₃ ↥L₁
this : IsScalarTower k ↥L₃ ↥L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
have : IsScalarTower L₃ 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₁
this✝ : IsScalarTower k ↥L₃ ↥L₂
this : IsScalarTower ↥L₃ ↥L₂ ↥L₁
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Proof state:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
f : L₁ ⟶ L₂
g : L₂ ⟶ L₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
iterate 2
  induction L₁ with | _ L₁ => ?_
  induction L₂ with | _ L₂ => ?_
  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

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₃)
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
algebraize [Subsemiring.inclusion g.unop.le, Subsemiring.inclusion f.unop.le,
  Subsemiring.inclusion (g.unop.le.trans f.unop.le)]

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
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g