awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
f : L₁ ⟶ L₂
g : L₂ ⟶ L₃
op :
  ∀ (L₁ : IntermediateField k K) [finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁]
    [isGalois : IsGalois.{u_1, u_2} k ↥L₁] (L₂ : IntermediateField k K)
    [finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂] [isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂]
    (f :
      Opposite.op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K } ⟶
        Opposite.op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 })
    (L₃ : IntermediateField k K) [finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃]
    [isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃]
    (g :
      Opposite.op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K } ⟶
        Opposite.op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }),
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
iterate 2
    induction L₁ with | _ L₁ => ?_
    induction L₂ with | _ L₂ => ?_
    induction L₃ with | _ L₃ => ?_
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
L₃ : IntermediateField k K
finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃
isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃
g :
  op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }
algInst : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_1 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_2 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
⊢ IsScalarTower.{u_1, u_2, u_2} k ↥L₂ ↥L₁

Tactic:
have : IsScalarTower k L₂ L₁ := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
L₃ : IntermediateField k K
finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃
isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃
g :
  op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }
algInst : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_1 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_2 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this : IsScalarTower.{u_1, u_2, u_2} k ↥L₂ ↥L₁
⊢ IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₁

Tactic:
have : IsScalarTower k L₃ L₁ := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
L₃ : IntermediateField k K
finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃
isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃
g :
  op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }
algInst : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_1 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_2 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this_1 : IsScalarTower.{u_1, u_2, u_2} k ↥L₂ ↥L₁
this : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₁
⊢ IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₂

Tactic:
have : IsScalarTower k L₃ L₂ := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
L₃ : IntermediateField k K
finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃
isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃
g :
  op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }
algInst : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_1 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_2 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this_1 : IsScalarTower.{u_1, u_2, u_2} k ↥L₂ ↥L₁
this_2 : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₁
this : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₂
⊢ IsScalarTower.{u_2, u_2, u_2} ↥L₃ ↥L₂ ↥L₁

Tactic:
have : IsScalarTower L₃ L₂ L₁ := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
f :
  Opposite.op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    Opposite.op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
L₃ : IntermediateField k K
finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃
isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃
g :
  Opposite.op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    Opposite.op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }
algInst : Algebra
  ↥(unop
        (Opposite.op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (Opposite.op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_1 : Algebra
  ↥(unop
        (Opposite.op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (Opposite.op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_2 : Algebra
  ↥(unop
        (Opposite.op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (Opposite.op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this_1 : IsScalarTower.{u_1, u_2, u_2} k ↥L₂ ↥L₁
this_2 : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₁
this_3 : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₂
this : IsScalarTower.{u_2, u_2, u_2} ↥L₃ ↥L₂ ↥L₁
op :
  ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u_2}) ↦ (↑x1.toGrp : Type u_2) →* (↑x2.toGrp : Type u_2)) (CC :=
      fun (X : FiniteGrp.{u_2}) ↦ (↑X.toGrp : Type u_2)) (finGaloisGroupMap (f ≫ g)) =
    ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u_2}) ↦ (↑x1.toGrp : Type u_2) →* (↑x2.toGrp : Type u_2)) (CC :=
      fun (X : FiniteGrp.{u_2}) ↦ (↑X.toGrp : Type u_2)) (finGaloisGroupMap f ≫ finGaloisGroupMap g)
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
ext : 1
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
L₂ : IntermediateField k K
finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂
isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
L₃ : IntermediateField k K
finiteDimensional_2 : FiniteDimensional.{u_1, u_2} k ↥L₃
isGalois_2 : IsGalois.{u_1, u_2} k ↥L₃
g :
  op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 }
algInst : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_1 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst_2 : Algebra
  ↥(unop
        (op
          { toIntermediateField := L₃, finiteDimensional := finiteDimensional_2, isGalois := isGalois_2 :
            FiniteGaloisIntermediateField k K })).toSubsemiring
  ↥(unop
        (op
          { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
            FiniteGaloisIntermediateField k K })).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this_1 : IsScalarTower.{u_1, u_2, u_2} k ↥L₂ ↥L₁
this_2 : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₁
this_3 : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₂
this : IsScalarTower.{u_2, u_2, u_2} ↥L₃ ↥L₂ ↥L₁
⊢ ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u_2}) ↦ (↑x1.toGrp : Type u_2) →* (↑x2.toGrp : Type u_2)) (CC :=
      fun (X : FiniteGrp.{u_2}) ↦ (↑X.toGrp : Type u_2)) (finGaloisGroupMap (f ≫ g)) =
    ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u_2}) ↦ (↑x1.toGrp : Type u_2) →* (↑x2.toGrp : Type u_2)) (CC :=
      fun (X : FiniteGrp.{u_2}) ↦ (↑X.toGrp : Type u_2)) (finGaloisGroupMap f ≫ finGaloisGroupMap g)

