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
rw [ofFn_eq_map, ofFn_eq_map, ← map_map]
no goals
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (↑σ) (finRange n)) ~ map f (finRange n)
exact σ.map_finRange_perm.map f