-- 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)
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)
have obtain : ∀ (x : (i : Module.Free.ChooseBasisIndex K L) → K)
  (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))
      (Pi.map (α := fun (i : Module.Free.ChooseBasisIndex K L) ↦ K) (β := fun (i : Module.Free.ChooseBasisIndex K L) ↦
        L) (fun (x : Module.Free.ChooseBasisIndex K L) ↦ (⇑(algebraMap K L : K →+* L) : (a : K) → L)) x)),
  Eq (α := L)
    ((MvPolynomial.eval
            (Pi.map (α := fun (i : Module.Free.ChooseBasisIndex K L) ↦ K) (β :=
              fun (i : Module.Free.ChooseBasisIndex K L) ↦ L)
              (fun (x : Module.Free.ChooseBasisIndex K L) ↦ (⇑(algebraMap K L : K →+* L) : (a : K) → L)) x) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
        M.det :
      L)
    ((MvPolynomial.eval
            (Pi.map (α := fun (i : Module.Free.ChooseBasisIndex K L) ↦ K) (β :=
              fun (i : Module.Free.ChooseBasisIndex K L) ↦ L)
              (fun (x : Module.Free.ChooseBasisIndex K L) ↦ (⇑(algebraMap K L : K →+* L) : (a : K) → L)) x) :
          (a : MvPolynomial (Module.Free.ChooseBasisIndex K L) L) → L)
        0 :
      L)
Tactic: obtain ⟨x, rfl⟩ := Set.range_piMap _ ▸ hx
Cleared hypotheses: x, hx