Tactic:
apply IsScalarTower.AlgEquiv.restrictNormalHom_comp k L₃ L₂ L₁

Premises used: Membership.mem, IsScalarTower.AlgEquiv.restrictNormalHom_comp, Subtype
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
σ : Gal(K/k)
L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ
π : L₁ ⟶ L₂
algInst : Algebra ↥(unop L₂).toSubsemiring ↥(unop L₁).toSubsemiring := (Subsemiring.inclusion ⋯).toAlgebra
⊢ IsScalarTower.{u_3, u_4, u_4} k ↥(unop L₂).toIntermediateField ↥(unop L₁).toIntermediateField

Tactic:
have : IsScalarTower k L₂.unop L₁.unop := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
σ : Gal(K/k)
L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ
π : L₁ ⟶ L₂
algInst : Algebra ↥(unop L₂).toSubsemiring ↥(unop L₁).toSubsemiring := (Subsemiring.inclusion ⋯).toAlgebra
this : IsScalarTower.{u_3, u_4, u_4} k ↥(unop L₂).toIntermediateField ↥(unop L₁).toIntermediateField
⊢ IsScalarTower (↥(unop L₂).toIntermediateField) (↥(unop L₁).toIntermediateField) K

Tactic:
have : IsScalarTower L₂.unop L₁.unop K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
σ : Gal(K/k)
L₁ L₂ : (FiniteGaloisIntermediateField k K)ᵒᵖ
π : L₁ ⟶ L₂
algInst : Algebra ↥(unop L₂).toSubsemiring ↥(unop L₁).toSubsemiring := (Subsemiring.inclusion ⋯).toAlgebra
this_1 : IsScalarTower.{u_3, u_4, u_4} k ↥(unop L₂).toIntermediateField ↥(unop L₁).toIntermediateField
this : IsScalarTower (↥(unop L₂).toIntermediateField) (↥(unop L₁).toIntermediateField) K
⊢ Eq (α :=
    (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L₂).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
    ((Hom.hom (CategoryTheory.Functor.map (asProfiniteGaloisGroupFunctor k K) π) :
          (a : (↑((asProfiniteGaloisGroupFunctor k K).obj L₁).toProfinite.toTop : Type u_4)) →
            (↑((asProfiniteGaloisGroupFunctor k K).obj L₂).toProfinite.toTop : Type u_4))
        ((fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
            ((AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
                  (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
                σ :
              Gal(↥(unop L).toIntermediateField/k)))
          L₁) :
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L₂).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
    ((fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
          ((AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
                (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
              σ :
            Gal(↥(unop L).toIntermediateField/k)))
        L₂ :
      Gal(↥(unop L₂).toIntermediateField/k))

Tactic:
apply (IsScalarTower.AlgEquiv.restrictNormalHom_comp_apply L₂.unop L₁.unop σ).symm

Premises used: Membership.mem, Subtype, FiniteGaloisIntermediateField.toIntermediateField, IsScalarTower.AlgEquiv.restrictNormalHom_comp_apply, Eq.symm, Opposite.unop
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
simp :
  Eq.{u_4 + 1} (α := ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
    (Subtype.mk (p :=
      fun
        (x :
          (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
            (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                  TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
              Type u_4)) ↦
      Membership.mem (γ :=
        Subgroup
          ((j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
            (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                  TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
              Type u_4)))
        (limitConePtAux (asProfiniteGaloisGroupFunctor k K)) x)
      (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦ 1) ⋯)
    1
⊢ Eq.{u_4 + 1} (α :=
    (↑((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))
    (Subtype.mk (p :=
      fun
        (x :
          (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
            (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                  TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
              Type u_4)) ↦
      Membership.mem (γ :=
        Subgroup
          ((j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
            (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                  TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
              Type u_4)))
        (limitConePtAux (asProfiniteGaloisGroupFunctor k K)) x)
      (fun (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) ↦
        (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField :
            (a : Gal(K/k)) → Gal(↥(unop L).toIntermediateField/k))
          1)
      ⋯)
    1

Tactic:
simp only [map_one]

Premises used: map_one