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.
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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) = n
length_ofFn
{n} (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.6
n
→
α: Type u
α
) :
length: {α : Type ?u.14} → List α → ℕ
length
(
ofFn: {α : Type ?u.16} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
) =
n: ?m.6
n
:=

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α


length (ofFn f) = n

Goals accomplished! 🐙
#align list.length_of_fn
List.length_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α), length (ofFn f) = n
List.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} (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.118
n
→
α: 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.125
i
=
f: Fin n → α
f
(
Fin.cast: {n m : ℕ} → n = m → Fin n ≃o Fin m
Fin.cast
(

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


length (ofFn f) = n

Goals accomplished! 🐙
)
i: ?m.125
i
) :=

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
α: Type u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


↑i < Array.size (Array.ofFn f)

Goals accomplished! 🐙
α: Type u

n: ℕ

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 u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
α: Type u

n: ℕ

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) }


mk
get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := hi })
α: Type u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
α: Type u

n: ℕ

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
get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := hi })
α: Type u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
α: Type u

n: ℕ

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
get (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := (_ : i < n) }
α: Type u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
α: Type u

n: ℕ

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
get (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := (_ : i < n) }
α: Type u

n: ℕ

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
get (ofFn f) { val := i, isLt := hi } = get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }
α: Type u

n: ℕ

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
get (ofFn f) { val := i, isLt := hi } = get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }
α: Type u

n: ℕ

f: Fin n → α

i: Fin (length (ofFn f))


get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
α: Type u

n: ℕ

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.h
ofFn f = (Array.ofFn f).data
α: Type u

n: ℕ

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_a
ofFn f = (Array.ofFn f).data
α: Type u

n: ℕ

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_3
HEq hi (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f))
α: Type u

n: ℕ

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
get (ofFn f) { val := i, isLt := hi } = get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }
α: Type u

n: ℕ

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.h
ofFn f = (Array.ofFn f).data
α: Type u

n: ℕ

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_a
ofFn f = (Array.ofFn f).data
α: Type u

n: ℕ

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_3
HEq hi (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f))
α: Type u

n: ℕ

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
get (ofFn f) { val := i, isLt := hi } = get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }

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 i
get?_ofFn
{
n: ?m.13674
n
} (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.13674
n
→
α: Type u
α
) (i) :
get?: {α : Type ?u.13685} → List α → ℕ → Option α
get?
(
ofFn: {α : Type ?u.13687} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
)
i: ?m.13681
i
=
ofFnNthVal: {α : Type ?u.13696} → {n : ℕ} → (Fin n → α) → ℕ → Option α
ofFnNthVal
f: Fin n → α
f
i: ?m.13681
i
:= if
h: ?m.13747
h
: i < (
ofFn: {α : Type ?u.13709} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
).
length: {α : Type ?u.13715} → List α → ℕ
length
then

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: i < length (ofFn f)


some (get (ofFn f) { val := i, isLt := h }) = ofFnNthVal f i
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i
α: Type u

n: ℕ

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 u

n: ℕ

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 u

n: ℕ

f: Fin n → α

i: ℕ

h: i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i
α: Type u

n: ℕ

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 u

n: ℕ

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 u

n: ℕ

f: Fin n → α

i: ℕ

h✝: i < length (ofFn f)

h: i < n


some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h✝ })) = ofFnNthVal f i
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h✝: i < length (ofFn f)

h: i < n


some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h✝ })) = ofFnNthVal f i
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: i < length (ofFn f)


some (f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i

Goals accomplished! 🐙
else

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i
α: Type u

n: ℕ

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 u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


get? (ofFn f) i = none
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


hnc
¬i < n
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


get? (ofFn f) i = none
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


hnc
¬i < n
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


get? (ofFn f) i = none
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


hnc
¬i < n
α: Type u

n: ℕ

f: Fin n → α

i: ℕ

h: ¬i < length (ofFn f)


get? (ofFn f) i = ofFnNthVal f i

Goals accomplished! 🐙
#align list.nth_of_fn
List.get?_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : ℕ), get? (ofFn f) i = ofFnNthVal f i
List.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 i
nthLe_ofFn
{
n: ?m.17429
n
} (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.17429
n
→
α: Type u
α
) (
i: Fin n
i
:
Fin: ℕ → Type
Fin
n: ?m.17429
n
) :
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 n
i
((
length_ofFn: ∀ {α : Type ?u.17554} {n : ℕ} (f : Fin n → α), length (ofFn f) = n
length_ofFn
f: Fin n → α
f
).
symm: ∀ {α : Sort ?u.17560} {a b : α}, a = b → b = a
symm
▸
i: Fin n
i
.
2: ∀ {n : ℕ} (self : Fin n), ↑self < n
2
) =
f: Fin n → α
f
i: Fin n
i
:=

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

