Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.list.of_fn
! leanprover-community/mathlib commit bf27744463e9620ca4e4ebe951fe83530ae6949b
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fin.Tuple.Basic
import Mathlib.Data.List.Join
import Mathlib.Data.List.Pairwise

/-!
# Lists from functions

Theorems and lemmas for dealing with `List.ofFn`, which converts a function on `Fin n` to a list
of length `n`.

## Main Statements

The main statements pertain to lists generated using `List.ofFn`

- `List.length_ofFn`, which tells us the length of such a list
- `List.get?_ofFn`, which tells us the nth element of such a list
- `List.equivSigmaTuple`, which is an `Equiv` between lists and the functions that generate them
via `List.ofFn`.
-/

universe u

variable {α: Type uα : Type u: Type (u+1)Type u}

open Nat

namespace List

#noalign list.length_of_fn_aux

/-- The length of a list converted from a function is the size of the domain. -/
@[simp]
theorem length_ofFn: ∀ {n : ℕ} (f : Fin n → α), length (ofFn f) = nlength_ofFn {n: ℕn} (f: Fin n → αf : Fin: ℕ → TypeFin n: ?m.6n → α: Type uα) : length: {α : Type ?u.14} → List α → ℕlength (ofFn: {α : Type ?u.16} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf) = n: ?m.6n := byGoals accomplished! 🐙
α: Type un: ℕf: Fin n → αlength (ofFn f) = nsimp [ofFn: {α : Type ?u.31} → {n : ℕ} → (Fin n → α) → List αofFn]Goals accomplished! 🐙
#align list.length_of_fn List.length_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α), length (ofFn f) = nList.length_ofFn

#noalign list.nth_of_fn_aux

--Porting note: new theorem
@[simp]
theorem get_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin (length (ofFn f))),
get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)get_ofFn {n: ℕn} (f: Fin n → αf : Fin: ℕ → TypeFin n: ?m.118n → α: Type uα) (i: Fin (length (ofFn f))i) : get: {α : Type ?u.129} → (as : List α) → Fin (length as) → αget (ofFn: {α : Type ?u.131} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf) i: ?m.125i = f: Fin n → αf (Fin.cast: {n m : ℕ} → n = m → Fin n ≃o Fin mFin.cast (byGoals accomplished! 🐙 α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))length (ofFn f) = nsimpGoals accomplished! 🐙) i: ?m.125i) := byGoals accomplished! 🐙
α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)have := Array.getElem_ofFn: ∀ {n : ℕ} {α : Type ?u.258} (f : Fin n → α) (i : ℕ) (h : i < Array.size (Array.ofFn f)),
(Array.ofFn f)[i] = f { val := i, isLt := (_ : i < n) }Array.getElem_ofFn f: Fin n → αf i: Fin (length (ofFn f))i (α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)byGoals accomplished! 🐙 α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))↑i < Array.size (Array.ofFn f)simpa using i: Fin (length (ofFn f))i.2: ∀ {n : ℕ} (self : Fin n), ↑self < n2Goals accomplished! 🐙)α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))this: (Array.ofFn f)[↑i] = f { val := ↑i, isLt := (_ : ↑i < n) }get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)cases' i: Fin (length (ofFn f))i with i: ℕi hi: i < ?m.1373hiα: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: (Array.ofFn f)[↑{ val := i, isLt := hi }] =   f { val := ↑{ val := i, isLt := hi }, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mkget (ofFn f) { val := i, isLt := hi } = f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := hi })
α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)simp only [getElem: {cont : Type ?u.1418} →
{idx : Type ?u.1417} →
{elem : outParam (Type ?u.1416)} →
{dom : outParam (cont → idx → Prop)} →
[self : GetElem cont idx elem dom] → (xs : cont) → (i : idx) → dom xs i → elemgetElem, Array.get: {α : Type ?u.1430} → (a : Array α) → Fin (Array.size a) → αArray.get] at this: (Array.ofFn f)[↑{ val := i, isLt := hi }] =   f { val := ↑{ val := i, isLt := hi }, isLt := (_ : ↑{ val := i, isLt := hi } < n) }thisα: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mkget (ofFn f) { val := i, isLt := hi } = f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := hi })
α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)simp only [Fin.cast_mk: ∀ {n m : ℕ} (h : n = m) (i : ℕ) (hn : i < n), ↑(Fin.cast h) { val := i, isLt := hn } = { val := i, isLt := (_ : i < m) }Fin.cast_mk]α: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mkget (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := (_ : i < n) }
α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)rw [α: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mkget (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := (_ : i < n) }← this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }thisα: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mkget (ofFn f) { val := i, isLt := hi } =   get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }]α: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mkget (ofFn f) { val := i, isLt := hi } =   get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }
α: Type un: ℕf: Fin n → αi: Fin (length (ofFn f))get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)congrα: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mk.h.e_2.hofFn f = (Array.ofFn f).dataα: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mk.h.e_3.e_1.e_aofFn f = (Array.ofFn f).dataα: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mk.h.e_3.e_3HEq hi (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) α: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mkget (ofFn f) { val := i, isLt := hi } =   get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }<;>α: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mk.h.e_2.hofFn f = (Array.ofFn f).dataα: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mk.h.e_3.e_1.e_aofFn f = (Array.ofFn f).dataα: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mk.h.e_3.e_3HEq hi (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) α: Type un: ℕf: Fin n → αi: ℕhi: i < length (ofFn f)this: get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =   f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }mkget (ofFn f) { val := i, isLt := hi } =   get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }simp [ofFn: {α : Type ?u.12801} → {n : ℕ} → (Fin n → α) → List αofFn]Goals accomplished! 🐙

