-- 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)))
    ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb :
  Ne (α := L)
    (Matrix.det
      (M.map
        (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)))
    0
a : Gal(L/K) → K
ha :
  Eq.{u_2 + 1} (α := L)
    (∑ i : Gal(L/K),
      HSMul.hSMul (β := L) (a i)
        ((i : (a : L) → L)
            (∑ k : Module.Free.ChooseBasisIndex K L,
              HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
          L))
    0
i : Gal(L/K)
simp_rw :
  Eq (α := L)
    ((i : (a : L) → L)
        (Matrix.mulVec
          (Matrix.map (α := 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))
            (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
              (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L))
          (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x)) i) :
      L)
    (∑ i : Gal(L/K),
        HSMul.hSMul (β := L) (a i)
          ((i : (a : L) → L)
              (∑ k : Module.Free.ChooseBasisIndex K L,
                HSMul.hSMul (β := L) (b k) ((e : (a : Module.Free.ChooseBasisIndex K L) → L) k : L)) :
            L) :
      L)
⊢ Eq (α := L)
    ((i : (a : L) → L)
        (Matrix.mulVec
          (M.map
            (⇑(MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b)) :
              (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L))
          (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x)) i) :
      L)
    ((i : (a : L) → L) (0 i) : L)

Tactic:
simp_rw [M, Pi.zero_apply, map_zero, ← ha]

Premises used: Pi.zero_apply, map_zero