Commit 2024-11-11 03:26 0962f38e

feat(Data/List): lemmas about ofFn (#18593) Add several lemmas that proved convenient in working with List.ofFn. There were two places where avoiding extra imports was awkward. In the proof of head_ofFn, I wanted to rewrite with head_eq_getElem_zero, but Mathlib.Data.List.Basic isn't imported in Mathlib.Data.List.OfFn so I inlined an equivalent rewrite on ← getElem_zero (length_ofFn _ ▸ Nat.pos_of_ne_zero hn) instead. chain'_ofFn depends on content from both Mathlib.Data.List.OfFn and Mathlib.Data.List.Chain, but neither of those imports the other. So to avoid adding extra imports or awkward local duplication of proofs, I created a new Mathlib.Data.List.ChainOfFn to have that one lemma. Alternative suggestions for avoiding import creep for these lemmas are welcome. Golfing is also welcome; the proof of find?_ofFn_eq_some is rather long.