/-- The `n`th element of a list -/
@[simp]
theorem get?_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : ℕ), get? (ofFn f) i = ofFnNthVal f iget?_ofFn {n: ?m.13674n} (f: Fin n → αf : Fin: ℕ → TypeFin n: ?m.13674n → α: Type uα) (i: ℕi) : get?: {α : Type ?u.13685} → List α → ℕ → Option αget? (ofFn: {α : Type ?u.13687} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf) i: ?m.13681i = ofFnNthVal: {α : Type ?u.13696} → {n : ℕ} → (Fin n → α) → ℕ → Option αofFnNthVal f: Fin n → αf i: ?m.13681i :=
if h: ?m.13747h : i: ℕi < (ofFn: {α : Type ?u.13709} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf).length: {α : Type ?u.13715} → List α → ℕlength
then byGoals accomplished! 🐙
α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f irw [α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f iget?_eq_get: ∀ {α : Type ?u.13756} {l : List α} {n : ℕ} (h : n < length l), get? l n = some (get l { val := n, isLt := h })get?_eq_get h: i < length (ofFn f)h,α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)some (get (ofFn f) { val := i, isLt := h }) = ofFnNthVal f i α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f iget_ofFn: ∀ {α : Type ?u.13769} {n : ℕ} (f : Fin n → α) (i : Fin (length (ofFn f))),
get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)get_ofFnα: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i]α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i
α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f i.α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f isimp at h: i < length (ofFn f)hα: Type un: ℕf: Fin n → αi: ℕh✝: i < length (ofFn f)h: i < nsome (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h✝ })) = ofFnNthVal f i;α: Type un: ℕf: Fin n → αi: ℕh✝: i < length (ofFn f)h: i < nsome (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h✝ })) = ofFnNthVal f i α: Type un: ℕf: Fin n → αi: ℕh: i < length (ofFn f)some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f isimp [ofFnNthVal: {α : Type ?u.13960} → {n : ℕ} → (Fin n → α) → ℕ → Option αofFnNthVal, h: i < nh]Goals accomplished! 🐙
else byGoals accomplished! 🐙
α: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f irw [α: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f iofFnNthVal: {α : Type ?u.14483} → {n : ℕ} → (Fin n → α) → ℕ → Option αofFnNthVal,α: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = if h : i < n then some (f { val := i, isLt := h }) else none α: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f idif_neg: ∀ {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort ?u.14484} {t : c → α} {e : ¬c → α}, dite c t e = e hncdif_negα: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = noneα: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)hnc¬i < n]α: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = noneα: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)hnc¬i < n α: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f i<;>α: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = noneα: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)hnc¬i < n
α: Type un: ℕf: Fin n → αi: ℕh: ¬i < length (ofFn f)get? (ofFn f) i = ofFnNthVal f isimpa using h: ¬i < length (ofFn f)hGoals accomplished! 🐙
#align list.nth_of_fn List.get?_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : ℕ), get? (ofFn f) i = ofFnNthVal f iList.get?_ofFn

set_option linter.deprecated false in
@[deprecated get_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin (length (ofFn f))),
get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)get_ofFn]
theorem nthLe_ofFn: ∀ {n : ℕ} (f : Fin n → α) (i : Fin n), nthLe (ofFn f) ↑i (_ : ↑i < length (ofFn f)) = f inthLe_ofFn {n: ?m.17429n} (f: Fin n → αf : Fin: ℕ → TypeFin n: ?m.17429n → α: Type uα) (i: Fin ni : Fin: ℕ → TypeFin n: ?m.17429n) :
nthLe: {α : Type ?u.17439} → (l : List α) → (n : ℕ) → n < length l → αnthLe (ofFn: {α : Type ?u.17441} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf) i: Fin ni ((length_ofFn: ∀ {α : Type ?u.17554} {n : ℕ} (f : Fin n → α), length (ofFn f) = nlength_ofFn f: Fin n → αf).symm: ∀ {α : Sort ?u.17560} {a b : α}, a = b → b = asymm ▸ i: Fin ni.2: ∀ {n : ℕ} (self : Fin n), ↑self < n2) = f: Fin n → αf i: Fin ni := byGoals accomplished! 🐙
α: Type un: ℕf: Fin n → αi: Fin nnthLe (ofFn f) ↑i (_ : ↑i < length (ofFn f)) = f isimp [nthLe: {α : Type ?u.17585} → (l : List α) → (n : ℕ) → n < length l → αnthLe]Goals accomplished! 🐙
#align list.nth_le_of_fn List.nthLe_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin n), nthLe (ofFn f) ↑i (_ : ↑i < length (ofFn f)) = f iList.nthLe_ofFn

set_option linter.deprecated false in
@[simp, deprecated get_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin (length (ofFn f))),
get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)get_ofFn]
theorem nthLe_ofFn': ∀ {α : Type u} {n : ℕ} (f : Fin n → α) {i : ℕ} (h : i < length (ofFn f)),
nthLe (ofFn f) i h = f { val := i, isLt := (_ : i < n) }nthLe_ofFn' {n: ?m.18338n} (f: Fin n → αf : Fin: ℕ → TypeFin n: ?m.18338n → α: Type uα) {i: ℕi : ℕ: Typeℕ} (h: i < length (ofFn f)h : i: ℕi < (ofFn: {α : Type ?u.18348} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf).length: {α : Type ?u.18355} → List α → ℕlength) :
nthLe: {α : Type ?u.18368} → (l : List α) → (n : ℕ) → n < length l → αnthLe (ofFn: {α : Type ?u.18370} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf) i: ℕi h: i < length (ofFn f)h = f: Fin n → αf ⟨i: ℕi, length_ofFn: ∀ {α : Type ?u.18381} {n : ℕ} (f : Fin n → α), length (ofFn f) = nlength_ofFn f: Fin n → αf ▸ h: i < length (ofFn f)h⟩ :=
nthLe_ofFn: ∀ {α : Type ?u.18399} {n : ℕ} (f : Fin n → α) (i : Fin n), nthLe (ofFn f) ↑i (_ : ↑i < length (ofFn f)) = f inthLe_ofFn f: Fin n → αf ⟨i: ℕi, length_ofFn: ∀ {α : Type ?u.18409} {n : ℕ} (f : Fin n → α), length (ofFn f) = nlength_ofFn f: Fin n → αf ▸ h: i < length (ofFn f)h⟩
#align list.nth_le_of_fn' List.nthLe_ofFn': ∀ {α : Type u} {n : ℕ} (f : Fin n → α) {i : ℕ} (h : i < length (ofFn f)),
nthLe (ofFn f) i h = f { val := i, isLt := (_ : i < n) }List.nthLe_ofFn'

@[simp]
theorem map_ofFn: ∀ {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β), map g (ofFn f) = ofFn (g ∘ f)map_ofFn {β: Type u_1β : Type _: Type (?u.18457+1)Type _} {n: ℕn : ℕ: Typeℕ} (f: Fin n → αf : Fin: ℕ → TypeFin n: ℕn → α: Type uα) (g: α → βg : α: Type uα → β: Type ?u.18457β) :
map: {α : Type ?u.18472} → {β : Type ?u.18471} → (α → β) → List α → List βmap g: α → βg (ofFn: {α : Type ?u.18478} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf) = ofFn: {α : Type ?u.18486} → {n : ℕ} → (Fin n → α) → List αofFn (g: α → βg ∘ f: Fin n → αf) :=
ext_get: ∀ {α : Type ?u.18513} {l₁ l₂ : List α},
length l₁ = length l₂ →
(∀ (n : ℕ) (h₁ : n < length l₁) (h₂ : n < length l₂),
get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }) →
l₁ = l₂ext_get (byGoals accomplished! 🐙 α: Type uβ: Type u_1n: ℕf: Fin n → αg: α → βlength (map g (ofFn f)) = length (ofFn (g ∘ f))simpGoals accomplished! 🐙) fun i: ?m.18523i h: ?m.18526h h': ?m.18529h' => byGoals accomplished! 🐙 α: Type uβ: Type u_1n: ℕf: Fin n → αg: α → βi: ℕh: i < length (map g (ofFn f))h': i < length (ofFn (g ∘ f))get (map g (ofFn f)) { val := i, isLt := h } = get (ofFn (g ∘ f)) { val := i, isLt := h' }simpGoals accomplished! 🐙
#align list.map_of_fn List.map_ofFn: ∀ {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β), map g (ofFn f) = ofFn (g ∘ f)List.map_ofFn

