Fix 2018 B5 (again)

This was previously "fixed" in c75c0b0
but unfortunately an error remained.

Alternative spellings of the basis element `fun k ↦ if k = i then 1 else 0`
are:
 * `if i = 0 then ![1, 0] else ![0, 1]`
 * `LinearMap.stdBasis ℝ _ i 1`

lean4/src/putnam_2018_b5.lean

@@ -6,8 +6,8 @@ open Function
 theorem putnam_2018_b5
     (f : (Fin 2 → ℝ) → (Fin 2 → ℝ))
     (h₁ : ContDiff ℝ 1 f)
-    (h₂ : ∀ x i j, 0 < fderiv ℝ f x i j)
-    (h₃ : ∀ x, 0 < fderiv ℝ f x 0 0 * fderiv ℝ f x 1 1 -
-      (1 / 4) * (fderiv ℝ f x 0 1 + fderiv ℝ f x 1 0) ^ 2) :
+    (h₂ : ∀ x i j, 0 < fderiv ℝ f x (fun k ↦ if k = i then 1 else 0) j)
+    (h₃ : ∀ x, 0 < fderiv ℝ f x ![1, 0] 0 * fderiv ℝ f x ![0, 1] 1 -
+      (1 / 4) * (fderiv ℝ f x ![1, 0] 1 + fderiv ℝ f x ![0, 1] 0) ^ 2) :
     Injective f :=
   sorry