i: Fin n


nthLe (ofFn f) ↑i (_ : ↑i < length (ofFn f)) = f i

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 i
List.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.18338
n
} (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.18338
n
→
α: Type u
α
) {i :
ℕ: Type
ℕ
} (
h: i < length (ofFn f)
h
: 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
h: i < length (ofFn f)
h
=
f: Fin n → α
f
⟨i,
length_ofFn: ∀ {α : Type ?u.18381} {n : ℕ} (f : Fin n → α), length (ofFn f) = n
length_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 i
nthLe_ofFn
f: Fin n → α
f
⟨i,
length_ofFn: ∀ {α : Type ?u.18409} {n : ℕ} (f : Fin n → α), length (ofFn f) = n
length_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 :
ℕ: Type
ℕ
} (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
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
(

Goals accomplished! 🐙
α: Type u

β: Type u_1

n: ℕ

f: Fin n → α

g: α → β


length (map g (ofFn f)) = length (ofFn (g ∘ f))

Goals accomplished! 🐙
) fun
i: ?m.18523
i
h: ?m.18526
h
h': ?m.18529
h'
=>

Goals accomplished! 🐙
α: Type u

β: Type u_1

n: ℕ

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' }

Goals 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 n :
ℕ: Type
ℕ
} (
h: m = n
h
: m = n) (
f: Fin m → α
f
:
Fin: ℕ → Type
Fin
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 n
i
:
Fin: ℕ → Type
Fin
n =>
f: Fin m → α
f
(
Fin.cast: {n m : ℕ} → n = m → Fin n ≃o Fin m
Fin.cast
h: m = n
h
.
symm: ∀ {α : Sort ?u.20537} {a b : α}, a = b → b = a
symm
i: Fin n
i
) :=

Goals accomplished! 🐙
α: Type u

m, n: ℕ

h: m = n

f: Fin m → α


ofFn f = ofFn fun i => f (↑(Fin.cast (_ : n = m)) i)
α: Type u

m: ℕ

f: Fin m → α


ofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)
α: Type u

m, n: ℕ

h: m = n

f: Fin m → α


ofFn f = ofFn fun i => f (↑(Fin.cast (_ : n = m)) i)
α: Type u

m: ℕ

f: Fin m → α


ofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)
α: Type u

m: ℕ

f: Fin m → α


ofFn f = ofFn fun i => f (↑(OrderIso.refl (Fin m)) i)
α: Type u

m: ℕ

f: Fin m → α


ofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)

Goals 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: ℕ → Type
Fin
0: ?m.21020
0
→
α: Type u
α
) :
ofFn: {α : Type ?u.21034} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin 0 → α
f
=
[]: List ?m.21042
[]
:=
rfl: ∀ {α : Sort ?u.21074} {a : α}, a = a
rfl
#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.21225
n
} (
f: Fin (succ n) → α
f
:
Fin: ℕ → Type
Fin
(
succ: ℕ → ℕ
succ
n: ?m.21225
n
) →
α: Type u
α
) :
ofFn: {α : Type ?u.21233} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin (succ n) → α
f
=
f: Fin (succ n) → α
f
0: ?m.21243
0
::
ofFn: {α : Type ?u.21271} → {n : ℕ} → (Fin n → α) → List α
ofFn
fun
i: ?m.21276
i
=>
f: Fin (succ n) → α
f
i: ?m.21276
i
.
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
(

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin (succ n) → α


length (ofFn f) = length (f 0 :: ofFn fun i => f (Fin.succ i))

Goals accomplished! 🐙
) (fun
i: ?m.21298
i
hi₁: ?m.21301
hi₁
hi₂: ?m.21304
hi₂
=>

Goals accomplished! 🐙
α: Type u

n: ℕ

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 u

n: ℕ

f: Fin (succ n) → α

hi₁: zero < length (ofFn f)

hi₂: zero < length (f 0 :: ofFn fun i => f (Fin.succ i))


zero
get (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }
α: Type u

n: ℕ

f: Fin (succ n) → α

n✝: ℕ

hi₁: succ n✝ < length (ofFn f)

hi₂: succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))