--Porting note: we don't have Array' in mathlib4
-- /-- Arrays converted to lists are the same as `of_fn` on the indexing function of the array. -/
-- theorem array_eq_of_fn {n} (a : Array' n α) : a.toList = ofFn a.read :=
--   by
--   suffices ∀ {m h l}, DArray.revIterateAux a (fun i => cons) m h l =
--      ofFnAux (DArray.read a) m h l
--     from this
--   intros ; induction' m with m IH generalizing l; · rfl
--   simp only [DArray.revIterateAux, of_fn_aux, IH]
-- #align list.array_eq_of_fn List.array_eq_of_fn

@[congr]
theorem ofFn_congr: ∀ {α : Type u} {m n : ℕ} (h : m = n) (f : Fin m → α), ofFn f = ofFn fun i => f (↑(Fin.cast (_ : n = m)) i)ofFn_congr {m: ℕm n: ℕn : ℕ: Typeℕ} (h: m = nh : m: ℕm = n: ℕn) (f: Fin m → αf : Fin: ℕ → TypeFin m: ℕm → α: Type uα) :
ofFn: {α : Type ?u.20523} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin m → αf = ofFn: {α : Type ?u.20530} → {n : ℕ} → (Fin n → α) → List αofFn fun i: Fin ni : Fin: ℕ → TypeFin n: ℕn => f: Fin m → αf (Fin.cast: {n m : ℕ} → n = m → Fin n ≃o Fin mFin.cast h: m = nh.symm: ∀ {α : Sort ?u.20537} {a b : α}, a = b → b = asymm i: Fin ni) := byGoals accomplished! 🐙
α: Type um, n: ℕh: m = nf: Fin m → αofFn f = ofFn fun i => f (↑(Fin.cast (_ : n = m)) i)subst h: m = nhα: Type um: ℕf: Fin m → αofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)
α: Type um, n: ℕh: m = nf: Fin m → αofFn f = ofFn fun i => f (↑(Fin.cast (_ : n = m)) i)simp_rw [α: Type um: ℕf: Fin m → αofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)Fin.cast_refl: ∀ {n : ℕ} (h : optParam (n = n) (_ : n = n)), Fin.cast h = OrderIso.refl (Fin n)Fin.cast_refl,α: Type um: ℕf: Fin m → αofFn f = ofFn fun i => f (↑(OrderIso.refl (Fin m)) i) α: Type um: ℕf: Fin m → αofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)OrderIso.refl_applyGoals accomplished! 🐙]Goals accomplished! 🐙
#align list.of_fn_congr List.ofFn_congr: ∀ {α : Type u} {m n : ℕ} (h : m = n) (f : Fin m → α), ofFn f = ofFn fun i => f (↑(Fin.cast (_ : n = m)) i)List.ofFn_congr

/-- `ofFn` on an empty domain is the empty list. -/
@[simp]
theorem ofFn_zero: ∀ {α : Type u} (f : Fin 0 → α), ofFn f = []ofFn_zero (f: Fin 0 → αf : Fin: ℕ → TypeFin 0: ?m.210200 → α: Type uα) : ofFn: {α : Type ?u.21034} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin 0 → αf = []: List ?m.21042[] :=
rfl: ∀ {α : Sort ?u.21074} {a : α}, a = arfl
#align list.of_fn_zero List.ofFn_zero: ∀ {α : Type u} (f : Fin 0 → α), ofFn f = []List.ofFn_zero

@[simp]
theorem ofFn_succ: ∀ {α : Type u} {n : ℕ} (f : Fin (succ n) → α), ofFn f = f 0 :: ofFn fun i => f (Fin.succ i)ofFn_succ {n: ?m.21225n} (f: Fin (succ n) → αf : Fin: ℕ → TypeFin (succ: ℕ → ℕsucc n: ?m.21225n) → α: Type uα) : ofFn: {α : Type ?u.21233} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin (succ n) → αf = f: Fin (succ n) → αf 0: ?m.212430 :: ofFn: {α : Type ?u.21271} → {n : ℕ} → (Fin n → α) → List αofFn fun i: ?m.21276i => f: Fin (succ n) → αf i: ?m.21276i.succ: {n : ℕ} → Fin n → Fin (succ n)succ :=
ext_get: ∀ {α : Type ?u.21288} {l₁ l₂ : List α},
length l₁ = length l₂ →
(∀ (n : ℕ) (h₁ : n < length l₁) (h₂ : n < length l₂),
get l₁ { val := n, isLt := h₁ } = get l₂ { val := n, isLt := h₂ }) →
l₁ = l₂ext_get (byGoals accomplished! 🐙 α: Type un: ℕf: Fin (succ n) → αlength (ofFn f) = length (f 0 :: ofFn fun i => f (Fin.succ i))simpGoals accomplished! 🐙) (fun i: ?m.21298i hi₁: ?m.21301hi₁ hi₂: ?m.21304hi₂ => byGoals accomplished! 🐙
α: Type un: ℕf: Fin (succ n) → αi: ℕhi₁: i < length (ofFn f)hi₂: i < length (f 0 :: ofFn fun i => f (Fin.succ i))get (ofFn f) { val := i, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := i, isLt := hi₂ }cases i: ℕiα: Type un: ℕf: Fin (succ n) → αhi₁: zero < length (ofFn f)hi₂: zero < length (f 0 :: ofFn fun i => f (Fin.succ i))zeroget (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }α: Type un: ℕf: Fin (succ n) → αn✝: ℕhi₁: succ n✝ < length (ofFn f)hi₂: succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))succget (ofFn f) { val := succ n✝, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
α: Type un: ℕf: Fin (succ n) → αi: ℕhi₁: i < length (ofFn f)hi₂: i < length (f 0 :: ofFn fun i => f (Fin.succ i))get (ofFn f) { val := i, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := i, isLt := hi₂ }.α: Type un: ℕf: Fin (succ n) → αhi₁: zero < length (ofFn f)hi₂: zero < length (f 0 :: ofFn fun i => f (Fin.succ i))zeroget (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ } α: Type un: ℕf: Fin (succ n) → αhi₁: zero < length (ofFn f)hi₂: zero < length (f 0 :: ofFn fun i => f (Fin.succ i))zeroget (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }α: Type un: ℕf: Fin (succ n) → αn✝: ℕhi₁: succ n✝ < length (ofFn f)hi₂: succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))succget (ofFn f) { val := succ n✝, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }simpGoals accomplished! 🐙
α: Type un: ℕf: Fin (succ n) → αi: ℕhi₁: i < length (ofFn f)hi₂: i < length (f 0 :: ofFn fun i => f (Fin.succ i))get (ofFn f) { val := i, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := i, isLt := hi₂ }.α: Type un: ℕf: Fin (succ n) → αn✝: ℕhi₁: succ n✝ < length (ofFn f)hi₂: succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))succget (ofFn f) { val := succ n✝, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ } α: Type un: ℕf: Fin (succ n) → αn✝: ℕhi₁: succ n✝ < length (ofFn f)hi₂: succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))succget (ofFn f) { val := succ n✝, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }simpGoals accomplished! 🐙)
#align list.of_fn_succ List.ofFn_succ: ∀ {α : Type u} {n : ℕ} (f : Fin (succ n) → α), ofFn f = f 0 :: ofFn fun i => f (Fin.succ i)List.ofFn_succ

