awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
H H' : Subgroup G
F F' : IntermediateField K L
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
g : G
⊢ g • (↑x : L) = (↑x : L)

Tactic:
simpa [coe_quotient_smul] using congr_arg Subtype.val (h g)

Premises used: QuotientGroup.mk, congr_arg, IsGaloisGroup.coe_quotient_smul, Subtype.val
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
H H' : Subgroup G
F F' : IntermediateField K L
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
⊢ ∀ (g : G), g • (↑x : L) = (↑x : L)

Tactic:
have : ∀ (g : G), g • (x : L) = x := fun g ↦ by
      simpa [coe_quotient_smul] using congr_arg Subtype.val (h g)
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
H H' : Subgroup G
F F' : IntermediateField K L
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
obtain : ∀ (a : K) (ha : (algebraMap K L : (a : K) → L) a = (↑x : L)), ∃ (a : K), (algebraMap K ↥F : (a : K) → ↥F) a = x
⊢ ∃ (a : K), (algebraMap K ↥F : (a : K) → ↥F) a = x

Tactic:
obtain ⟨a, ha⟩ := hK.isInvariant.isInvariant x this

Premises used: Algebra.IsInvariant.isInvariant, Subtype.val
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
H H' : Subgroup G
F F' : IntermediateField K L
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
a : K
ha : (algebraMap K L : (a : K) → L) a = (↑x : L)
⊢ ∃ (a : K), (algebraMap K ↥F : (a : K) → ↥F) a = x

Tactic:
⟨a, FaithfulSMul.algebraMap_injective F L ?_⟩

Premises used: Membership.mem, Subtype, FaithfulSMul.algebraMap_injective, Exists.intro
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
H H' : Subgroup G
F F' : IntermediateField K L
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
a : K
ha : (algebraMap K L : (a : K) → L) a = (↑x : L)
refine :
  Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap K ↥F : (a : K) → ↥F) a : ↥F) : L)
    ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
⊢ ∃ (a : K), (algebraMap K ↥F : (a : K) → ↥F) a = x

Tactic:
refine ⟨a, FaithfulSMul.algebraMap_injective F L ?_⟩
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
H H' : Subgroup G
F F' : IntermediateField K L
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
a : K
ha : (algebraMap K L : (a : K) → L) a = (↑x : L)
rw : Eq.{u_4 + 1} (α := L) ((algebraMap K L : (a : K) → L) a : L) ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
rw₁ : (↑x : L) = (algebraMap (↥F) L : (a : ↥F) → L) x
rw₂ rw₃ : (↑x : L) = (↑x : L)
⊢ Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap K ↥F : (a : K) → ↥F) a : ↥F) : L)
    ((algebraMap (↥F) L : (a : ↥F) → L) x : L)

Tactic:
rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply]

Premises used: IntermediateField.algebraMap_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
⊢ FaithfulSMul.{u_1, u_4} (G ⧸ N) ↥F

