Merge branch 'master' into YK-smul-set-prod

Archive/Arithcc.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Xi Wang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xi Wang
 -/
-import Mathlib.Data.Nat.Defs
+import Mathlib.Data.Nat.Basic
 import Mathlib.Order.Basic
 import Mathlib.Tactic.Common
 

Archive/Imo/Imo2006Q3.lean

@@ -80,7 +80,7 @@ theorem subst_proof₁ (x y z s : ℝ) (hxyz : x + y + z = 0) :
   wlog h' : 0 ≤ x * y generalizing x y z; swap
   · rw [div_mul_eq_mul_div, le_div_iff₀' zero_lt_32]
     exact subst_wlog h' hxyz
-  cases' (mul_nonneg_of_three x y z).resolve_left h' with h h
+  rcases (mul_nonneg_of_three x y z).resolve_left h' with h | h
   · convert this y z x _ h using 2 <;> linarith
   · convert this z x y _ h using 2 <;> linarith
 

Archive/Imo/Imo2006Q5.lean

@@ -53,8 +53,8 @@ theorem Int.natAbs_eq_of_chain_dvd {l : Cycle ℤ} {x y : ℤ} (hl : l.Chain (·
 theorem Int.add_eq_add_of_natAbs_eq_of_natAbs_eq {a b c d : ℤ} (hne : a ≠ b)
     (h₁ : (c - a).natAbs = (d - b).natAbs) (h₂ : (c - b).natAbs = (d - a).natAbs) :
     a + b = c + d := by
-  cases' Int.natAbs_eq_natAbs_iff.1 h₁ with h₁ h₁
-  · cases' Int.natAbs_eq_natAbs_iff.1 h₂ with h₂ h₂
+  rcases Int.natAbs_eq_natAbs_iff.1 h₁ with h₁ | h₁
+  · rcases Int.natAbs_eq_natAbs_iff.1 h₂ with h₂ | h₂
     · exact (hne <| by linarith).elim
     · linarith
   · linarith
@@ -110,7 +110,7 @@ theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
     push_neg at HC'
     obtain ⟨n, hn⟩ := HC'
     -- They must have opposite sign, so that P^{k + 1}(t) - P^k(t) = P^{k + 2}(t) - P^{k + 1}(t).
-    cases' Int.natAbs_eq_natAbs_iff.1 (Habs n n.succ) with hn' hn'
+    rcases Int.natAbs_eq_natAbs_iff.1 (Habs n n.succ) with hn' | hn'
     · apply (hn _).elim
       convert hn' <;> simp only [Function.iterate_succ_apply']
     -- We deduce P^{k + 2}(t) = P^k(t) and hence P(P(t)) = t.

Archive/Imo/Imo2008Q3.lean

@@ -48,7 +48,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   have hnat₃ : p ≥ 2 * n := by omega
   set k : ℕ := p - 2 * n with hnat₄
   have hnat₅ : p ∣ k ^ 2 + 4 := by
-    cases' hnat₁ with x hx
+    obtain ⟨x, hx⟩ := hnat₁
     have : (p : ℤ) ∣ (k : ℤ) ^ 2 + 4 := by
       use (p : ℤ) - 4 * n + 4 * x
       have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast

Archive/Imo/Imo2008Q4.lean

@@ -77,7 +77,7 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
   rw [hfa₂, hfb₂] at H₂
   have h2ab_ne_0 : 2 * (a * b) ≠ 0 := by positivity
   specialize h₃ (a * b) hab
-  cases' h₃ with hab₁ hab₂
+  rcases h₃ with hab₁ | hab₂
   -- f(ab) = ab → b^4 = 1 → b = 1 → f(b) = b → false
   · rw [hab₁, div_left_inj' h2ab_ne_0] at H₂
     field_simp at H₂

Archive/Imo/Imo2019Q1.lean

@@ -39,7 +39,7 @@ theorem imo2019_q1 (f : ℤ → ℤ) :
   -- Hence, `f` is an affine map, `f b = f 0 + m * b`
   obtain ⟨c, H⟩ : ∃ c, ∀ b, f b = c + m * b := by
     refine ⟨f 0, fun b => ?_⟩
-    induction' b using Int.induction_on with b ihb b ihb
+    induction' b with b ihb b ihb
     · simp
     · simp [H, ihb, mul_add, add_assoc]
     · rw [← sub_eq_of_eq_add (H _)]

Archive/Imo/Imo2021Q1.lean

@@ -126,5 +126,5 @@ theorem imo2021_q1 :
   rcases hC with ⟨a, ha, b, hb, hab⟩
   simp only [Finset.subset_iff, Finset.mem_inter] at hCA
   -- Now we split into the two cases C ⊆ [n, 2n] \ A and C ⊆ A, which can be dealt with identically.
-  cases' hCA with hCA hCA <;> [right; left] <;>
+  rcases hCA with hCA | hCA <;> [right; left] <;>
     exact ⟨a, (hCA ha).2, b, (hCA hb).2, hab, h₁ a (hCA ha).1 b (hCA hb).1 hab⟩

Archive/Imo/Imo2024Q3.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
+import Mathlib.Data.Fintype.Pigeonhole
 import Mathlib.Data.Nat.Nth
 
 /-!
@@ -30,7 +31,7 @@ open scoped Finset
 namespace Imo2024Q3
 
 /-- The condition of the problem. Following usual Lean conventions, this is expressed with
-indices starting from 0, rather than from 1 as in the informal statment (but `N` remains as the
+indices starting from 0, rather than from 1 as in the informal statement (but `N` remains as the
 index of the last term for which `a n` is not defined in terms of previous terms). -/
 def Condition (a : ℕ → ℕ) (N : ℕ) : Prop :=
   (∀ i, 0 < a i) ∧ ∀ n, N < n → a n = #{i ∈ Finset.range n | a i = a (n - 1)}

Archive/MiuLanguage/DecisionNec.lean

@@ -53,9 +53,9 @@ example : CountEquivOrEquivTwoMulMod3 "IUIM" "MI" :=
 -/
 theorem mod3_eq_1_or_mod3_eq_2 {a b : ℕ} (h1 : a % 3 = 1 ∨ a % 3 = 2)
     (h2 : b % 3 = a % 3 ∨ b % 3 = 2 * a % 3) : b % 3 = 1 ∨ b % 3 = 2 := by
-  cases' h2 with h2 h2
+  rcases h2 with h2 | h2
   · rw [h2]; exact h1
-  · cases' h1 with h1 h1
+  · rcases h1 with h1 | h1
     · right; simp [h2, mul_mod, h1, Nat.succ_lt_succ]
     · left; simp only [h2, mul_mod, h1, mod_mod]
 
@@ -122,7 +122,7 @@ We'll show, for each `i` from 1 to 4, that if `en` follows by Rule `i` from `st`
 
 theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ [I])) (h₂ : Goodm (xs ++ [I])) :
     Goodm (xs ++ [I, U]) := by
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   constructor
   · cases xs <;> simp_all
   · change ¬M ∈ tail (xs ++ ([I] ++ [U]))
@@ -134,14 +134,14 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
     Goodm ((M :: xs) ++ xs) := by
   constructor
   · rfl
-  · cases' h₂ with mhead mtail
+  · obtain ⟨mhead, mtail⟩ := h₂
     contrapose! mtail
     rw [cons_append] at mtail
     exact or_self_iff.mp (mem_append.mp mtail)
 
 theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [I, I, I] ++ bs))
     (h₂ : Goodm (as ++ [I, I, I] ++ bs)) : Goodm (as ++ (U :: bs)) := by
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   have k : as ≠ nil := by rintro rfl; contradiction
   constructor
   · cases as
