awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.NormalBasis (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Infinite K
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have Choose : ∀ (e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L),
  ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: classical
  /- Choose a basis `e` of `L` over `K` and form the matrix `M` with entries
    `∑ₖ i⁻¹j(eₖ)Xₖ` where `i,j ∈ Gal(L/K)` and `Xₖ`s are independent variables. -/
  have e := Module.Free.chooseBasis K L
  let M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial _ L) :=
    .of fun i j ↦ ∑ k, i.symm (j (e k)) • .X k
  /- By [ConradLinearChar] Lemma 3.4, there exists `{xₖ} ⊆ L` such that `∑ₖ j(eₖ)xₖ = 1`
    if `j = 1` and `∑ₖ j(eₖ)xₖ = 0` otherwise. -/
  have hq : Submodule.span L (Set.range fun k (j : Gal(L/K)) ↦ j (e k)) = ⊤ := by
    apply span_flip_eq_top_iff_linearIndependent.mpr <|
      ((linearIndependent_algHom_toLinearMap K L L).comp _
        (algEquivEquivAlgHom K L).injective).map' _ (e.constr L).symm.ker
  /- If we evaluate `M` at `Xₖ = xₖ`, the determinant of `M` evaluates to 1. -/
  obtain ⟨c, hc⟩ : ∃ c : _ → L, M.det.eval c = 1 := by
    obtain ⟨g, hg⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp
      (hq ▸ Submodule.mem_top (x := Pi.single 1 1))
    simp_rw [RingHom.map_det]
    refine ⟨g, congr(Matrix.det $(?_)).trans Matrix.det_one⟩
    ext i j
    simpa [M, Pi.single_apply, inv_mul_eq_one, mul_comm, Matrix.one_apply]
      using congr($hg (i⁻¹ * j))
  /- Therefore `det M` is nonzero. -/
  have hM : M.det ≠ 0 := fun h0 ↦ by
    simpa [hc] using congr(($h0).eval c)
  /- Since `K` is infinite, we may evaluate `det M` at some point with coordinates in `K`
    and get a nonzero value. The coordinates give rise to an element of `L` via the basis `e`. -/
  obtain ⟨b, hb⟩ : ∃ b : _ → K, M.det.eval (algebraMap K L ∘ b) ≠ 0 := by
    by_contra! h
    refine hM (MvPolynomial.funext_set _
      (fun _ ↦ Set.infinite_range_of_injective (algebraMap K L).injective) fun x hx ↦ ?_)
    obtain ⟨x, rfl⟩ := Set.range_piMap _ ▸ hx
    simpa using h x
  /- This element of `L` is exactly what we want: we simply need to show the first row of the
    evaluated matrix is `K`-linearly independent. But since the other rows are obtained from the
    first row by applying a `K`-endomorphism, it suffices to show that the columns are linearly
    independent, which follows from the nonzeroness of the evaluated determinant. -/
  refine ⟨∑ k, b k • e k, Fintype.linearIndependent_iff.mpr fun a ha ↦
    funext_iff.mp <| (algebraMap K L).injective.comp_left ?_⟩
  simp_rw [Function.comp_def, map_zero]
  rw [RingHom.map_det, RingHom.mapMatrix_apply] at hb
  refine Matrix.eq_zero_of_mulVec_eq_zero hb (funext fun i ↦ i.injective ?_)
  simp_rw [M, Pi.zero_apply, map_zero, ← ha]
  simp [Algebra.smul_def, Matrix.mulVec_eq_sum, mul_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.NormalBasis (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have inl : ∀ (h : Finite K), ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: obtain h | h := finite_or_infinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.NormalBasis (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inl : ∀ (h : Finite K), ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have inr : ∀ (h : Infinite K), ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: obtain h | h := finite_or_infinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.NormalBasis (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
h : Finite K
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have this : Finite L
Tactic: have := Module.finite_of_finite K (M := L)
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have op : ∀ (L₁ : FiniteGaloisIntermediateField k K) (f : op L₁ ⟶ L₂),
  finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Tactic: induction L₁ with | _ L₁ => ?_
Cleared hypotheses: L₁, f
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
g : L₂ ⟶ L₃
L₁ : FiniteGaloisIntermediateField k K
f : op L₁ ⟶ L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have op : ∀ (L₂ : FiniteGaloisIntermediateField k K) (g : op L₂ ⟶ L₃) (f : op L₁ ⟶ op L₂),
  finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Tactic: induction L₂ with | _ L₂ => ?_
Cleared hypotheses: L₂, g, f
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
L₁ L₂ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ L₃
f : op L₁ ⟶ op L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have op : ∀ (L₃ : FiniteGaloisIntermediateField k K) (g : op L₂ ⟶ op L₃),
  finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Tactic: induction L₃ with | _ L₃ => ?_
Cleared hypotheses: L₃, g
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : 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
have op : ∀ (L₁ : IntermediateField k K) [finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁]
  [isGalois : IsGalois.{u_1, u_2} k ↥L₁]
  (f :
    op
        { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
          FiniteGaloisIntermediateField k K } ⟶
      op L₂),
  finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Tactic: induction L₁ with | _ L₁ => ?_
Cleared hypotheses: L₁, f
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₂ L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
L₁ : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_1, u_2} k ↥L₁
isGalois : IsGalois.{u_1, u_2} k ↥L₁
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have op : ∀ (L₂ : IntermediateField k K) [finiteDimensional_1 : FiniteDimensional.{u_1, u_2} k ↥L₂]
  [isGalois_1 : IsGalois.{u_1, u_2} k ↥L₂]
  (g :
    op
        { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
          FiniteGaloisIntermediateField k K } ⟶
      op L₃)
  (f :
    op
        { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
          FiniteGaloisIntermediateField k K } ⟶
      op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }),
  finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Tactic: induction L₂ with | _ L₂ => ?_
Cleared hypotheses: L₂, g, f
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L₃ : FiniteGaloisIntermediateField 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₂
g :
  op
      { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 :
        FiniteGaloisIntermediateField k K } ⟶
    op L₃
f :
  op
      { toIntermediateField := L₁, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional_1, isGalois := isGalois_1 }
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have op : ∀ (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 }),
  finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Tactic: induction L₃ with | _ L₃ => ?_
Cleared hypotheses: L₃, g
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have 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 :
    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 }),
  finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Tactic: iterate 2
    induction L₁ with | _ L₁ => ?_
    induction L₂ with | _ L₂ => ?_
    induction L₃ with | _ L₃ => ?_
Cleared hypotheses: L₁, L₂, L₃, f, g
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (hypothesis)
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
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have this : IsScalarTower.{u_1, u_2, u_2} k ↥L₂ ↥L₁
Tactic: have : IsScalarTower k L₂ L₁ := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (hypothesis)
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₁
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have this₁ : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₁
Tactic: have : IsScalarTower k L₃ L₁ := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (hypothesis)
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₁
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have this₁ : IsScalarTower.{u_1, u_2, u_2} k ↥L₃ ↥L₂
Tactic: have : IsScalarTower k L₃ L₂ := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (hypothesis)
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₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
have this₁ : IsScalarTower.{u_2, u_2, u_2} ↥L₃ ↥L₂ ↥L₁
Tactic: have : IsScalarTower L₃ L₂ L₁ := IsScalarTower.of_algebraMap_eq' rfl