succ
get (ofFn f) { val := succ n✝, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
α: Type u

n: ℕ

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 u

n: ℕ

f: Fin (succ n) → α

hi₁: zero < length (ofFn f)

hi₂: zero < length (f 0 :: ofFn fun i => f (Fin.succ i))


zero
get (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }
α: Type u

n: ℕ

f: Fin (succ n) → α

hi₁: zero < length (ofFn f)

hi₂: zero < length (f 0 :: ofFn fun i => f (Fin.succ i))


zero
get (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }
α: Type u

n: ℕ

f: Fin (succ n) → α

n✝: ℕ

hi₁: succ n✝ < length (ofFn f)

hi₂: succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))


succ
get (ofFn f) { val := succ n✝, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }

Goals accomplished! 🐙
α: Type u

n: ℕ

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 u

n: ℕ

f: Fin (succ n) → α

n✝: ℕ

hi₁: succ n✝ < length (ofFn f)

hi₂: succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))


succ
get (ofFn f) { val := succ n✝, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
α: Type u

n: ℕ

f: Fin (succ n) → α

n✝: ℕ

hi₁: succ n✝ < length (ofFn f)

hi₂: succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))


succ
get (ofFn f) { val := succ n✝, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }

Goals 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} (
f: Fin (succ n) → α
f
:
Fin: ℕ → Type
Fin
(
succ: ℕ → ℕ
succ
n: ?m.25515
n
) →
α: 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.25534
i
=>
f: Fin (succ n) → α
f
(
Fin.castSucc: {n : ℕ} → Fin n ↪o Fin (n + 1)
Fin.castSucc
i: ?m.25534
i
)).
concat: {α : Type ?u.25716} → List α → α → List α
concat
(
f: Fin (succ n) → α
f
(
Fin.last: (n : ℕ) → Fin (n + 1)
Fin.last
_)) :=

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin (succ n) → α


ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))
α: Type u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n: ℕ

f: Fin (succ n) → α


ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))
α: Type u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
(f 0 :: ofFn fun i => f (Fin.succ i)) = [f (Fin.last zero)]
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
[f 0] = [f (Fin.last zero)]
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
[f 0] = [f (Fin.last zero)]
α: Type u

n: ℕ

f✝: Fin (succ n) → α

f: Fin (succ zero) → α


zero
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last zero))

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin (succ n) → α


ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last n))
α: Type u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n✝: ℕ

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 u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n✝: ℕ

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 :: 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 u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n✝: ℕ

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 :: 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 u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n✝: ℕ

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 :: 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 u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))
α: Type u

n✝: ℕ

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 :: 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 u

n✝: ℕ

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 :: 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 u

n✝: ℕ

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
ofFn f = concat (ofFn fun i => f (↑Fin.castSucc i)) (f (Fin.last (succ n)))

Goals 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 = 0
ofFn_eq_nil_iff
{n :
ℕ: Type
ℕ
} {
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n →
α: Type u
α
} :
ofFn: {α : Type ?u.26680} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
=
[]: List ?m.26688
[]
↔ n =
0: ?m.26720
0
:=

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α


ofFn f = [] ↔ n = 0
α: Type u

f: Fin zero → α


zero
ofFn f = [] ↔ zero = 0
α: Type u

n✝: ℕ

f: Fin (succ n✝) → α


succ
ofFn f = [] ↔ succ n✝ = 0
α: Type u

n: ℕ

f: Fin n → α


ofFn f = [] ↔ n = 0
α: Type u

f: Fin zero → α


zero
ofFn f = [] ↔ zero = 0
α: Type u

n✝: ℕ

f: Fin (succ n✝) → α


succ
ofFn f = [] ↔ succ n✝ = 0
α: Type u

n: ℕ

