awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))))
e_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : 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)

Tactic:
ext i
-- 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)))))
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
h :
  (⇑(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 : ℕ))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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]

Premises used: finCongr_apply, AlgEquiv.coe_pow, LinearMap.coe_restrictScalars, Equiv.ofBijective_apply, Module.Basis.coe_mk, LinearMap.coe_comp, Function.comp_apply, Equiv.coe_trans, AdjoinRoot.powerBasisAux, LinearEquiv.coe_coe, AdjoinRoot.powerBasis
-- 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)))))
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 : ℕ))

Tactic:
(LinearEquiv.eq_symm_apply _).mpr (.symm <| (liftQ_apply ..).trans ?_)

Premises used: Iff.mpr, LinearEquiv.eq_symm_apply, Submodule.liftQ_apply, Eq.symm, Eq.trans
-- 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)))))
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
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 ⋯ i) : ℕ)] x) :
      AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
⊢ (⇑(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 : ℕ))

Tactic:
refine (LinearEquiv.eq_symm_apply _).mpr (.symm <| (liftQ_apply ..).trans ?_)

Premises used: Iff.mpr, LinearEquiv.eq_symm_apply, Submodule.liftQ_apply, Eq.symm, Eq.trans
-- 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)))))
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
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 ⋯ i) : ℕ)] x) :
      AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))
⊢ 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)))

Tactic:
rw [toSpanSingleton_apply, AEval'.X_pow_smul_of, End.smul_def, End.coe_pow]

Premises used: Module.End.smul_def, Module.AEval'.X_pow_smul_of, Module.End.coe_pow, LinearMap.toSpanSingleton_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
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)))
    ((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 ⋯ i) : ℕ)] x) :
      AEval' (AlgHom.toLinearMap (frobeniusAlgHom K L)))

Tactic:
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 : FiniteDimensional K L
inst_4 : Infinite K
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
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x

Tactic:
have e := Module.Free.chooseBasis K L
-- 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 : 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)
⊢ 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:
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

Premises used: Iff.mpr, LinearEquiv.symm, linearIndependent_algHom_toLinearMap, LinearIndependent.map', algEquivEquivAlgHom, span_flip_eq_top_iff_linearIndependent, LinearEquiv.ker, LinearIndependent.comp, MulEquiv.injective, Module.Basis.constr
-- 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 : 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)
⊢ 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
-- 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 : 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)))
    ⊤
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)
⊢ ∃ (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))

Premises used: Submodule.mem_span_range_iff_exists_fun, Iff.mp
-- 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 : 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)
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
⊢ ∃ (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:
simp_rw [RingHom.map_det]

Premises used: RingHom.map_det
-- 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 : 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.{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:
⟨g, congr(Matrix.det $(?_)).trans Matrix.det_one⟩

Premises used: congrArg, id, Exists.intro, Matrix.det_one, Matrix.det, Eq.trans
-- 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 : 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)
refine :
  Eq (α := Matrix Gal(L/K) Gal(L/K) L)
    ((RingHom.mapMatrix (MvPolynomial.eval g) :
          (a : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L)) →
            Matrix Gal(L/K) Gal(L/K) L)
        M :
      Matrix Gal(L/K) Gal(L/K) L)
    (1 : Matrix Gal(L/K) Gal(L/K) L)
⊢ ∃ (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:
refine ⟨g, congr(Matrix.det $(?_)).trans Matrix.det_one⟩