@@ -159,7 +159,7 @@ The proof of the next lemma is identical, on the tactic level, to the previous p
 
 theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [U, U] ++ bs))
     (h₂ : Goodm (as ++ [U, U] ++ bs)) : Goodm (as ++ bs) := by
-  cases' h₂ with mhead nmtail
+  obtain ⟨mhead, nmtail⟩ := h₂
   have k : as ≠ nil := by rintro rfl; contradiction
   constructor
   · cases as

Archive/MiuLanguage/DecisionSuf.lean

@@ -143,7 +143,7 @@ private theorem le_pow2_and_pow2_eq_mod3' (c : ℕ) (x : ℕ) (h : c = 1 ∨ c =
     ∃ m : ℕ, c + 3 * x ≤ 2 ^ m ∧ 2 ^ m % 3 = c % 3 := by
   induction' x with k hk
   · use c + 1
-    cases' h with hc hc <;> · rw [hc]; norm_num
+    rcases h with hc | hc <;> · rw [hc]; norm_num
   rcases hk with ⟨g, hkg, hgmod⟩
   by_cases hp : c + 3 * (k + 1) ≤ 2 ^ g
   · use g, hp, hgmod
@@ -180,7 +180,7 @@ theorem der_replicate_I_of_mod3 (c : ℕ) (h : c % 3 = 1 ∨ c % 3 = 2) :
   -- From `der_cons_replicate`, we can derive the `Miustr` `M::w` described in the introduction.
   obtain ⟨m, hm⟩ := le_pow2_and_pow2_eq_mod3 c h -- `2^m` will be the number of `I`s in `M::w`
   have hw₂ : Derivable (M :: replicate (2 ^ m) I ++ replicate ((2 ^ m - c) / 3 % 2) U) := by