f: Fin n → α


ofFn f = [] ↔ n = 0

Goals accomplished! 🐙
#align list.of_fn_eq_nil_iff
List.ofFn_eq_nil_iff: ∀ {α : Type u} {n : ℕ} {f : Fin n → α}, ofFn f = [] ↔ n = 0
List.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 :
ℕ: Type
ℕ
} (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
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 -
1: ?m.27167
1
< n :=
Nat.pred_lt: ∀ {n : ℕ}, n ≠ 0 → pred n < n
Nat.pred_lt
<|
ofFn_eq_nil_iff: ∀ {α : Type ?u.27282} {n : ℕ} {f : Fin n → α}, ofFn f = [] ↔ n = 0
ofFn_eq_nil_iff
.
not: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
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 -
1: ?m.27401
1
,
hn: optParam (n - 1 < n) (_ : pred ?m.27239 < ?m.27239)
hn
⟩ :=

Goals accomplished! 🐙
α: 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 }

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 :
ℕ: Type
ℕ
} (
f: Fin (succ n) → α
f
:
Fin: ℕ → Type
Fin
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 → ¬a
mt
ofFn_eq_nil_iff: ∀ {α : Type ?u.28933} {n : ℕ} {f : Fin n → α}, ofFn f = [] ↔ n = 0
ofFn_eq_nil_iff
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
(
Nat.succ_ne_zero: ∀ (n : ℕ), succ n ≠ 0
Nat.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.29018
m
n} (
f: Fin (m + n) → α
f
:
Fin: ℕ → Type
Fin
(
m: ?m.29018
m
+
n: ?m.29021
n
) →
α: 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.29083
i
=>
f: Fin (m + n) → α
f
(
Fin.castAdd: {n : ℕ} → (m : ℕ) → Fin n ↪o Fin (n + m)
Fin.castAdd
n: ?m.29021
n
i: ?m.29083
i
)) ++
List.ofFn: {α : Type ?u.29271} → {n : ℕ} → (Fin n → α) → List α
List.ofFn
fun
j: ?m.29275
j
=>
f: Fin (m + n) → α
f
(
Fin.natAdd: (n : ℕ) → {m : ℕ} → Fin m ↪o Fin (n + m)
Fin.natAdd
m: ?m.29018
m
j: ?m.29275
j
) :=

Goals accomplished! 🐙
α: 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)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: 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)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ []
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = ofFn fun i => f (↑(Fin.castAdd zero) i)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = ofFn fun i => f (↑(OrderIso.refl (Fin m)) i)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = ofFn fun i => f (↑(OrderIso.refl (Fin m)) i)
α: Type u

m, n: ℕ

f✝: Fin (m + n) → α

f: Fin (m + zero) → α


zero
ofFn f = (ofFn fun i => f (↑(Fin.castAdd zero) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)

Goals accomplished! 🐙
α: 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)
α: Type u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, 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) → α


succ
concat (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 u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, 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) → α


succ
concat (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 u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, 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) → α


succ
concat ((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 u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)
α: Type u

m, 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) → α


