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, Kenny Lau, Scott Morrison

! This file was ported from Lean 3 source module data.list.fin_range
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.OfFn
import Mathlib.Data.List.Perm

/-!
# Lists of elements of `Fin n`

This file develops some results on `finRange n`.
-/


universe u

namespace List

variable {
Ī±: Type u
Ī± : 
Type u: Type (u+1)
Type u}

@[simp]
theorem 
map_coe_finRange: āˆ€ (n : ā„•), map Fin.val (finRange n) = range n
map_coe_finRange (
n: ā„•
n : 
ā„•: Type
ā„•) : ((
finRange: (n : ā„•) ā†’ List (Fin n)
finRange 
n: ā„•
n) : 
List: Type ?u.10 ā†’ Type ?u.10
List (
Fin: ā„• ā†’ Type
Fin 
n: ā„•
n)).
map: {Ī± : Type ?u.13} ā†’ {Ī² : Type ?u.12} ā†’ (Ī± ā†’ Ī²) ā†’ List Ī± ā†’ List Ī²
map (
Fin.val: {n : ā„•} ā†’ Fin n ā†’ ā„•
Fin.val) = 
List.range: ā„• ā†’ List ā„•
List.range 
n: ā„•
n := 
Goals accomplished! šŸ™
Ī±: Type u

n: ā„•

map Fin.val (finRange n) = range n
Ī±: Type u

n: ā„•

map Fin.val (finRange n) = range n
Ī±: Type u

n: ā„•

map Fin.val (pmap Fin.mk (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n)) = range n
Ī±: Type u

n: ā„•

map Fin.val (finRange n) = range n
Ī±: Type u

n: ā„•

pmap (fun a h => a) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n) = range n
Ī±: Type u

n: ā„•

map Fin.val (finRange n) = range n
Ī±: Type u

n: ā„•

map (fun a => a) (range n) = range n
Ī±: Type u

n: ā„•

map (fun a => a) (range n) = range n
Ī±: Type u

n: ā„•

map Fin.val (finRange n) = range n
Goals accomplished! šŸ™

#align list.map_coe_fin_range 
List.map_coe_finRange: āˆ€ (n : ā„•), map Fin.val (finRange n) = range n
List.map_coe_finRange

theorem 
finRange_succ_eq_map: āˆ€ (n : ā„•), finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
finRange_succ_eq_map (
n: ā„•
n : 
ā„•: Type
ā„•) : 
finRange: (n : ā„•) ā†’ List (Fin n)
finRange 
n: ā„•
n.
succ: ā„• ā†’ ā„•
succ = 
0: ?m.498
0 :: (
finRange: (n : ā„•) ā†’ List (Fin n)
finRange 
n: ā„•
n).
map: {Ī± : Type ?u.508} ā†’ {Ī² : Type ?u.507} ā†’ (Ī± ā†’ Ī²) ā†’ List Ī± ā†’ List Ī²
map 
Fin.succ: {n : ā„•} ā†’ Fin n ā†’ Fin (Nat.succ n)
Fin.succ := 
Goals accomplished! šŸ™
Ī±: Type u

n: ā„•

finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = ā†‘0 :: map Fin.val (map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
range (Nat.succ n) = ā†‘0 :: map Fin.val (map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
0 :: map Nat.succ (range n) = ā†‘0 :: map Fin.val (map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
0 :: map Nat.succ (range n) = 0 :: map Fin.val (map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
0 :: map Nat.succ (map Fin.val (finRange n)) = 0 :: map Fin.val (map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
0 :: map (Nat.succ āˆ˜ Fin.val) (finRange n) = 0 :: map Fin.val (map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
Ī±: Type u

n: ā„•

a
0 :: map (Nat.succ āˆ˜ Fin.val) (finRange n) = 0 :: map (Fin.val āˆ˜ Fin.succ) (finRange n)
Ī±: Type u

n: ā„•

a
0 :: map (Nat.succ āˆ˜ Fin.val) (finRange n) = 0 :: map (Fin.val āˆ˜ Fin.succ) (finRange n)
Ī±: Type u

n: ā„•

finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
Goals accomplished! šŸ™

#align list.fin_range_succ_eq_map 
List.finRange_succ_eq_map: āˆ€ (n : ā„•), finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
List.finRange_succ_eq_map

-- Porting note : `map_nth_le` moved to `List.finRange_map_get` in Data.List.Range

theorem 
ofFn_eq_pmap: āˆ€ {Ī± : Type u_1} {n : ā„•} {f : Fin n ā†’ Ī±},
  ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n)
ofFn_eq_pmap {
Ī±: ?m.851
Ī± 
n: ā„•
n} {
f: Fin n ā†’ Ī±
f : 
Fin: ā„• ā†’ Type
Fin 
n: ?m.854
n ā†’ 
Ī±: ?m.851
Ī±} :
    
ofFn: {Ī± : Type ?u.862} ā†’ {n : ā„•} ā†’ (Fin n ā†’ Ī±) ā†’ List Ī±
ofFn 
f: Fin n ā†’ Ī±
f = 
pmap: {Ī± : Type ?u.870} ā†’
  {Ī² : Type ?u.869} ā†’ {p : Ī± ā†’ Prop} ā†’ ((a : Ī±) ā†’ p a ā†’ Ī²) ā†’ (l : List Ī±) ā†’ (āˆ€ (a : Ī±), a āˆˆ l ā†’ p a) ā†’ List Ī²
pmap (fun 
i: ?m.875
i 
hi: ?m.878
hi => 
f: Fin n ā†’ Ī±
f āŸØ
i: ?m.875
i, 
hi: ?m.878
hiāŸ©) (
range: ā„• ā†’ List ā„•
range 
n: ?m.854
n) fun 
_: ?m.892
_ => 
mem_range: āˆ€ {m n : ā„•}, m āˆˆ range n ā†” m < n
mem_range.
1: āˆ€ {a b : Prop}, (a ā†” b) ā†’ a ā†’ b
1 := 
Goals accomplished! šŸ™
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map (fun x => f { val := ā†‘x, isLt := (_ : ā†‘x < n) }) (attach (range n))
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map (fun x => f { val := ā†‘x, isLt := (_ : ā†‘x < n) }) (attach (range n))
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map (fun x => f { val := ā†‘x, isLt := (_ : ā†‘x < n) }) (attach (range n))
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map (fun x => f { val := ā†‘x, isLt := (_ : ā†‘x < n) }) (attach (range n))
Goals accomplished! šŸ™
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

length (ofFn f) = length (map (fun x => f { val := ā†‘x, isLt := (_ : ā†‘x < n) }) (attach (range n)))
Goals accomplished! šŸ™
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map (fun x => f { val := ā†‘x, isLt := (_ : ā†‘x < n) }) (attach (range n))
Goals accomplished! šŸ™
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

i: ā„•

hi1: i < length (ofFn f)

hi2: i < length (map (fun x => f { val := ā†‘x, isLt := (_ : ā†‘x < n) }) (attach (range n)))

get (ofFn f) { val := i, isLt := hi1 } =   get (map (fun x => f { val := ā†‘x, isLt := (_ : ā†‘x < n) }) (attach (range n))) { val := i, isLt := hi2 }
Goals accomplished! šŸ™
Goals accomplished! šŸ™

#align list.of_fn_eq_pmap 
List.ofFn_eq_pmap: āˆ€ {Ī± : Type u_1} {n : ā„•} {f : Fin n ā†’ Ī±},
  ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n)
List.ofFn_eq_pmap

theorem 
ofFn_id: āˆ€ (n : ā„•), ofFn id = finRange n
ofFn_id (
n: ?m.2312
n) : 
ofFn: {Ī± : Type ?u.2316} ā†’ {n : ā„•} ā†’ (Fin n ā†’ Ī±) ā†’ List Ī±
ofFn 
id: {Ī± : Sort ?u.2319} ā†’ Ī± ā†’ Ī±
id = 
finRange: (n : ā„•) ā†’ List (Fin n)
finRange 
n: ?m.2312
n :=
  
ofFn_eq_pmap: āˆ€ {Ī± : Type ?u.2352} {n : ā„•} {f : Fin n ā†’ Ī±},
  ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n)
ofFn_eq_pmap
#align list.of_fn_id 
List.ofFn_id: āˆ€ (n : ā„•), ofFn id = finRange n
List.ofFn_id

theorem 
ofFn_eq_map: āˆ€ {Ī± : Type u_1} {n : ā„•} {f : Fin n ā†’ Ī±}, ofFn f = map f (finRange n)
ofFn_eq_map {
Ī±: Type u_1
Ī± 
n: ?m.2420
n} {
f: Fin n ā†’ Ī±
f : 
Fin: ā„• ā†’ Type
Fin 
n: ?m.2420
n ā†’ 
Ī±: ?m.2417
Ī±} : 
ofFn: {Ī± : Type ?u.2428} ā†’ {n : ā„•} ā†’ (Fin n ā†’ Ī±) ā†’ List Ī±
ofFn 
f: Fin n ā†’ Ī±
f = (
finRange: (n : ā„•) ā†’ List (Fin n)
finRange 
n: ?m.2420
n).
map: {Ī± : Type ?u.2436} ā†’ {Ī² : Type ?u.2435} ā†’ (Ī± ā†’ Ī²) ā†’ List Ī± ā†’ List Ī²
map 
f: Fin n ā†’ Ī±
f := 
Goals accomplished! šŸ™
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map f (finRange n)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map f (finRange n)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map f (ofFn id)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map f (finRange n)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = ofFn (f āˆ˜ id)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = map f (finRange n)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

ofFn f = ofFn f
Goals accomplished! šŸ™

#align list.of_fn_eq_map 
List.ofFn_eq_map: āˆ€ {Ī± : Type u_1} {n : ā„•} {f : Fin n ā†’ Ī±}, ofFn f = map f (finRange n)
List.ofFn_eq_map

theorem 
nodup_ofFn_ofInjective: āˆ€ {Ī± : Type u_1} {n : ā„•} {f : Fin n ā†’ Ī±}, Function.Injective f ā†’ Nodup (ofFn f)
nodup_ofFn_ofInjective {
Ī±: ?m.2523
Ī± 
n: ?m.2526
n} {
f: Fin n ā†’ Ī±
f : 
Fin: ā„• ā†’ Type
Fin 
n: ?m.2526
n ā†’ 
Ī±: ?m.2523
Ī±} (
hf: Function.Injective f
hf : 
Function.Injective: {Ī± : Sort ?u.2534} ā†’ {Ī² : Sort ?u.2533} ā†’ (Ī± ā†’ Ī²) ā†’ Prop
Function.Injective 
f: Fin n ā†’ Ī±
f) :
    
Nodup: {Ī± : Type ?u.2542} ā†’ List Ī± ā†’ Prop
Nodup (
ofFn: {Ī± : Type ?u.2544} ā†’ {n : ā„•} ā†’ (Fin n ā†’ Ī±) ā†’ List Ī±
ofFn 
f: Fin n ā†’ Ī±
f) := 
Goals accomplished! šŸ™
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

hf: Function.Injective f

Nodup (ofFn f)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

hf: Function.Injective f

Nodup (ofFn f)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

hf: Function.Injective f

Nodup (pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n))
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

hf: Function.Injective f

Nodup (pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : āˆ€ (x : ā„•), x āˆˆ range n ā†’ x < n))
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

hf: Function.Injective f

Nodup (ofFn f)
Goals accomplished! šŸ™

#align list.nodup_of_fn_of_injective 
List.nodup_ofFn_ofInjective: āˆ€ {Ī± : Type u_1} {n : ā„•} {f : Fin n ā†’ Ī±}, Function.Injective f ā†’ Nodup (ofFn f)
List.nodup_ofFn_ofInjective

theorem 
nodup_ofFn: āˆ€ {Ī± : Type u_1} {n : ā„•} {f : Fin n ā†’ Ī±}, Nodup (ofFn f) ā†” Function.Injective f
nodup_ofFn {
Ī±: Type u_1
Ī± 
n: ā„•
n} {
f: Fin n ā†’ Ī±
f : 
Fin: ā„• ā†’ Type
Fin 
n: ?m.2681
n ā†’ 
Ī±: ?m.2678
Ī±} : 
Nodup: {Ī± : Type ?u.2688} ā†’ List Ī± ā†’ Prop
Nodup (
ofFn: {Ī± : Type ?u.2690} ā†’ {n : ā„•} ā†’ (Fin n ā†’ Ī±) ā†’ List Ī±
ofFn 
f: Fin n ā†’ Ī±
f) ā†” 
Function.Injective: {Ī± : Sort ?u.2700} ā†’ {Ī² : Sort ?u.2699} ā†’ (Ī± ā†’ Ī²) ā†’ Prop
Function.Injective 
f: Fin n ā†’ Ī±
f := 
Goals accomplished! šŸ™
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

Nodup (ofFn f) ā†” Function.Injective f
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

Nodup (ofFn f) ā†’ Function.Injective f
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

Nodup (ofFn f) ā†” Function.Injective f
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

refine'_1
Nodup (ofFn Fin.elim0) ā†’ Function.Injective Fin.elim0
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

refine'_2
Nodup (ofFn (Fin.cons xā‚€ xs)) ā†’ Function.Injective (Fin.cons xā‚€ xs)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

Nodup (ofFn f) ā†” Function.Injective f
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

refine'_1
Nodup (ofFn Fin.elim0) ā†’ Function.Injective Fin.elim0
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

refine'_1
Nodup (ofFn Fin.elim0) ā†’ Function.Injective Fin.elim0
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

refine'_2
Nodup (ofFn (Fin.cons xā‚€ xs)) ā†’ Function.Injective (Fin.cons xā‚€ xs)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

aāœ: Nodup (ofFn Fin.elim0)

refine'_1
Function.Injective Fin.elim0
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

refine'_1
Nodup (ofFn Fin.elim0) ā†’ Function.Injective Fin.elim0
Goals accomplished! šŸ™
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

Nodup (ofFn f) ā†” Function.Injective f
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

refine'_2
Nodup (ofFn (Fin.cons xā‚€ xs)) ā†’ Function.Injective (Fin.cons xā‚€ xs)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

refine'_2
Nodup (ofFn (Fin.cons xā‚€ xs)) ā†’ Function.Injective (Fin.cons xā‚€ xs)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Function.Injective (Fin.cons xā‚€ xs)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

refine'_2
Nodup (ofFn (Fin.cons xā‚€ xs)) ā†’ Function.Injective (Fin.cons xā‚€ xs)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Function.Injective (Fin.cons xā‚€ xs)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

refine'_2
Nodup (ofFn (Fin.cons xā‚€ xs)) ā†’ Function.Injective (Fin.cons xā‚€ xs)
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (Fin.cons xā‚€ xs 0 :: ofFn fun i => Fin.cons xā‚€ xs (Fin.succ i))

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (Fin.cons xā‚€ xs 0 :: ofFn fun i => xs i)

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: (Ā¬Fin.cons xā‚€ xs 0 āˆˆ ofFn fun i => xs i) āˆ§ Nodup (ofFn fun i => xs i)

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: (Ā¬xā‚€ āˆˆ ofFn fun i => xs i) āˆ§ Nodup (ofFn fun i => xs i)

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: Nodup (ofFn (Fin.cons xā‚€ xs))

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: (Ā¬xā‚€ āˆˆ Set.range fun i => xs i) āˆ§ Nodup (ofFn fun i => xs i)

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

h: (Ā¬xā‚€ āˆˆ Set.range fun i => xs i) āˆ§ Nodup (ofFn fun i => xs i)

refine'_2
Ā¬xā‚€ āˆˆ Set.range xs āˆ§ Function.Injective xs
Ī±āœ: Type u

Ī±: Type u_1

n: ā„•

f: Fin n ā†’ Ī±

nāœ: ā„•

xā‚€: Ī±

xs: Fin nāœ ā†’ Ī±

ih: Nodup (ofFn xs) ā†’ Function.Injective xs

refine'_2
Nodup (ofFn (Fin.cons xā‚€ xs)) ā†’ Function.Injective (Fin.cons xā‚€ xs)
Goals accomplished! šŸ™

#align list.nodup_of_fn 
List.nodup_ofFn: āˆ€ {Ī± : Type u_1} {n : ā„•} {f : Fin n ā†’ Ī±}, Nodup (ofFn f) ā†” Function.Injective f
List.nodup_ofFn

end List

open List

theorem 
Equiv.Perm.map_finRange_perm: āˆ€ {n : ā„•} (Ļƒ : Perm (Fin n)), map (ā†‘Ļƒ) (finRange n) ~ finRange n
Equiv.Perm.map_finRange_perm {
n: ā„•
n : 
ā„•: Type
ā„•} (
Ļƒ: Perm (Fin n)
Ļƒ : 
Equiv.Perm: Sort ?u.3610 ā†’ Sort (max1?u.3610)
Equiv.Perm (
Fin: ā„• ā†’ Type
Fin 
n: ā„•
n)) :
    
map: {Ī± : Type ?u.3616} ā†’ {Ī² : Type ?u.3615} ā†’ (Ī± ā†’ Ī²) ā†’ List Ī± ā†’ List Ī²
map 
Ļƒ: Perm (Fin n)
Ļƒ (
finRange: (n : ā„•) ā†’ List (Fin n)
finRange 
n: ā„•
n) ~ 
finRange: (n : ā„•) ā†’ List (Fin n)
finRange 
n: ā„•
n := 
Goals accomplished! šŸ™
n: ā„•

Ļƒ: Perm (Fin n)

map (ā†‘Ļƒ) (finRange n) ~ finRange n
n: ā„•

Ļƒ: Perm (Fin n)

map (ā†‘Ļƒ) (finRange n) ~ finRange n
n: ā„•

Ļƒ: Perm (Fin n)

āˆ€ (a : Fin n), a āˆˆ map (ā†‘Ļƒ) (finRange n) ā†” a āˆˆ finRange n
n: ā„•

Ļƒ: Perm (Fin n)

āˆ€ (a : Fin n), a āˆˆ map (ā†‘Ļƒ) (finRange n) ā†” a āˆˆ finRange n
n: ā„•

Ļƒ: Perm (Fin n)

map (ā†‘Ļƒ) (finRange n) ~ finRange n
Goals accomplished! šŸ™

#align equiv.perm.map_fin_range_perm 
Equiv.Perm.map_finRange_perm: āˆ€ {n : ā„•} (Ļƒ : Equiv.Perm (Fin n)), map (ā†‘Ļƒ) (finRange n) ~ finRange n
Equiv.Perm.map_finRange_perm

/-- The list obtained from a permutation of a tuple `f` is permutation equivalent to
the list obtained from `f`. -/
theorem 
Equiv.Perm.ofFn_comp_perm: āˆ€ {n : ā„•} {Ī± : Type u} (Ļƒ : Perm (Fin n)) (f : Fin n ā†’ Ī±), ofFn (f āˆ˜ ā†‘Ļƒ) ~ ofFn f
Equiv.Perm.ofFn_comp_perm {
n: ā„•
n : 
ā„•: Type
ā„•} {
Ī±: Type u
Ī± : 
Type u: Type (u+1)
Type u} (
Ļƒ: Perm (Fin n)
Ļƒ : 
Equiv.Perm: Sort ?u.8670 ā†’ Sort (max1?u.8670)
Equiv.Perm (
Fin: ā„• ā†’ Type
Fin 
n: ā„•
n)) (
f: Fin n ā†’ Ī±
f : 
Fin: ā„• ā†’ Type
Fin 
n: ā„•
n ā†’ 
Ī±: Type u
Ī±) :
    
ofFn: {Ī± : Type ?u.8679} ā†’ {n : ā„•} ā†’ (Fin n ā†’ Ī±) ā†’ List Ī±
ofFn (
f: Fin n ā†’ Ī±
f āˆ˜ 
Ļƒ: Perm (Fin n)
Ļƒ) ~ 
ofFn: {Ī± : Type ?u.8781} ā†’ {n : ā„•} ā†’ (Fin n ā†’ Ī±) ā†’ List Ī±
ofFn 
f: Fin n ā†’ Ī±
f := 
Goals accomplished! šŸ™
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

ofFn (f āˆ˜ ā†‘Ļƒ) ~ ofFn f
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

ofFn (f āˆ˜ ā†‘Ļƒ) ~ ofFn f
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

map (f āˆ˜ ā†‘Ļƒ) (finRange n) ~ ofFn f
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

ofFn (f āˆ˜ ā†‘Ļƒ) ~ ofFn f
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

map (f āˆ˜ ā†‘Ļƒ) (finRange n) ~ map f (finRange n)
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

ofFn (f āˆ˜ ā†‘Ļƒ) ~ ofFn f
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

map f (map (ā†‘Ļƒ) (finRange n)) ~ map f (finRange n)
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

map f (map (ā†‘Ļƒ) (finRange n)) ~ map f (finRange n)
n: ā„•

Ī±: Type u

Ļƒ: Perm (Fin n)

f: Fin n ā†’ Ī±

ofFn (f āˆ˜ ā†‘Ļƒ) ~ ofFn f
Goals accomplished! šŸ™

#align equiv.perm.of_fn_comp_perm 
Equiv.Perm.ofFn_comp_perm: āˆ€ {n : ā„•} {Ī± : Type u} (Ļƒ : Equiv.Perm (Fin n)) (f : Fin n ā†’ Ī±), ofFn (f āˆ˜ ā†‘Ļƒ) ~ ofFn f
Equiv.Perm.ofFn_comp_perm