theorem ofFn_succ': ∀ {n : ℕ} (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))ofFn_succ' {n: ℕn} (f: Fin (succ n) → αf : Fin: ℕ → TypeFin (succ: ℕ → ℕsucc n: ?m.25515n) → α: Type uα) :
ofFn: {α : Type ?u.25523} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin (succ n) → αf = (ofFn: {α : Type ?u.25530} → {n : ℕ} → (Fin n → α) → List αofFn fun i: ?m.25534i => f: Fin (succ n) → αf (Fin.castSucc: {n : ℕ} → Fin n ↪o Fin (n + 1)Fin.castSucc i: ?m.25534i)).concat: {α : Type ?u.25716} → List α → α → List αconcat (f: Fin (succ n) → αf (Fin.last: (n : ℕ) → Fin (n + 1)Fin.last _: ℕ_)) := byGoals accomplished! 🐙
α: Type un: ℕf: Fin (succ n) → αofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))induction' n: ℕn with n: ℕn IH: ?m.25742 nIHα: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type un: ℕf: Fin (succ n) → αofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))·α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero)) α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))rw [α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))ofFn_zero: ∀ {α : Type ?u.25759} (f : Fin 0 → α), ofFn f = []ofFn_zero,α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat [] (f (Fin.last zero)) α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))concat_nil: ∀ {α : Type ?u.25794} (a : α), concat [] a = [a]concat_nil,α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = [f (Fin.last zero)] α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))ofFn_succ: ∀ {α : Type ?u.25805} {n : ℕ} (f : Fin (succ n) → α), ofFn f = f 0 :: ofFn fun i => f (Fin.succ i)ofFn_succ,α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzero(f 0 :: ofFn fun i => f (Fin.succ i)) = [f (Fin.last zero)] α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))ofFn_zero: ∀ {α : Type ?u.25814} (f : Fin 0 → α), ofFn f = []ofFn_zeroα: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzero[f 0] = [f (Fin.last zero)]]α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzero[f 0] = [f (Fin.last zero)]
α: Type un: ℕf✝: Fin (succ n) → αf: Fin (succ zero) → αzeroofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))rflGoals accomplished! 🐙
α: Type un: ℕf: Fin (succ n) → αofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))·α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n))) α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))rw [α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))ofFn_succ: ∀ {α : Type ?u.25861} {n : ℕ} (f : Fin (succ n) → α), ofFn f = f 0 :: ofFn fun i => f (Fin.succ i)ofFn_succ,α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsucc(f 0 :: ofFn fun i => f (Fin.succ i)) = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n))) α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))IH: ?m.25742 nIH,α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccf 0 :: concat (ofFn fun i => f (Fin.succ (↑Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =   concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n))) α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))ofFn_succ: ∀ {α : Type ?u.25928} {n : ℕ} (f : Fin (succ n) → α), ofFn f = f 0 :: ofFn fun i => f (Fin.succ i)ofFn_succ,α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccf 0 :: concat (ofFn fun i => f (Fin.succ (↑Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =   concat (f (↑Fin.castSucc 0) :: ofFn fun i => f (↑Fin.castSucc (Fin.succ i))) (f (Fin.last (succ n))) α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))concat_cons: ∀ {α : Type ?u.25961} (a b : α) (l : List α), concat (a :: l) b = a :: concat l bconcat_cons,α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccf 0 :: concat (ofFn fun i => f (Fin.succ (↑Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =   f (↑Fin.castSucc 0) :: concat (ofFn fun i => f (↑Fin.castSucc (Fin.succ i))) (f (Fin.last (succ n))) α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))Fin.castSucc_zero: ∀ {n : ℕ} [inst : NeZero n], ↑Fin.castSucc 0 = 0Fin.castSucc_zeroα: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccf 0 :: concat (ofFn fun i => f (Fin.succ (↑Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =   f 0 :: concat (ofFn fun i => f (↑Fin.castSucc (Fin.succ i))) (f (Fin.last (succ n)))]α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccf 0 :: concat (ofFn fun i => f (Fin.succ (↑Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =   f 0 :: concat (ofFn fun i => f (↑Fin.castSucc (Fin.succ i))) (f (Fin.last (succ n)))
α: Type un✝: ℕf✝: Fin (succ n✝) → αn: ℕIH: ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))f: Fin (succ (succ n)) → αsuccofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))congrGoals accomplished! 🐙
#align list.of_fn_succ' List.ofFn_succ': ∀ {α : Type u} {n : ℕ} (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))List.ofFn_succ'

@[simp]
theorem ofFn_eq_nil_iff: ∀ {α : Type u} {n : ℕ} {f : Fin n → α}, ofFn f = [] ↔ n = 0ofFn_eq_nil_iff {n: ℕn : ℕ: Typeℕ} {f: Fin n → αf : Fin: ℕ → TypeFin n: ℕn → α: Type uα} : ofFn: {α : Type ?u.26680} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf = []: List ?m.26688[] ↔ n: ℕn = 0: ?m.267200 := byGoals accomplished! 🐙
α: Type un: ℕf: Fin n → αofFn f = [] ↔ n = 0cases n: ℕnα: Type uf: Fin zero → αzeroofFn f = [] ↔ zero = 0α: Type un✝: ℕf: Fin (succ n✝) → αsuccofFn f = [] ↔ succ n✝ = 0 α: Type un: ℕf: Fin n → αofFn f = [] ↔ n = 0<;>α: Type uf: Fin zero → αzeroofFn f = [] ↔ zero = 0α: Type un✝: ℕf: Fin (succ n✝) → αsuccofFn f = [] ↔ succ n✝ = 0 α: Type un: ℕf: Fin n → αofFn f = [] ↔ n = 0simp only [ofFn_zero: ∀ {α : Type ?u.26948} (f : Fin 0 → α), ofFn f = []ofFn_zero, ofFn_succ: ∀ {α : Type ?u.26827} {n : ℕ} (f : Fin (succ n) → α), ofFn f = f 0 :: ofFn fun i => f (Fin.succ i)ofFn_succ, eq_self_iff_true: ∀ {α : Sort ?u.26835} (a : α), a = a ↔ Trueeq_self_iff_true, Nat.succ_ne_zero: ∀ (n : ℕ), succ n ≠ 0Nat.succ_ne_zero]Goals accomplished! 🐙
#align list.of_fn_eq_nil_iff List.ofFn_eq_nil_iff: ∀ {α : Type u} {n : ℕ} {f : Fin n → α}, ofFn f = [] ↔ n = 0List.ofFn_eq_nil_iff

theorem last_ofFn: ∀ {n : ℕ} (f : Fin n → α) (h : ofFn f ≠ []) (hn : optParam (n - 1 < n) (_ : pred (Nat.sub n 0) < Nat.sub n 0)),
getLast (ofFn f) h = f { val := n - 1, isLt := hn }last_ofFn {n: ℕn : ℕ: Typeℕ} (f: Fin n → αf : Fin: ℕ → TypeFin n: ℕn → α: Type uα) (h: ofFn f ≠ []h : ofFn: {α : Type ?u.27149} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf ≠ []: List ?m.27158[])
(hn: optParam (n - 1 < n) (_ : pred (Nat.sub n 0) < Nat.sub n 0)hn : n: ℕn - 1: ?m.271671 < n: ℕn := Nat.pred_lt: ∀ {n : ℕ}, n ≠ 0 → pred n < nNat.pred_lt <| ofFn_eq_nil_iff: ∀ {α : Type ?u.27282} {n : ℕ} {f : Fin n → α}, ofFn f = [] ↔ n = 0ofFn_eq_nil_iff.not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not.mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp h: ofFn f ≠ []h) :
getLast: {α : Type ?u.27380} → (as : List α) → as ≠ [] → αgetLast (ofFn: {α : Type ?u.27382} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf) h: ofFn f ≠ []h = f: Fin n → αf ⟨n: ℕn - 1: ?m.274011, hn: optParam (n - 1 < n) (_ : pred ?m.27239 < ?m.27239)hn⟩ := byGoals accomplished! 🐙 α: Type un: ℕf: Fin n → αh: ofFn f ≠ []hn: optParam (n - 1 < n) (_ : pred (Nat.sub n 0) < Nat.sub n 0)getLast (ofFn f) h = f { val := n - 1, isLt := hn }simp [getLast_eq_get: ∀ {α : Type ?u.27455} (l : List α) (h : l ≠ []),
getLast l h = get l { val := length l - 1, isLt := (_ : length l - 1 < length l) }getLast_eq_get]Goals accomplished! 🐙
#align list.last_of_fn List.last_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (h : ofFn f ≠ [])
(hn : optParam (n - 1 < n) (_ : pred (Nat.sub n 0) < Nat.sub n 0)),
getLast (ofFn f) h = f { val := n - 1, isLt := hn }List.last_ofFn

theorem last_ofFn_succ: ∀ {n : ℕ} (f : Fin (succ n) → α) (h : optParam (ofFn f ≠ []) (_ : ¬ofFn f = [])), getLast (ofFn f) h = f (Fin.last n)last_ofFn_succ {n: ℕn : ℕ: Typeℕ} (f: Fin (succ n) → αf : Fin: ℕ → TypeFin n: ℕn.succ: ℕ → ℕsucc → α: Type uα)
(h: optParam (ofFn f ≠ []) (_ : ¬ofFn f = [])h : ofFn: {α : Type ?u.28919} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin (succ n) → αf ≠ []: List ?m.28928[] := mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬amt ofFn_eq_nil_iff: ∀ {α : Type ?u.28933} {n : ℕ} {f : Fin n → α}, ofFn f = [] ↔ n = 0ofFn_eq_nil_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp (Nat.succ_ne_zero: ∀ (n : ℕ), succ n ≠ 0Nat.succ_ne_zero _: ℕ_)) :
getLast: {α : Type ?u.28962} → (as : List α) → as ≠ [] → αgetLast (ofFn: {α : Type ?u.28964} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin (succ n) → αf) h: optParam (ofFn f ≠ []) (_ : ¬?m.28929)h = f: Fin (succ n) → αf (Fin.last: (n : ℕ) → Fin (n + 1)Fin.last _: ℕ_) :=
last_ofFn: ∀ {α : Type ?u.28978} {n : ℕ} (f : Fin n → α) (h : ofFn f ≠ [])
(hn : optParam (n - 1 < n) (_ : pred (Nat.sub n 0) < Nat.sub n 0)),
getLast (ofFn f) h = f { val := n - 1, isLt := hn }last_ofFn f: Fin (succ n) → αf h: optParam (ofFn f ≠ []) (_ : ¬ofFn f = [])h
#align list.last_of_fn_succ List.last_ofFn_succ: ∀ {α : Type u} {n : ℕ} (f : Fin (succ n) → α) (h : optParam (ofFn f ≠ []) (_ : ¬ofFn f = [])),
getLast (ofFn f) h = f (Fin.last n)List.last_ofFn_succ

/-- Note this matches the convention of `List.ofFn_succ'`, putting the `Fin m` elements first. -/
theorem ofFn_add: ∀ {α : Type u} {m n : ℕ} (f : Fin (m + n) → α),
ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)ofFn_add {m: ?m.29018m n: ℕn} (f: Fin (m + n) → αf : Fin: ℕ → TypeFin (m: ?m.29018m + n: ?m.29021n) → α: Type uα) :
List.ofFn: {α : Type ?u.29069} → {n : ℕ} → (Fin n → α) → List αList.ofFn f: Fin (m + n) → αf =
(List.ofFn: {α : Type ?u.29079} → {n : ℕ} → (Fin n → α) → List αList.ofFn fun i: ?m.29083i => f: Fin (m + n) → αf (Fin.castAdd: {n : ℕ} → (m : ℕ) → Fin n ↪o Fin (n + m)Fin.castAdd n: ?m.29021n i: ?m.29083i)) ++ List.ofFn: {α : Type ?u.29271} → {n : ℕ} → (Fin n → α) → List αList.ofFn fun j: ?m.29275j => f: Fin (m + n) → αf (Fin.natAdd: (n : ℕ) → {m : ℕ} → Fin m ↪o Fin (n + m)Fin.natAdd m: ?m.29018m j: ?m.29275j) := byGoals accomplished! 🐙
α: Type um, n: ℕf: Fin (m + n) → αofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)induction' n: ℕn with n: ℕn IH: ?m.29479 nIHα: Type um, n: ℕf✝: Fin (m + n) → αf: Fin (m + zero) → αzeroofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type um, n: ℕf✝: Fin (m + n) → αf: Fin (m + zero) → αzeroofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)rflGoals accomplished! 🐙
α: Type um, n: ℕf: Fin (m + n) → αofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)·α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j) α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)rw [α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)ofFn_succ': ∀ {α : Type ?u.29708} {n : ℕ} (f : Fin (succ n) → α),
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))ofFn_succ',α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccconcat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (Nat.add m n))) =   (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j) α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)ofFn_succ': ∀ {α : Type ?u.29745} {n : ℕ} (f : Fin (succ n) → α),
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))ofFn_succ',α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccconcat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (Nat.add m n))) =   (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++     concat (ofFn fun i => f (↑(Fin.natAdd m) (↑Fin.castSucc i))) (f (↑(Fin.natAdd m) (Fin.last n))) α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)IH: ?m.29479 nIH,α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccconcat ((ofFn fun i => f (↑Fin.castSucc (↑(Fin.castAdd n) i))) ++ ofFn fun j => f (↑Fin.castSucc (↑(Fin.natAdd m) j)))
(f (Fin.last (Nat.add m n))) =   (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++     concat (ofFn fun i => f (↑(Fin.natAdd m) (↑Fin.castSucc i))) (f (↑(Fin.natAdd m) (Fin.last n))) α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)append_concat: ∀ {α : Type ?u.29857} (a : α) (l₁ l₂ : List α), l₁ ++ concat l₂ a = concat (l₁ ++ l₂) aappend_concatα: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccconcat ((ofFn fun i => f (↑Fin.castSucc (↑(Fin.castAdd n) i))) ++ ofFn fun j => f (↑Fin.castSucc (↑(Fin.natAdd m) j)))
(f (Fin.last (Nat.add m n))) =   concat ((ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun i => f (↑(Fin.natAdd m) (↑Fin.castSucc i)))
(f (↑(Fin.natAdd m) (Fin.last n)))]α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccconcat ((ofFn fun i => f (↑Fin.castSucc (↑(Fin.castAdd n) i))) ++ ofFn fun j => f (↑Fin.castSucc (↑(Fin.natAdd m) j)))
(f (Fin.last (Nat.add m n))) =   concat ((ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun i => f (↑(Fin.natAdd m) (↑Fin.castSucc i)))
α: Type um, n✝: ℕf✝: Fin (m + n✝) → αn: ℕIH: ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)f: Fin (m + succ n) → αsuccofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)rflGoals accomplished! 🐙
#align list.of_fn_add List.ofFn_add: ∀ {α : Type u} {m n : ℕ} (f : Fin (m + n) → α),
ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)List.ofFn_add