succ
concat ((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 u

m, 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) → α


succ
concat ((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 u

m, 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) → α


succ
ofFn f = (ofFn fun i => f (↑(Fin.castAdd (succ n)) i)) ++ ofFn fun j => f (↑(Fin.natAdd m) j)

Goals 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 b
ofFn_fin_append
{m
n: ?m.30110
n
} (
a: Fin m → α
a
:
Fin: ℕ → Type
Fin
m: ?m.30107
m
→
α: Type u
α
) (
b: Fin n → α
b
:
Fin: ℕ → Type
Fin
n: ?m.30110
n
→
α: 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
:=

Goals accomplished! 🐙
α: Type u

m, n: ℕ

a: Fin m → α

b: Fin n → α


α: Type u

m, n: ℕ

a: Fin m → α

b: Fin n → α


α: Type u

m, 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 u

m, n: ℕ

a: Fin m → α

b: Fin n → α


α: Type u

m, 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 u

m, n: ℕ

a: Fin m → α

b: Fin n → α



Goals 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 b
List.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.31131
m
n: ?m.31134
n
} (
f: Fin (m * n) → α
f
:
Fin: ℕ → Type
Fin
(
m: ?m.31131
m
*
n: ?m.31134
n
) →
α: 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 m
i
:
Fin: ℕ → Type
Fin
m: ?m.31131
m
=>
List.ofFn: {α : Type ?u.31205} → {n : ℕ} → (Fin n → α) → List α
List.ofFn
fun
j: Fin n
j
:
Fin: ℕ → Type
Fin
n: ?m.31134
n
=>
f: Fin (m * n) → α
f
⟨
i: Fin m
i
*
n: ?m.31134
n
+
j: Fin n
j
, calc ↑
i: Fin m
i
*
n: ?m.31134
n
+
j: Fin n
j
< (
i: Fin m
i
+
1: ?m.31653
1
) *
n: ?m.31134
n
:= (
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 + c
add_lt_add_left
j: Fin n
j
.
prop: ∀ {n : ℕ} (a : Fin n), ↑a < n
prop
_: ?m.31940
_
).
trans_eq: ∀ {α : Type ?u.32211} [inst : Preorder α] {a b c : α}, a < b → b = c → a < c
trans_eq
(
add_one_mul: ∀ {α : Type ?u.32272} [inst : Add α] [inst_1 : MulOneClass α] [inst_2 : RightDistribClass α] (a b : α), (a + 1) * b = a * b + b
add_one_mul
(_ :
ℕ: Type
ℕ
)
_: ?m.32273
_
).
symm: ∀ {α : Sort ?u.32320} {a b : α}, a = b → b = a
symm
_: ?m✝
_
≤
_: ?m.32349
_
:=
Nat.mul_le_mul_right: ∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * k
Nat.mul_le_mul_right
_
i: Fin m
i
.
prop: ∀ {n : ℕ} (a : Fin n), ↑a < n
prop
⟩) :=

Goals accomplished! 🐙
α: 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) })
α: Type u

m, n: ℕ

f✝: Fin (m * n) → α

f: Fin (zero * n) → α


zero
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })
α: Type u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: 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) })
α: Type u

m, n: ℕ

f✝: Fin (m * n) → α

f: Fin (zero * n) → α


zero
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })
α: Type u

m, n: ℕ

f✝: Fin (m * n) → α

f: Fin (zero * n) → α


zero
ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })
α: Type u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })

Goals accomplished! 🐙
α: 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) })
α: Type u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: Type u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: Type u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: Type u

m✝, 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 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 u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: Type u

m✝, 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 u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: Type u

m✝, 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 u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: Type u

m✝, 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 u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α: Type u

m✝, 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 u

m✝, 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 u

m✝, 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 f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })

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 := ↑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.34699
m
n: ?m.34702
n
} (
f: Fin (m * n) → α
f
:
Fin: ℕ → Type
Fin
(
m: ?m.34699
m
*
n: ?m.34702
n
) →
α: 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 n
i
:
Fin: ℕ → Type
Fin
n: ?m.34702
n
=>
List.ofFn: {α : Type ?u.34773} → {n : ℕ} → (Fin n → α) → List α
List.ofFn
fun
j: Fin m
j
:
Fin: ℕ → Type
Fin
m: ?m.34699
m
=>
f: Fin (m * n) → α
f
⟨
m: ?m.34699
m
*
i: Fin n
i
+
j: Fin m
j
, calc
m: ?m.34699
m
*
i: Fin n
i
+
j: Fin m
j
<
m: ?m.34699
m
* (
i: Fin n
i
+
1: ?m.35218
1
) := (
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 + c
add_lt_add_left
j: Fin m
j
.
prop: ∀ {n : ℕ} (a : Fin n), ↑a < n
prop
_: ?m.35588
_
).
trans_eq: ∀ {α : Type ?u.35859} [inst : Preorder α] {a b c : α}, a < b → b = c → a < c
trans_eq
(
mul_add_one: ∀ {α : Type ?u.35920} [inst : Add α] [inst_1 : MulOneClass α] [inst_2 : LeftDistribClass α] (a b : α), a * (b + 1) = a * b + a
mul_add_one
(_ :
ℕ: Type
ℕ
)
_: ?m.35921
_
).
symm: ∀ {α : Sort ?u.35968} {a b : α}, a = b → b = a
symm
_: ?m✝
_
≤
_: ?m.35997
_
:=
Nat.mul_le_mul_left: ∀ {n m : ℕ} (k : ℕ), n ≤ m → k * n ≤ k * m
Nat.mul_le_mul_left
_
i: Fin n
i
.
prop: ∀ {n : ℕ} (a : Fin n), ↑a < n
prop
⟩) :=

