-- 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
Choose Choose₁ Choose₂ Choose₃ :
  ∀ (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
have Choose₄ : ∀ (e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L)
  (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
Tactic: classical
  /- Choose a basis `e` of `L` over `K` and form the matrix `M` with entries
    `∑ₖ i⁻¹j(eₖ)Xₖ` where `i,j ∈ Gal(L/K)` and `Xₖ`s are independent variables. -/
  have e := Module.Free.chooseBasis K L
  let M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial _ L) :=
    .of fun i j ↦ ∑ k, i.symm (j (e k)) • .X k
  /- By [ConradLinearChar] Lemma 3.4, there exists `{xₖ} ⊆ L` such that `∑ₖ j(eₖ)xₖ = 1`
    if `j = 1` and `∑ₖ j(eₖ)xₖ = 0` otherwise. -/
  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
  /- If we evaluate `M` at `Xₖ = xₖ`, the determinant of `M` evaluates to 1. -/
  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))
  /- Therefore `det M` is nonzero. -/
  have hM : M.det ≠ 0 := fun h0 ↦ by
    simpa [hc] using congr(($h0).eval c)
  /- Since `K` is infinite, we may evaluate `det M` at some point with coordinates in `K`
    and get a nonzero value. The coordinates give rise to an element of `L` via the basis `e`. -/
  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
  /- This element of `L` is exactly what we want: we simply need to show the first row of the
    evaluated matrix is `K`-linearly independent. But since the other rows are obtained from the
    first row by applying a `K`-endomorphism, it suffices to show that the columns are linearly
    independent, which follows from the nonzeroness of the evaluated determinant. -/
  refine ⟨∑ k, b k • e k, Fintype.linearIndependent_iff.mpr fun a ha ↦
    funext_iff.mp <| (algebraMap K L).injective.comp_left ?_⟩
  simp_rw [Function.comp_def, map_zero]
  rw [RingHom.map_det, RingHom.mapMatrix_apply] at hb
  refine Matrix.eq_zero_of_mulVec_eq_zero hb (funext fun i ↦ i.injective ?_)
  simp_rw [M, Pi.zero_apply, map_zero, ← ha]
  simp [Algebra.smul_def, Matrix.mulVec_eq_sum, mul_comm]