@[simp]
theorem ofFn_fin_append: ∀ {α : Type u} {m n : ℕ} (a : Fin m → α) (b : Fin n → α), ofFn (Fin.append a b) = ofFn a ++ ofFn bofFn_fin_append {m: ℕm n: ?m.30110n} (a: Fin m → αa : Fin: ℕ → TypeFin m: ?m.30107m → α: Type uα) (b: Fin n → αb : Fin: ℕ → TypeFin n: ?m.30110n → α: Type uα) :
List.ofFn: {α : Type ?u.30122} → {n : ℕ} → (Fin n → α) → List αList.ofFn (Fin.append: {m n : ℕ} → {α : Type ?u.30125} → (Fin m → α) → (Fin n → α) → Fin (m + n) → αFin.append a: Fin m → αa b: Fin n → αb) = List.ofFn: {α : Type ?u.30144} → {n : ℕ} → (Fin n → α) → List αList.ofFn a: Fin m → αa ++ List.ofFn: {α : Type ?u.30150} → {n : ℕ} → (Fin n → α) → List αList.ofFn b: Fin n → αb := byGoals accomplished! 🐙
α: Type um, n: ℕa: Fin m → αb: Fin n → αofFn (Fin.append a b) = ofFn a ++ ofFn bsimp_rw [α: Type um, n: ℕa: Fin m → αb: Fin n → αofFn (Fin.append a b) = ofFn a ++ ofFn bofFn_add: ∀ {α : Type ?u.30354} {m n : ℕ} (f : Fin (m + n) → α),
ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)ofFn_add,α: Type um, n: ℕa: Fin m → αb: Fin n → α((ofFn fun i => Fin.append a b (↑(Fin.castAdd n) i)) ++ ofFn fun j => Fin.append a b (↑(Fin.natAdd m) j)) =   ofFn a ++ ofFn b α: Type um, n: ℕa: Fin m → αb: Fin n → αofFn (Fin.append a b) = ofFn a ++ ofFn bFin.append_left: ∀ {m n : ℕ} {α : Type ?u.30746} (u : Fin m → α) (v : Fin n → α) (i : Fin m), Fin.append u v (↑(Fin.castAdd n) i) = u iFin.append_left,α: Type um, n: ℕa: Fin m → αb: Fin n → α((ofFn fun i => a i) ++ ofFn fun j => Fin.append a b (↑(Fin.natAdd m) j)) = ofFn a ++ ofFn b α: Type um, n: ℕa: Fin m → αb: Fin n → αofFn (Fin.append a b) = ofFn a ++ ofFn bFin.append_right: ∀ {m n : ℕ} {α : Type ?u.30929} (u : Fin m → α) (v : Fin n → α) (i : Fin n), Fin.append u v (↑(Fin.natAdd m) i) = v iFin.append_rightGoals accomplished! 🐙]Goals accomplished! 🐙
#align list.of_fn_fin_append List.ofFn_fin_append: ∀ {α : Type u} {m n : ℕ} (a : Fin m → α) (b : Fin n → α), ofFn (Fin.append a b) = ofFn a ++ ofFn bList.ofFn_fin_append

