awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst_5 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_6 : Finite G
E : IntermediateField K L
hE : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥E) L
h_1 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this_1 : Algebra ↥E ↥F := (IntermediateField.inclusion h_1).toAlgebra
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
a : ↥E
ha : (algebraMap (↥E) L : (a : ↥E) → L) a = (↑x : L)
this : IsScalarTower (↥E) (↥F) L
rw : Eq (α := L) ((algebraMap (↥E) L : (a : ↥E) → L) a : L) ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
rw₁ : (↑x : L) = (algebraMap (↥F) L : (a : ↥F) → L) x
⊢ Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap ↥E ↥F : (a : ↥E) → ↥F) a : ↥F) : L)
    ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
have rw₂ : (↑x : L) = (↑x : L)
Tactic: rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply]
-- 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 : Finite L
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have this : Finite K
Tactic: have := Finite.of_injective _ (algebraMap K L).injective
-- 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 : Finite L
this : Finite K
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have have : ∀ (this : Fintype K), ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: have := Fintype.ofFinite 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 : Finite L
this_1 : Finite K
this : Fintype K
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have obtain : ∀ (x : AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
  (hx :
    Eq.{u_1 + 1} (α := Submodule K[X] K[X])
      (ker (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L))) x))
      (Module.annihilator.{u_1, u_2} K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L))))),
  ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: obtain ⟨x, hx⟩ := exists_ker_toSpanSingleton_eq_annihilator K[X]
    (AEval' (frobeniusAlgHom K L).toLinearMap)
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L))
hx :
  Eq.{u_1 + 1} (α := Submodule K[X] K[X])
    (ker (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L))) x))
    (Module.annihilator.{u_1, u_2} K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L))))
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have obtain : ∀ (x : L)
  (hx :
    Eq.{u_1 + 1} (α := Submodule K[X] K[X])
      (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
        (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
            ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
              x) :
          LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
            (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
      (Module.annihilator.{u_1, u_2} K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L))))),
  ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: obtain ⟨x, rfl⟩ := (AEval'.of _).surjective x
Cleared hypotheses: x, hx
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : L
hx :
  Eq.{u_1 + 1} (α := Submodule K[X] K[X])
    (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
          ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
            x) :
        LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
          (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
    (Module.annihilator.{u_1, u_2} K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L))))
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have h : LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: use x
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : L
hx :
  Eq.{u_1 + 1} (α := Submodule K[X] K[X])
    (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
          ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
            x) :
        LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
          (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
    (Module.annihilator.{u_1, u_2} K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L))))