-    cases' mod_two_eq_zero_or_one ((2 ^ m - c) / 3) with h_zero h_one
+    rcases mod_two_eq_zero_or_one ((2 ^ m - c) / 3) with h_zero | h_one
     · -- `(2^m - c)/3 ≡ 0 [MOD 2]`
       simp only [der_cons_replicate m, append_nil, List.replicate, h_zero]
     · -- case `(2^m - c)/3 ≡ 1 [MOD 2]`
@@ -206,7 +206,7 @@ example (c : ℕ) (h : c % 3 = 1 ∨ c % 3 = 2) : Derivable (M :: replicate c I)
   -- From `der_cons_replicate`, we can derive the `Miustr` `M::w` described in the introduction.
   obtain ⟨m, hm⟩ := le_pow2_and_pow2_eq_mod3 c h -- `2^m` will be the number of `I`s in `M::w`
   have hw₂ : Derivable (M :: replicate (2 ^ m) I ++ replicate ((2 ^ m - c) / 3 % 2) U) := by
-    cases' mod_two_eq_zero_or_one ((2 ^ m - c) / 3) with h_zero h_one
+    rcases mod_two_eq_zero_or_one ((2 ^ m - c) / 3) with h_zero | h_one
     · -- `(2^m - c)/3 ≡ 0 [MOD 2]`
       simp only [der_cons_replicate m, append_nil, List.replicate, h_zero]
     · -- case `(2^m - c)/3 ≡ 1 [MOD 2]`

Archive/Sensitivity.lean

