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
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
have 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)
Tactic: refine ⟨g, congr(Matrix.det $(?_)).trans Matrix.det_one⟩
-- 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)
⊢ 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)
have a : ∀ (i j : Gal(L/K)),
  Eq (α := 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 i j :
      L)
    (1 i j : L)
Tactic: ext i j
-- 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)))
    ⊤
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have obtain : ∀ (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)),
  ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: 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))
-- 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)
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)
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have hM : M.det ≠ 0
Tactic: have hM : M.det ≠ 0 := fun h0 ↦ by
    simpa [hc] using congr(($h0).eval c)
-- 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
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),
    Ne (α := L)
      ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
            (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
          M.det :
        L)
      (0 : L)
have by_contra! : ∀
  (h :
    ∀ (b : Module.Free.ChooseBasisIndex K L → K),
      Eq (α := L)
        ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
              (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
            M.det :
          L)
        (0 : L)),
  False
Tactic: by_contra! h
-- 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
hc : Eq (α := L) ((MvPolynomial.eval c : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L) (1 : L)
hM : M.det ≠ 0
h :
  ∀ (b : Module.Free.ChooseBasisIndex K L → K),
    Eq (α := L)
      ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
            (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
          M.det :
        L)
      (0 : L)
⊢ False
have refine : ∀ (x : (i : Module.Free.ChooseBasisIndex K L) → L)
  (hx :
    Membership.mem (γ := Set ((i : Module.Free.ChooseBasisIndex K L) → L))
      (Set.pi (α := fun (i : Module.Free.ChooseBasisIndex K L) ↦ L) Set.univ
        fun (x : Module.Free.ChooseBasisIndex K L) ↦
        Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L : K →+* L) : (a : K) → L))
      x),
  Eq (α := L) ((MvPolynomial.eval x : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) M.det : L)
    ((MvPolynomial.eval x : (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L) 0 : L)
Tactic: refine hM (MvPolynomial.funext_set _
      (fun _ ↦ Set.infinite_range_of_injective (algebraMap K L).injective) fun 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 : 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
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have obtain : ∀ (b : Module.Free.ChooseBasisIndex K L → K)
  (hb :
    Ne (α := L)
      ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
            (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
          M.det :
        L)
      (0 : L)),
  ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
Tactic: 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
-- 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
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)
    ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
        M.det :
      L)
    (0 : L)
⊢ ∃ (x : L), LinearIndependent K (M := L) fun (σ : Gal(L/K)) ↦ (σ : (a : L) → L) x
have refine : ∀ (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),
  Eq.{u_2 + 1} (α := Gal(L/K) → L)
    ((fun (x : Gal(L/K) → K) ↦ ((⇑(algebraMap K L : K →+* L) : (a : K) → L) ∘ x : Gal(L/K) → L)) a)
    ((fun (x : Gal(L/K) → K) ↦ ((⇑(algebraMap K L : K →+* L) : (a : K) → L) ∘ x : Gal(L/K) → L)) fun (i : Gal(L/K)) ↦ 0)
Tactic: refine ⟨∑ k, b k • e k, Fintype.linearIndependent_iff.mpr fun a ha ↦
    funext_iff.mp <| (algebraMap K L).injective.comp_left ?_⟩
-- 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
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)
    ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
        M.det :
      L)
    (0 : L)
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
⊢ Eq.{u_2 + 1} (α := Gal(L/K) → L)
    ((fun (x : Gal(L/K) → K) ↦ ((⇑(algebraMap K L : K →+* L) : (a : K) → L) ∘ x : Gal(L/K) → L)) a)
    ((fun (x : Gal(L/K) → K) ↦ ((⇑(algebraMap K L : K →+* L) : (a : K) → L) ∘ x : Gal(L/K) → L)) fun (i : Gal(L/K)) ↦ 0)
have simp_rw : Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
  fun (x : Gal(L/K)) ↦ 0
Tactic: simp_rw [Function.comp_def, map_zero]
-- 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
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)
    ((MvPolynomial.eval ((⇑(algebraMap K L) : (a : K) → L) ∘ b) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
        M.det :
      L)
    (0 : L)
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
⊢ Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
    fun (x : Gal(L/K)) ↦ 0
have rw : ∀
  (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),
  Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
    fun (x : Gal(L/K)) ↦ 0
Tactic: rw [RingHom.map_det, RingHom.mapMatrix_apply] at hb
Cleared hypotheses: hb, a, ha
-- 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
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
⊢ Eq.{u_2 + 1} (α := Gal(L/K) → L) (fun (x : Gal(L/K)) ↦ ((algebraMap K L : K →+* L) : (a : K) → L) (a x))
    fun (x : Gal(L/K)) ↦ 0
have refine : ∀ (i : Gal(L/K)),
  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: refine Matrix.eq_zero_of_mulVec_eq_zero hb (funext fun i ↦ i.injective ?_)