Goals accomplished! 🐙
α: 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) })
α: 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) })
α: Type u

m, 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 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) })
α: Type u

m, 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 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) })
α: Type u

m, 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 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) })

Goals 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) = l
ofFn_get
: ∀
l: List α
l
:
List: Type ?u.37191 → Type ?u.37191
List
α: 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 = a
rfl
|
a: α
a
::
l: List α
l
=>

Goals accomplished! 🐙
α: Type u

a: α

l: List α


ofFn (get (a :: l)) = a :: l
α: Type u

a: α

l: List α


ofFn (get (a :: l)) = a :: l
α: Type u

a: α

l: List α


(get (a :: l) 0 :: ofFn fun i => get (a :: l) (Fin.succ i)) = a :: l
α: Type u

a: α

l: List α


(get (a :: l) 0 :: ofFn fun i => get (a :: l) (Fin.succ i)) = a :: l
α: Type u

a: α

l: List α


ofFn (get (a :: l)) = a :: l
α: Type u

a: α

l: List α


e_tail
(ofFn fun i => get (a :: l) (Fin.succ i)) = l
α: Type u

a: α

l: List α


ofFn (get (a :: l)) = a :: l
α: Type u

a: α

l: List α


e_tail
(ofFn fun i => get (a :: l) (Fin.succ i)) = l
α: Type u

a: α

l: List α


ofFn (get (a :: l)) = a :: l

Goals accomplished! 🐙
set_option linter.deprecated false in @[deprecated
ofFn_get: ∀ {α : Type u} (l : List α), ofFn (get l) = l
ofFn_get
] theorem
ofFn_nthLe: ∀ {α : Type u} (l : List α), (ofFn fun i => nthLe l ↑i (_ : ↑i < length l)) = l
ofFn_nthLe
: ∀
l: List α
l
:
List: Type ?u.39293 → Type ?u.39293
List
α: Type u
α
, (
ofFn: {α : Type ?u.39297} → {n : ℕ} → (Fin n → α) → List α
ofFn
fun
i: ?m.39301
i
=>
nthLe: {α : Type ?u.39303} → (l : List α) → (n : ℕ) → n < length l → α
nthLe
l: List α
l
i: ?m.39301
i
i: ?m.39301
i
.
2: ∀ {n : ℕ} (self : Fin n), ↑self < n
2
) =
l: List α
l
:=
ofFn_get: ∀ {α : Type ?u.39423} (l : List α), ofFn (get l) = l
ofFn_get
#align list.of_fn_nth_le
List.ofFn_nthLe: ∀ {α : Type u} (l : List α), (ofFn fun i => nthLe l ↑i (_ : ↑i < length l)) = l
List.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 f
mem_ofFn
{n} (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.39455
n
→
α: 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
:=

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

a: α


α: Type u

n: ℕ

f: Fin n → α

a: α


(∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = a
α: Type u

n: ℕ

f: Fin n → α

a: α


α: Type u

n: ℕ

f: Fin n → α

a: α


(∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = a

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

a: α

x✝: ∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a

i: Fin (length (ofFn f))

hi: f (↑(Fin.cast (_ : length (ofFn f) = n)) i) = a


length (ofFn f) = n

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

a: α


(∃ n_1, f (↑(Fin.cast (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = a

Goals accomplished! 🐙
α: Type u

n: ℕ

f: Fin n → α

a: α

x✝: ∃ y, f y = a

i: Fin n

hi: f i = a


n = length (ofFn f)

Goals accomplished! 🐙

Goals accomplished! 🐙
#align list.mem_of_fn
List.mem_ofFn: ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (a : α), a ∈ ofFn f ↔ a ∈ Set.range f
List.mem_ofFn
@[simp] theorem
forall_mem_ofFn_iff: ∀ {α : Type u} {n : ℕ} {f : Fin n → α} {P : α → Prop}, (∀ (