@@ -210,7 +210,7 @@ theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by
 theorem epsilon_total {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 := by
   induction' n with n ih
   · dsimp [ε] at h; exact h fun _ => true
-  · cases' v with v₁ v₂
+  · obtain ⟨v₁, v₂⟩ := v
     ext <;> change _ = (0 : V n) <;> simp only <;> apply ih <;> intro p <;>
       [let q : Q n.succ := fun i => if h : i = 0 then true else p (i.pred h);
       let q : Q n.succ := fun i => if h : i = 0 then false else p (i.pred h)]

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -6,8 +6,9 @@ Authors: Thomas Browning
 import Mathlib.Analysis.Calculus.LocalExtr.Polynomial
 import Mathlib.Analysis.Complex.Polynomial.Basic
 import Mathlib.FieldTheory.AbelRuffini
-import Mathlib.RingTheory.RootsOfUnity.Minpoly
 import Mathlib.RingTheory.EisensteinCriterion
+import Mathlib.RingTheory.Int.Basic
+import Mathlib.RingTheory.RootsOfUnity.Minpoly
 
 /-!
 # Construction of an algebraic number that is not solvable by radicals.

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -328,8 +328,8 @@ theorem ballot_problem' :
     rw [← uniformOn_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
       first_vote_pos _ _ h₃, first_vote_neg _ _ h₃, ballot_pos, ballot_neg _ _ qp]
     rw [ENNReal.toReal_add, ENNReal.toReal_mul, ENNReal.toReal_mul, ← Nat.cast_add,
-      ENNReal.toReal_div, ENNReal.toReal_div, ENNReal.toReal_nat, ENNReal.toReal_nat,
-      ENNReal.toReal_nat, h₁, h₂]
+      ENNReal.toReal_div, ENNReal.toReal_div, ENNReal.toReal_natCast, ENNReal.toReal_natCast,
+      ENNReal.toReal_natCast, h₁, h₂]
     · have h₄ : (p + 1 : ℝ) + (q + 1 : ℝ) ≠ (0 : ℝ) := by
         apply ne_of_gt
         assumption_mod_cast
@@ -355,8 +355,8 @@ theorem ballot_problem :
     (uniformOn (countedSequence p q) staysPositive).toReal =
       ((p - q) / (p + q) : ℝ≥0∞).toReal := by
     rw [ballot_problem' q p qp]
-    rw [ENNReal.toReal_div, ← Nat.cast_add, ← Nat.cast_add, ENNReal.toReal_nat,
-      ENNReal.toReal_sub_of_le, ENNReal.toReal_nat, ENNReal.toReal_nat]
+    rw [ENNReal.toReal_div, ← Nat.cast_add, ← Nat.cast_add, ENNReal.toReal_natCast,
+      ENNReal.toReal_sub_of_le, ENNReal.toReal_natCast, ENNReal.toReal_natCast]
     exacts [Nat.cast_le.2 qp.le, ENNReal.natCast_ne_top _]
   rwa [ENNReal.toReal_eq_toReal (measure_lt_top _ _).ne] at this
   simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le,

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -334,7 +334,7 @@ include hG in
 theorem friendship_theorem [Nonempty V] : ExistsPolitician G := by
   by_contra npG
   rcases hG.isRegularOf_not_existsPolitician npG with ⟨d, dreg⟩
-  cases' lt_or_le d 3 with dle2 dge3
+  rcases lt_or_le d 3 with dle2 | dge3
   · exact npG (hG.existsPolitician_of_degree_le_two dreg (Nat.lt_succ_iff.mp dle2))
   · exact hG.false_of_three_le_degree dreg dge3
 

Archive/Wiedijk100Theorems/HeronsFormula.lean

@@ -34,7 +34,7 @@ variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V
   `√(s * (s - a) * (s - b) * (s - c))` where `s = (a + b + c) / 2` is the semiperimeter.
   We show this by equating this formula to `a * b * sin γ`, where `γ` is the angle opposite
   the side `c`.
- -/
+-/
 theorem heron {p₁ p₂ p₃ : P} (h1 : p₁ ≠ p₂) (h2 : p₃ ≠ p₂) :
     let a := dist p₁ p₂
     let b := dist p₃ p₂
@@ -54,7 +54,7 @@ theorem heron {p₁ p₂ p₃ : P} (h1 : p₁ ≠ p₂) (h2 : p₃ ≠ p₂) :
   have numerator_nonneg : 0 ≤ numerator := by
     have frac_nonneg : 0 ≤ numerator / denominator :=
       (sub_nonneg.mpr (cos_sq_le_one γ)).trans_eq split_to_frac
-    cases' div_nonneg_iff.mp frac_nonneg with h h
+    rcases div_nonneg_iff.mp frac_nonneg with h | h
     · exact h.left
     · simpa [numerator, denominator, a, b, c, h1, h2] using le_antisymm h.right (sq_nonneg _)
   have ab2_nonneg : 0 ≤ 2 * a * b := by positivity

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -56,7 +56,7 @@ theorem even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).Pr
 
 theorem eq_two_pow_mul_odd {n : ℕ} (hpos : 0 < n) : ∃ k m : ℕ, n = 2 ^ k * m ∧ ¬Even m := by
   have h := Nat.finiteMultiplicity_iff.2 ⟨Nat.prime_two.ne_one, hpos⟩
