[GOAL]
α : Type u
n : ℕ
⊢ map Fin.val (finRange n) = range n
[PROOFSTEP]
simp_rw [finRange, map_pmap, pmap_eq_map]
[GOAL]
α : Type u
n : ℕ
⊢ map (fun a => a) (range n) = range n
[PROOFSTEP]
exact List.map_id _
[GOAL]
α : Type u
n : ℕ
⊢ finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
[PROOFSTEP]
apply map_injective_iff.mpr Fin.val_injective
[GOAL]
case a
α : Type u
n : ℕ
⊢ map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
[PROOFSTEP]
rw [map_cons, map_coe_finRange, range_succ_eq_map, Fin.val_zero, ← map_coe_finRange, map_map, map_map]
[GOAL]
case a
α : Type u
n : ℕ
⊢ 0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)
[PROOFSTEP]
simp only [Function.comp, Fin.val_succ]
[GOAL]
α✝ : 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)
[PROOFSTEP]
rw [pmap_eq_map_attach]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))
[PROOFSTEP]
exact ext_get (by simp) fun i hi1 hi2 => by simp [get_ofFn f ⟨i, hi1⟩]
[GOAL]
α✝ : 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)))
[PROOFSTEP]
simp
[GOAL]
α✝ : 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 }
[PROOFSTEP]
simp [get_ofFn f ⟨i, hi1⟩]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (finRange n)
[PROOFSTEP]
rw [← ofFn_id, map_ofFn, Function.right_id]
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ Nodup (ofFn f)
[PROOFSTEP]
rw [ofFn_eq_pmap]
[GOAL]
α✝ : 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))
[PROOFSTEP]
exact (nodup_range n).pmap fun _ _ _ _ H => Fin.veq_of_eq <| hf H
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn f) ↔ Function.Injective f
[PROOFSTEP]
refine' ⟨_, nodup_ofFn_ofInjective⟩
[GOAL]
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn f) → Function.Injective f
[PROOFSTEP]
refine' Fin.consInduction _ (fun x₀ xs ih => _) f
[GOAL]
case refine'_1
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn Fin.elim0) → Function.Injective Fin.elim0
[PROOFSTEP]
intro _
[GOAL]
case refine'_1
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
a✝ : Nodup (ofFn Fin.elim0)
⊢ Function.Injective Fin.elim0
[PROOFSTEP]
exact Function.injective_of_subsingleton _
[GOAL]
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
⊢ Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
α✝ : 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))
⊢ Function.Injective (Fin.cons x₀ xs)
[PROOFSTEP]
rw [Fin.cons_injective_iff]
[GOAL]
case refine'_2
α✝ : 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))
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
[PROOFSTEP]
simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h 
[GOAL]
case refine'_2
α✝ : 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)
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
[PROOFSTEP]
exact h.imp_right ih
[GOAL]
n : ℕ
σ : Perm (Fin n)
⊢ map (↑σ) (finRange n) ~ finRange n
[PROOFSTEP]
rw [perm_ext ((nodup_finRange n).map σ.injective) <| nodup_finRange n]
[GOAL]
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (↑σ) (finRange n) ↔ a ∈ finRange n
[PROOFSTEP]
simpa [mem_map, mem_finRange, true_and_iff, iff_true_iff] using σ.surjective
[GOAL]
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ ofFn (f ∘ ↑σ) ~ ofFn f
[PROOFSTEP]
rw [ofFn_eq_map, ofFn_eq_map, ← map_map]
[GOAL]
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (↑σ) (finRange n)) ~ map f (finRange n)
[PROOFSTEP]
exact σ.map_finRange_perm.map f