/-- This breaks a list of `m*n` items into `m` groups each containing `n` elements. -/
theorem ofFn_mul: ∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })ofFn_mul {m: ?m.31131m n: ?m.31134n} (f: Fin (m * n) → αf : Fin: ℕ → TypeFin (m: ?m.31131m * n: ?m.31134n) → α: Type uα) :
List.ofFn: {α : Type ?u.31190} → {n : ℕ} → (Fin n → α) → List αList.ofFn f: Fin (m * n) → αf = List.join: {α : Type ?u.31197} → List (List α) → List αList.join (List.ofFn: {α : Type ?u.31199} → {n : ℕ} → (Fin n → α) → List αList.ofFn fun i: Fin mi : Fin: ℕ → TypeFin m: ?m.31131m => List.ofFn: {α : Type ?u.31205} → {n : ℕ} → (Fin n → α) → List αList.ofFn fun j: Fin nj : Fin: ℕ → TypeFin n: ?m.31134n => f: Fin (m * n) → αf ⟨i: Fin mi * n: ?m.31134n + j: Fin nj,
calc
↑i: Fin mi * n: ?m.31134n + j: Fin nj < (i: Fin mi + 1: ?m.316531) * n: ?m.31134n := (add_lt_add_left: ∀ {α : Type ?u.31939} [inst : Add α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b c : α}, b < c → ∀ (a : α), a + b < a + cadd_lt_add_left j: Fin nj.prop: ∀ {n : ℕ} (a : Fin n), ↑a < nprop _: ?m.31940_).trans_eq: ∀ {α : Type ?u.32211} [inst : Preorder α] {a b c : α}, a < b → b = c → a < ctrans_eq (add_one_mul: ∀ {α : Type ?u.32272} [inst : Add α] [inst_1 : MulOneClass α] [inst_2 : RightDistribClass α] (a b : α),
(a + 1) * b = a * b + badd_one_mul (_: ℕ_ : ℕ: Typeℕ) _: ?m.32273_).symm: ∀ {α : Sort ?u.32320} {a b : α}, a = b → b = asymm
_: ?m✝_ ≤ _: ?m.32349_ := Nat.mul_le_mul_right: ∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * kNat.mul_le_mul_right _: ℕ_ i: Fin mi.prop: ∀ {n : ℕ} (a : Fin n), ↑a < nprop⟩) := byGoals accomplished! 🐙
α: Type um, n: ℕf: Fin (m * n) → αofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })induction' m: ℕm with m: ℕm IH: ?m.32451 mIHα: Type um, n: ℕf✝: Fin (m * n) → αf: Fin (zero * n) → αzeroofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: Type um, n: ℕf: Fin (m * n) → αofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })·α: Type um, n: ℕf✝: Fin (m * n) → αf: Fin (zero * n) → αzeroofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) }) α: Type um, n: ℕf✝: Fin (m * n) → αf: Fin (zero * n) → αzeroofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })simp [ofFn_zero: ∀ {α : Type ?u.32468} (f : Fin 0 → α), ofFn f = []ofFn_zero, zero_mul: ∀ {M₀ : Type ?u.32478} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0zero_mul, ofFn_zero: ∀ {α : Type ?u.32495} (f : Fin 0 → α), ofFn f = []ofFn_zero, join: {α : Type ?u.32501} → List (List α) → List αjoin]Goals accomplished! 🐙
α: Type um, n: ℕf: Fin (m * n) → αofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })·α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) }) α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })simp_rw [α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })ofFn_succ': ∀ {α : Type ?u.33232} {n : ℕ} (f : Fin (succ n) → α),
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))ofFn_succ',α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f =   join
(concat
(ofFn fun i =>
ofFn fun j => f { val := ↑(↑Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(↑Fin.castSucc i) * n + ↑j < succ m * n) })
(ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) })) α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })succ_mul: ∀ (n m : ℕ), succ n * m = n * m + msucc_mul,α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsucc(ofFn fun i => f (↑(Fin.cast (_ : m * n + n = succ m * n)) i)) =   join
(concat
(ofFn fun i =>
ofFn fun j => f { val := ↑(↑Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(↑Fin.castSucc i) * n + ↑j < succ m * n) })
(ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) })) α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })join_concat: ∀ {α : Type ?u.33814} (L : List (List α)) (l : List α), join (concat L l) = join L ++ ljoin_concat,α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsucc(ofFn fun i => f (↑(Fin.cast (_ : m * n + n = succ m * n)) i)) =   join
(ofFn fun i =>
ofFn fun j =>
f { val := ↑(↑Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(↑Fin.castSucc i) * n + ↑j < succ m * n) }) ++     ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) } α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })ofFn_add: ∀ {α : Type ?u.33976} {m n : ℕ} (f : Fin (m + n) → α),
ofFn f = (ofFn fun i => f (↑(Fin.castAdd n) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)ofFn_add,α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsucc((ofFn fun i => f (↑(Fin.cast (_ : m * n + n = succ m * n)) (↑(Fin.castAdd n) i))) ++     ofFn fun j => f (↑(Fin.cast (_ : m * n + n = succ m * n)) (↑(Fin.natAdd (m * n)) j))) =   join
(ofFn fun i =>
ofFn fun j =>
f { val := ↑(↑Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(↑Fin.castSucc i) * n + ↑j < succ m * n) }) ++     ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) } α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })IH: ?m.32451 mIHα: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsucc(join
(ofFn fun i =>
ofFn fun j =>
f
(↑(Fin.cast (_ : m * n + n = succ m * n))
(↑(Fin.castAdd n) { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) }))) ++     ofFn fun j => f (↑(Fin.cast (_ : m * n + n = succ m * n)) (↑(Fin.natAdd (m * n)) j))) =   join
(ofFn fun i =>
ofFn fun j =>
f { val := ↑(↑Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(↑Fin.castSucc i) * n + ↑j < succ m * n) }) ++     ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) }]α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsucc(join
(ofFn fun i =>
ofFn fun j =>
f
(↑(Fin.cast (_ : m * n + n = succ m * n))
(↑(Fin.castAdd n) { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) }))) ++     ofFn fun j => f (↑(Fin.cast (_ : m * n + n = succ m * n)) (↑(Fin.natAdd (m * n)) j))) =   join
(ofFn fun i =>
ofFn fun j =>
f { val := ↑(↑Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(↑Fin.castSucc i) * n + ↑j < succ m * n) }) ++     ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) }
α: Type um✝, n: ℕf✝: Fin (m✝ * n) → αm: ℕIH: ∀ (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })f: Fin (succ m * n) → αsuccofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })rflGoals accomplished! 🐙
#align list.of_fn_mul List.ofFn_mul: ∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })List.ofFn_mul