-  cases' pow_multiplicity_dvd 2 n with m hm
+  obtain ⟨m, hm⟩ := pow_multiplicity_dvd 2 n
   use multiplicity 2 n, m
   refine ⟨hm, ?_⟩
   rw [even_iff_two_dvd]

Archive/ZagierTwoSquares.lean

@@ -47,7 +47,7 @@ lemma zagierSet_lower_bound {x y z : ℕ} (h : (x, y, z) ∈ zagierSet k) : 0 <
   · apply_fun (· % 4) at h
     simp [mul_assoc, Nat.add_mod] at h
   all_goals
-    cases' (Nat.dvd_prime hk.out).1 (dvd_of_mul_left_eq _ h) with e e
+    rcases (Nat.dvd_prime hk.out).1 (dvd_of_mul_left_eq _ h) with e | e
     all_goals
       simp only [e, self_eq_add_left, ne_eq, add_eq_zero, and_false, not_false_eq_true,
         mul_eq_left₀, reduceCtorEq] at h
@@ -158,7 +158,7 @@ theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (comple
     replace mem := (mul_left_cancel₀ two_ne_zero mem).symm
     subst mem
     rw [show x * x + 4 * x * z = x * (x + 4 * z) by linarith] at h
-    cases' (Nat.dvd_prime hk.out).1 (dvd_of_mul_left_eq _ h) with e e
+    rcases (Nat.dvd_prime hk.out).1 (dvd_of_mul_left_eq _ h) with e | e
     · rw [e, mul_one] at h
       simp_all [h, show z = 0 by linarith [e]]
     · simp only [e, mul_left_eq_self₀, add_eq_zero, and_false, or_false, reduceCtorEq] at h

Cache/Hashing.lean

@@ -109,7 +109,7 @@ partial def getHash (filePath : FilePath) (visited : Std.HashSet FilePath := ∅
   match (← get).cache[filePath]? with
   | some hash? => return hash?
   | none =>
-    let fixedPath := (← IO.getPackageDir filePath) / filePath
+    let fixedPath := (← IO.getSrcDir filePath) / filePath
     if !(← fixedPath.pathExists) then
       IO.println s!"Warning: {fixedPath} not found. Skipping all files that depend on it."
       if fixedPath.extension != "lean" then

Cache/IO.lean

@@ -133,12 +133,26 @@ end
 
 def getPackageDirs : CacheM PackageDirs := return (← read).packageDirs
 
-def getPackageDir (path : FilePath) : CacheM FilePath := do
-  match path.withExtension "" |>.components.head? with
-  | none => throw <| IO.userError "Can't find package directory for empty path"
-  | some pkg => match (← getPackageDirs).find? pkg with
-    | none => throw <| IO.userError s!"Unknown package directory for {pkg}"
-    | some path => return path
+/--
+`path` is assumed to be the unresolved file path corresponding to a module:
+For `Mathlib.Init` this would be `Mathlib/Init.lean`.
+
+Find the source directory for `path`.
+This corresponds to the folder where the `.lean` files are located, i.e. for `Mathlib.Init`,
+the file should be located at `(← getSrcDir _) / "Mathlib" / "Init.lean`.
+
+Usually it is either `.` or something like `./.lake/packages/mathlib/`
+-/
+def getSrcDir (path : FilePath) : CacheM FilePath := do
+  let sp := (← read).srcSearchPath
+
+  -- `path` is a unresolved file name like `Aesop/Build.lean`
+  let mod : Name := .fromComponents <| path.withExtension "" |>.components.map Name.mkSimple
+
+  let .some srcDir ← sp.findWithExtBase "lean" mod |
+    throw <| IO.userError s!"Unknown package directory for {mod}\nsearch paths: {sp}"
+
+  return srcDir
 
 /-- Runs a terminal command and retrieves its output, passing the lines to `processLine` -/
 partial def runCurlStreaming (args : Array String) (init : α)
@@ -269,7 +283,21 @@ Given a path to a Lean file, concatenates the paths to its build files.
 Each build file also has a `Bool` indicating whether that file is required for caching to proceed.
 -/
 def mkBuildPaths (path : FilePath) : CacheM <| List (FilePath × Bool) := do
-  let packageDir ← getPackageDir path
+  /-
+  TODO: if `srcDir` or other custom lake layout options are set in the `lean_lib`,
+  `packageSrcDir / LIBDIR` might be the wrong path!
+
+  See [Lake documentation](https://github.com/leanprover/lean4/tree/master/src/lake#layout)
+  for available options.
+
+  If a dependency is added to mathlib which uses such a custom layout, `mkBuildPaths`
+  needs to be adjusted!
+  -/
+  let packageDir ← getSrcDir path
+  if !(← (packageDir / ".lake").isDir) then
+    IO.eprintln <| s!"Warning: {packageDir / ".lake"} seems not to exist, most likely `cache` \
+      will not work as expected!"
+
   return [
     -- Note that `packCache` below requires that the `.trace` file is first in this list.
     (packageDir / LIBDIR / path.withExtension "trace", true),

Cache/Lean.lean

@@ -27,6 +27,34 @@ def Nat.toHexDigits (n : Nat) : Nat → (res : String := "") → String
 def UInt64.asLTar (n : UInt64) : String :=
   s!"{Nat.toHexDigits n.toNat 8}.ltar"
 
+-- copied from Mathlib
+/-- Create a `Name` from a list of components. -/
+def Lean.Name.fromComponents : List Name → Name := go .anonymous where
+  go : Name → List Name → Name
+  | n, []        => n
+  | n, s :: rest => go (s.updatePrefix n) rest
+
+namespace Lean.SearchPath
+
+open System in
+
+/--
+Find the source directory for a module. This could be `.`
+(or in fact also something uncleaned like `./././.`) if the
+module is part of the current package, or something like `.lake/packages/mathlib` if the
+module is from a dependency.
+
+This is an exact copy of the first part of `Lean.SearchPath.findWithExt` which, in turn,
+is used by `Lean.findLean sp mod`. In the future, `findWithExt` could be refactored to
+expose this base path.
+-/
+def findWithExtBase (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do
+  let pkg := mod.getRoot.toString (escape := false)
+  sp.findM? fun p =>
+    (p / pkg).isDir <||> ((p / pkg).addExtension ext).pathExists
+
+end Lean.SearchPath
+
 namespace System.FilePath
 
 /-- Removes a parent path from the beginning of a path -/

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -134,7 +134,7 @@ theorem αβγ_ne_zero : α * β * γ ≠ 0 := fun h =>
 /-- The 1-form on $K^3$, the kernel of which we will take a quotient by.
 
 Our source uses $αx - βy - γz$, though since this is characteristic two we just use $αx + βy + γz$.
- -/
+-/
 @[simps!]
 def lFunc : (Fin 3 → K) →ₗ[K] K :=
   letI proj : Fin 3 → (Fin 3 → K) →ₗ[K] K := LinearMap.proj