Tactic:
have := hFN.faithful
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this_1 : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
this : FaithfulSMul.{u_1, u_4} (G ⧸ N) ↥F
⊢ FaithfulSMul.{u_1, u_4} ↥(Subgroup.map (QuotientGroup.mk' N) H) ↥F

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
g : G
hg : g ∈ (↑H : Set G)
x : ↥E
y : ↥F
⊢ HSMul.hSMul (α := ↥(Subgroup.map (QuotientGroup.mk' N) H))
      (Subtype.mk (p := fun (x : G ⧸ N) ↦
          Membership.mem (γ := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) H) x)
          ((QuotientGroup.mk' N : (a : G) → G ⧸ N) g) ⋯ :
        ↥(Subgroup.map (QuotientGroup.mk' N) H))
      (x • y) =
    x •
      HSMul.hSMul (α := ↥(Subgroup.map (QuotientGroup.mk' N) H))
        (Subtype.mk (p := fun (x : G ⧸ N) ↦
            Membership.mem (γ := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) H) x)
            ((QuotientGroup.mk' N : (a : G) → G ⧸ N) g) ⋯ :
          ↥(Subgroup.map (QuotientGroup.mk' N) H))
        y

Tactic:
FaithfulSMul.algebraMap_injective F L (hE.commutes.smul_comm ⟨g, hg⟩ x (y : L))

Premises used: Membership.mem, Subtype, Subtype.mk, FaithfulSMul.algebraMap_injective, SMulCommClass.smul_comm, Subtype.val
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
g : G
hg : g ∈ (↑H : Set G)
x : ↥E
y : ↥F
⊢ HSMul.hSMul (α := ↥(Subgroup.map (QuotientGroup.mk' N) H))
      (Subtype.mk (p := fun (x : G ⧸ N) ↦
          Membership.mem (γ := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) H) x)
          ((QuotientGroup.mk' N : (a : G) → G ⧸ N) g) ⋯ :
        ↥(Subgroup.map (QuotientGroup.mk' N) H))
      (x • y) =
    x •
      HSMul.hSMul (α := ↥(Subgroup.map (QuotientGroup.mk' N) H))
        (Subtype.mk (p := fun (x : G ⧸ N) ↦
            Membership.mem (γ := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) H) x)
            ((QuotientGroup.mk' N : (a : G) → G ⧸ N) g) ⋯ :
          ↥(Subgroup.map (QuotientGroup.mk' N) H))
        y

Tactic:
exact FaithfulSMul.algebraMap_injective F L (hE.commutes.smul_comm ⟨g, hg⟩ x (y : L))

Premises used: Membership.mem, Subtype, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 : Algebra ↥E ↥F := (IntermediateField.inclusion h_1).toAlgebra
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
obtain :
  ∀ (a : ↥E) (ha : (algebraMap (↥E) L : (a : ↥E) → L) a = (↑x : L)),
    ∃ (a : ↥E), (algebraMap ↥E ↥F : (a : ↥E) → ↥F) a = x
⊢ ∃ (a : ↥E), (algebraMap ↥E ↥F : (a : ↥E) → ↥F) a = x

Tactic:
obtain ⟨a, ha⟩ := hE.isInvariant.isInvariant x
        fun ⟨g, hg⟩ ↦ congr_arg Subtype.val (h ⟨g, g, hg, rfl⟩)

Premises used: QuotientGroup.mk, _private.0.IsGaloisGroup.fixedPoints_le_of_le.match_1, Subtype.mk, congr_arg, Algebra.IsInvariant.isInvariant, And.intro, Exists.intro, HSMul.hSMul, Subtype.val, Eq, rfl
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 : 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)
⊢ IsScalarTower (↥E) (↥F) L

Tactic:
have : IsScalarTower E F L := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
rw₂ rw₃ : (↑x : L) = (↑x : L)
⊢ 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)

Tactic:
rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply]

Premises used: IntermediateField.algebraMap_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ ∃ (a : ↥E), (algebraMap ↥E ↥F : (a : ↥E) → ↥F) a = x

Tactic:
exact ⟨a, FaithfulSMul.algebraMap_injective F L
        (by rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply])⟩
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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
⊢ Finite K

Tactic:
have := Finite.of_injective _ (algebraMap K L).injective
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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
have : ∀ (this : Fintype 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

Tactic:
have := Fintype.ofFinite K
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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
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
⊢ ∃ (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)

Premises used: AlgHom.toLinearMap, Module.AEval', Polynomial, FiniteField.frobeniusAlgHom, Module.exists_ker_toSpanSingleton_eq_annihilator
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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))))
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
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x

Tactic:
obtain ⟨x, rfl⟩ := (AEval'.of _).surjective x

Premises used: Module.AEval'.of, LinearEquiv.surjective, rfl
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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))))
h : 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

Tactic:
use x
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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))))
⊢ 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

Premises used: eq_comm, Polynomial.span_minpoly_eq_annihilator, FiniteField.minpoly_frobeniusAlgHom
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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)))
rw : K
⊢ LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x

Tactic:
rw [← linearIndependent_equiv ((finCongr <| natDegree_X_pow_sub_C (R := K)).trans <|
    .ofBijective _ <| bijective_frobeniusAlgEquivOfAlgebraic_pow K L)]

Premises used: Polynomial.natDegree_X_pow_sub_C, Equiv.trans, finCongr, linearIndependent_equiv, Equiv.ofBijective, FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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)))))
⊢ Eq (α := Submodule K (AdjoinRoot (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1)))
    (ker
      ((↑(LinearEquiv.symm (AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)))) :
          AEval' (frobeniusAlgHom K L).toLinearMap →ₗ[K] L) ∘ₗ
        (↑K :
            {S M : Type u_1} →
              {M₂ : Type u_2} →
                [inst : Semiring K] →
                  [inst_4 : Semiring S] →
                    [inst_5 : AddCommMonoid M] →
                      [inst_6 : AddCommMonoid M₂] →
                        [inst_7 : Module K M] →
                          [inst_8 : Module K M₂] →
                            [inst_9 : Module S M] →
                              [inst_10 : Module S M₂] → [CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
          (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))
            ⋯)))
    ⊥

Tactic:
congr($(ker_liftQ_eq_bot' _ _ hx).restrictScalars K)

Premises used: AlgHom.toLinearMap, congrArg, Submodule.restrictScalars, Module.AEval'.of, Module.AEval', HSub.hSub, id, Submodule.ker_liftQ_eq_bot', Polynomial, FiniteField.frobeniusAlgHom, HPow.hPow, Ideal.span, Singleton.singleton, OfNat.ofNat, Polynomial.X, DFunLike.coe, LinearMap.toSpanSingleton, Module.finrank
-- Module: Mathlib.FieldTheory.Galois.NormalBasis
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)))))
⊢ Eq (α := Submodule K (AdjoinRoot (HPow.hPow (α := K[X]) X (finrank K L) - (C : (a : K) → K[X]) 1)))
    (ker
      ((↑(LinearEquiv.symm (AEval'.of (AlgHom.toLinearMap (frobeniusAlgHom K L)))) :
          AEval' (frobeniusAlgHom K L).toLinearMap →ₗ[K] L) ∘ₗ
        (↑K :
            {S M : Type u_1} →
              {M₂ : Type u_2} →
                [inst : Semiring K] →
                  [inst_4 : Semiring S] →
                    [inst_5 : AddCommMonoid M] →
                      [inst_6 : AddCommMonoid M₂] →
                        [inst_7 : Module K M] →
                          [inst_8 : Module K M₂] →
                            [inst_9 : Module S M] →
                              [inst_10 : Module S M₂] → [CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
          (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))
            ⋯)))
    ⊥

Tactic:
exact congr($(ker_liftQ_eq_bot' _ _ hx).restrictScalars K)