/-- This breaks a list of `m*n` items into `n` groups each containing `m` elements. -/
theorem ofFn_mul': ∀ {m n : ℕ} (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })ofFn_mul' {m: ?m.34699m n: ?m.34702n} (f: Fin (m * n) → αf : Fin: ℕ → TypeFin (m: ?m.34699m * n: ?m.34702n) → α: Type uα) :
List.ofFn: {α : Type ?u.34758} → {n : ℕ} → (Fin n → α) → List αList.ofFn f: Fin (m * n) → αf = List.join: {α : Type ?u.34765} → List (List α) → List αList.join (List.ofFn: {α : Type ?u.34767} → {n : ℕ} → (Fin n → α) → List αList.ofFn fun i: Fin ni : Fin: ℕ → TypeFin n: ?m.34702n => List.ofFn: {α : Type ?u.34773} → {n : ℕ} → (Fin n → α) → List αList.ofFn fun j: Fin mj : Fin: ℕ → TypeFin m: ?m.34699m => f: Fin (m * n) → αf ⟨m: ?m.34699m * i: Fin ni + j: Fin mj,
calc
m: ?m.34699m * i: Fin ni + j: Fin mj < m: ?m.34699m * (i: Fin ni + 1: ?m.352181) := (add_lt_add_left: ∀ {α : Type ?u.35587} [inst : Add α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b c : α}, b < c → ∀ (a : α), a + b < a + cadd_lt_add_left j: Fin mj.prop: ∀ {n : ℕ} (a : Fin n), ↑a < nprop _: ?m.35588_).trans_eq: ∀ {α : Type ?u.35859} [inst : Preorder α] {a b c : α}, a < b → b = c → a < ctrans_eq (mul_add_one: ∀ {α : Type ?u.35920} [inst : Add α] [inst_1 : MulOneClass α] [inst_2 : LeftDistribClass α] (a b : α),
a * (b + 1) = a * b + amul_add_one (_: ℕ_ : ℕ: Typeℕ) _: ?m.35921_).symm: ∀ {α : Sort ?u.35968} {a b : α}, a = b → b = asymm
_: ?m✝_ ≤ _: ?m.35997_ := Nat.mul_le_mul_left: ∀ {n m : ℕ} (k : ℕ), n ≤ m → k * n ≤ k * mNat.mul_le_mul_left _: ℕ_ i: Fin ni.prop: ∀ {n : ℕ} (a : Fin n), ↑a < nprop⟩) := byGoals accomplished! 🐙
α: Type um, n: ℕf: Fin (m * n) → αofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })simp_rw [α: Type um, n: ℕf: Fin (m * n) → αofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })mul_comm: ∀ {G : Type ?u.36250} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm m: ℕm n: ℕn,α: Type um, n: ℕf: Fin (m * n) → α(ofFn fun i => f (↑(Fin.cast (_ : n * m = m * n)) i)) =   join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) }) α: Type um, n: ℕf: Fin (m * n) → αofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })mul_comm: ∀ {G : Type ?u.36480} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm m: ℕm,α: Type um, n: ℕf: Fin (m * n) → α(ofFn fun i => f (↑(Fin.cast (_ : n * m = m * n)) i)) =   join (ofFn fun i => ofFn fun j => f { val := ↑i * m + ↑j, isLt := (_ : ↑i * m + ↑j < m * n) }) α: Type um, n: ℕf: Fin (m * n) → αofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })ofFn_mul: ∀ {α : Type ?u.36693} {m n : ℕ} (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })ofFn_mul,α: Type um, n: ℕf: Fin (m * n) → αjoin
(ofFn fun i =>
ofFn fun j => f (↑(Fin.cast (_ : n * m = m * n)) { val := ↑i * m + ↑j, isLt := (_ : ↑i * m + ↑j < n * m) })) =   join (ofFn fun i => ofFn fun j => f { val := ↑i * m + ↑j, isLt := (_ : ↑i * m + ↑j < m * n) }) α: Type um, n: ℕf: Fin (m * n) → αofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })Fin.cast_mkGoals accomplished! 🐙]Goals accomplished! 🐙
#align list.of_fn_mul' List.ofFn_mul': ∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α),
ofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })List.ofFn_mul'