⊢ LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have hx₁ : Eq (α := Submodule K[X] K[X]) (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
  (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
    (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
        ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
          x) :
      LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
        (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
Tactic: rw [← span_minpoly_eq_annihilator, minpoly_frobeniusAlgHom, eq_comm] at hx
Cleared hypotheses: hx
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : L
hx :
  Eq (α := Submodule K[X] K[X]) (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
    (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
          ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
            x) :
        LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
          (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
⊢ LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have h : LinearIndependent (ι := Fin (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1).natDegree) K (M := L)
  ((fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x) ∘
    (⇑(Equiv.trans (finCongr sorry)
          (Equiv.ofBijective
            (fun (n : Fin (finrank K L)) ↦ HPow.hPow (α := Gal(L/K)) (frobeniusAlgEquivOfAlgebraic K L) (↑n : ℕ)) sorry)) :
      (a : Fin (X ^ finrank K L - (C : (a : K) → K[X]) 1).natDegree) → Gal(L/K)))
Tactic: rw [← linearIndependent_equiv ((finCongr <| natDegree_X_pow_sub_C (R := K)).trans <|
    .ofBijective _ <| bijective_frobeniusAlgEquivOfAlgebraic_pow K L)]
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : L
hx :
  Eq (α := Submodule K[X] K[X]) (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
    (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
          ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
            x) :
        LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
          (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
h :
  LinearIndependent (ι := Fin (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1).natDegree) K (M := L)
    ((fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x) ∘
      (⇑(Equiv.trans (finCongr ⋯)
            (Equiv.ofBijective
              (fun (n : Fin (finrank K L)) ↦ HPow.hPow (α := Gal(L/K)) (frobeniusAlgEquivOfAlgebraic K L) (↑n : ℕ))
              ⋯)) :
        (a : Fin (X ^ finrank K L - (C : (a : K) → K[X]) 1).natDegree) → Gal(L/K)))
⊢ LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have rw : K
Tactic: rw [← linearIndependent_equiv ((finCongr <| natDegree_X_pow_sub_C (R := K)).trans <|
    .ofBijective _ <| bijective_frobeniusAlgEquivOfAlgebraic_pow K L)]
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : L
hx :
  Eq (α := Submodule K[X] K[X]) (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
    (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
          ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
            x) :
        LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
          (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
e_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext i
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : L
hx :
  Eq (α := Submodule K[X] K[X]) (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
    (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
          ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
            x) :
        LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
          (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
e_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : Fin (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1).natDegree
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : (⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L)^[(↑(Fin.cast sorry i) : ℕ)] x =
  Function.comp (β := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
    (⇑(LinearEquiv.symm (AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)))) :
      (a : AEval' (frobeniusAlgHom K L).toLinearMap) → L)
    (⇑(liftQ (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
          (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
            ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
              x))
          sorry) :
      (a : AdjoinRoot (X ^ finrank K L - (C : (a : K) → K[X]) 1)) → AEval' (frobeniusAlgHom K L).toLinearMap)
    (AdjoinRoot.root (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1) ^ (↑i : ℕ))
Tactic: simp_rw [Equiv.coe_trans, Function.comp_apply, finCongr_apply, Equiv.ofBijective_apply,
    AlgEquiv.coe_pow, AdjoinRoot.powerBasis, AdjoinRoot.powerBasisAux, Basis.coe_mk,
    coe_comp, LinearEquiv.coe_coe, LinearMap.coe_restrictScalars]
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : L
hx :
  Eq (α := Submodule K[X] K[X]) (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
    (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
          ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
            x) :
        LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
          (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
e_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : Fin (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1).natDegree
⊢ (⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L)^[(↑(Fin.cast ⋯ i) : ℕ)] x =
    Function.comp (β := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (⇑(LinearEquiv.symm (AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)))) :
        (a : AEval' (frobeniusAlgHom K L).toLinearMap) → L)
      (⇑(liftQ (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
            (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
              ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) :
                  (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
                x))
            ⋯) :
        (a : AdjoinRoot (X ^ finrank K L - (C : (a : K) → K[X]) 1)) → AEval' (frobeniusAlgHom K L).toLinearMap)
      (AdjoinRoot.root (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1) ^ (↑i : ℕ))
have h : Eq (α := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
  (((toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
            ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
              x) :
          LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
            (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))) :
        (a : K[X]) → AEval' (frobeniusAlgHom K L).toLinearMap)
      ((fun (x : K[X]) ↦ x ^ (↑i : ℕ)) X) :
    AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
  ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
      ((⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L)^[(↑(Fin.cast sorry i) : ℕ)] x) :
    AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
Tactic: refine (LinearEquiv.eq_symm_apply _).mpr (.symm <| (liftQ_apply ..).trans ?_)
-- 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 : Finite L
this_1 : Finite K
this : Fintype K
x : L
hx :
  Eq (α := Submodule K[X] K[X]) (Ideal.span {HPow.hPow (α := K[X]) X (finrank K L) - 1})
    (ker (M₂ := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
      (toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
          ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
            x) :
        LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
          (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))))
e_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : Fin (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1).natDegree
⊢ Eq (α := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
    (((toSpanSingleton K[X] (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
              ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) :
                  (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
                x) :
            LinearMap.{u_1, u_1, u_1, u_2} (R := K[X]) (RingHom.id K[X]) K[X]
              (AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))) :
          (a : K[X]) → AEval' (frobeniusAlgHom K L).toLinearMap)
        ((fun (x : K[X]) ↦ x ^ (↑i : ℕ)) X) :
      AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
    ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
        ((⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L)^[(↑(Fin.cast ⋯ i) : ℕ)] x) :
      AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
have h : Eq (α := AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
  ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
      ((⇑(AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → L)^[(↑i : ℕ)] x) :
    AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
  ((AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : L) → AEval' (frobeniusAlgHom K L).toLinearMap)
      ((⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L)^[(↑(Fin.cast sorry i) : ℕ)] x) :
    AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
Tactic: rw [toSpanSingleton_apply, AEval'.X_pow_smul_of, End.smul_def, End.coe_pow]
-- 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 have : ∀ (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: have e := Module.Free.chooseBasis K L
-- 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
inst_4 : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  (Matrix.of :
      (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
        Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
    fun (i j : Gal(L/K)) ↦
    ∑ k : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
        ((i.symm : (a : L) → L) ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) : L)
        (MvPolynomial.X k)
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have hq : Eq (α := Submodule L ((j : Gal(L/K)) → L))
  (Submodule.span L
    (Set.range fun (k : Module.Free.ChooseBasisIndex K L) (j : Gal(L/K)) ↦
      (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)))
  ⊤
Tactic: 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
-- 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
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  (Matrix.of :
      (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
        Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
    fun (i j : Gal(L/K)) ↦
    ∑ k : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
        ((i.symm : (a : L) → L) ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) : L)
        (MvPolynomial.X k)
hq :
  Eq (α := Submodule L ((j : Gal(L/K)) → L))
    (Submodule.span L
      (Set.range fun (k : Module.Free.ChooseBasisIndex K L) (j : Gal(L/K)) ↦
        (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)))
    ⊤
⊢ ∃ (c : Module.Free.ChooseBasisIndex K L → L),
    Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
have obtain : ∀ (g : Module.Free.ChooseBasisIndex K L → L)
  (hg :
    Eq.{u_2 + 1} (α := (j : Gal(L/K)) → L)
      (∑ i : Module.Free.ChooseBasisIndex K L,
        HSMul.hSMul (β := (j : Gal(L/K)) → L) (g i) fun (j : Gal(L/K)) ↦
          (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) i : L))
      (Pi.single (M := fun (j : Gal(L/K)) ↦ L) 1 1)),
  ∃ (c : Module.Free.ChooseBasisIndex K L → L),
    Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
Tactic: obtain ⟨g, hg⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp
      (hq ▸ Submodule.mem_top (x := Pi.single 1 1))
-- 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
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  (Matrix.of :
      (a : Gal(L/K) → Gal(L/K) → MvPolynomial (Module.Free.ChooseBasisIndex K L) L) →
        Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L))
    fun (i j : Gal(L/K)) ↦
    ∑ k : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (α := L) (β := MvPolynomial (Module.Free.ChooseBasisIndex K L) L)
        ((i.symm : (a : L) → L) ((j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L) : L) : L)
        (MvPolynomial.X k)
hq :
  Eq (α := Submodule L ((j : Gal(L/K)) → L))
    (Submodule.span L
      (Set.range fun (k : Module.Free.ChooseBasisIndex K L) (j : Gal(L/K)) ↦
        (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)))
    ⊤
g : Module.Free.ChooseBasisIndex K L → L
hg :
  Eq.{u_2 + 1} (α := (j : Gal(L/K)) → L)
    (∑ i : Module.Free.ChooseBasisIndex K L,
      HSMul.hSMul (β := (j : Gal(L/K)) → L) (g i) fun (j : Gal(L/K)) ↦
        (j : (a : L) → L) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) i : L))
    (Pi.single (M := fun (j : Gal(L/K)) ↦ L) 1 1)
⊢ ∃ (c : Module.Free.ChooseBasisIndex K L → L),
    Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
have simp_rw : ∃ (c : Module.Free.ChooseBasisIndex K L → L),
  Eq.{u_2 + 1} (α := L)
    (Matrix.det (n := Gal(L/K))
      ((RingHom.mapMatrix (MvPolynomial.eval c) :
          (a : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L)) →
            Matrix Gal(L/K) Gal(L/K) L)
        M))
    1
Tactic: simp_rw [RingHom.map_det]