theorem ofFn_get: ∀ (l : List α), ofFn (get l) = lofFn_get : ∀ l: List αl : List: Type ?u.37191 → Type ?u.37191List α: Type uα, (ofFn: {α : Type ?u.37195} → {n : ℕ} → (Fin n → α) → List αofFn (get: {α : Type ?u.37198} → (as : List α) → Fin (length as) → αget l: List αl)) = l: List αl
| [] => rfl: ∀ {α : Sort ?u.37221} {a : α}, a = arfl
| a: αa :: l: List αl => byGoals accomplished! 🐙
α: Type ua: αl: List αofFn (get (a :: l)) = a :: lrw [α: Type ua: αl: List αofFn (get (a :: l)) = a :: lofFn_succ: ∀ {α : Type ?u.37612} {n : ℕ} (f : Fin (succ n) → α), ofFn f = f 0 :: ofFn fun i => f (Fin.succ i)ofFn_succα: Type ua: αl: List α(get (a :: l) 0 :: ofFn fun i => get (a :: l) (Fin.succ i)) = a :: l]α: Type ua: αl: List α(get (a :: l) 0 :: ofFn fun i => get (a :: l) (Fin.succ i)) = a :: l
α: Type ua: αl: List αofFn (get (a :: l)) = a :: lcongrα: Type ua: αl: List αe_tail(ofFn fun i => get (a :: l) (Fin.succ i)) = l
α: Type ua: αl: List αofFn (get (a :: l)) = a :: lsimp only [Fin.val_succ: ∀ {n : ℕ} (j : Fin n), ↑(Fin.succ j) = ↑j + 1Fin.val_succ]α: Type ua: αl: List αe_tail(ofFn fun i => get (a :: l) (Fin.succ i)) = l
α: Type ua: αl: List αofFn (get (a :: l)) = a :: lexact ofFn_get: ∀ (l : List α), ofFn (get l) = lofFn_get l: List αlGoals accomplished! 🐙

set_option linter.deprecated false in
@[deprecated ofFn_get: ∀ {α : Type u} (l : List α), ofFn (get l) = lofFn_get]
theorem ofFn_nthLe: ∀ {α : Type u} (l : List α), (ofFn fun i => nthLe l ↑i (_ : ↑i < length l)) = lofFn_nthLe : ∀ l: List αl : List: Type ?u.39293 → Type ?u.39293List α: Type uα, (ofFn: {α : Type ?u.39297} → {n : ℕ} → (Fin n → α) → List αofFn fun i: ?m.39301i => nthLe: {α : Type ?u.39303} → (l : List α) → (n : ℕ) → n < length l → αnthLe l: List αl i: ?m.39301i i: ?m.39301i.2: ∀ {n : ℕ} (self : Fin n), ↑self < n2) = l: List αl :=
ofFn_get: ∀ {α : Type ?u.39423} (l : List α), ofFn (get l) = lofFn_get
#align list.of_fn_nth_le List.ofFn_nthLe: ∀ {α : Type u} (l : List α), (ofFn fun i => nthLe l ↑i (_ : ↑i < length l)) = lList.ofFn_nthLe

-- not registered as a simp lemma, as otherwise it fires before `forall_mem_ofFn_iff` which
-- is much more useful
theorem mem_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (a : α), a ∈ ofFn f ↔ a ∈ Set.range fmem_ofFn {n: ℕn} (f: Fin n → αf : Fin: ℕ → TypeFin n: ?m.39455n → α: Type uα) (a: αa : α: Type uα) : a: αa ∈ ofFn: {α : Type ?u.39469} → {n : ℕ} → (Fin n → α) → List αofFn f: Fin n → αf ↔ a: αa ∈ Set.range: {α : Type ?u.39492} → {ι : Sort ?u.39491} → (ι → α) → Set αSet.range f: Fin n → αf := byGoals accomplished! 🐙
α: Type un: ℕf: Fin n → αa: αa ∈ ofFn f ↔ a ∈ Set.range fsimp only [mem_iff_get: ∀ {α : Type ?u.39523} {a : α} {l : List α}, a ∈ l ↔ ∃ n, get l n = amem_iff_get, Set.mem_range: ∀ {α : Type ?u.39542} {ι : Sort ?u.39543} {f : ι → α} {x : α}, x ∈ Set.range f ↔ ∃ y, f y = xSet.mem_range, get_ofFn: ∀ {α : Type ?u.39571} {n : ℕ} (f : Fin n → α) (i : Fin (length (ofFn f))),
get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)get_ofFn]α: Type un: ℕf: Fin n → αa: α(∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = a
α: Type un: ℕf: Fin n → αa: αa ∈ ofFn f ↔ a ∈ Set.range fexact ⟨fun ⟨i: Fin (length (ofFn f))i, hi: f (↑(Fin.cast (_ : length (ofFn f) = n)) i) = ahi⟩ => ⟨Fin.cast: {n m : ℕ} → n = m → Fin n ≃o Fin mFin.cast (α: Type un: ℕf: Fin n → αa: α(∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = abyGoals accomplished! 🐙 α: Type un: ℕf: Fin n → αa: αx✝: ∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = ai: Fin (length (ofFn f))hi: f (↑(Fin.cast (_ : length (ofFn f) = n)) i) = alength (ofFn f) = nsimpGoals accomplished! 🐙) i: Fin (length (ofFn f))i, hi: f (↑(Fin.cast (_ : length (ofFn f) = n)) i) = ahi⟩, fun ⟨i: Fin ni, hi: f i = ahi⟩ => ⟨Fin.cast: {n m : ℕ} → n = m → Fin n ≃o Fin mFin.cast (α: Type un: ℕf: Fin n → αa: α(∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = abyGoals accomplished! 🐙 α: Type un: ℕf: Fin n → αa: αx✝: ∃ y, f y = ai: Fin nhi: f i = an = length (ofFn f)simpGoals accomplished! 🐙) i: Fin ni, hi: f i = ahi⟩⟩Goals accomplished! 🐙
#align list.mem_of_fn List.mem_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (a : α), a ∈ ofFn f ↔ a ∈ Set.range fList.mem_ofFn

@[simp]
theorem forall_mem_ofFn_iff: ∀ {α : Type u} {n : ℕ} {f : Fin n → α} {P : α → Prop}, (∀ (```