no goals
α : Type u_1
β : Type ?u.70902
inst✝ : DecidableEq α
a : Option α
f : Perm α
⊢ f ∈ fiber a ↔ ∃ F, F ∈ derangements (Option α) ∧ ↑F none = a ∧ removeNone F = f
simp [RemoveNone.fiber, derangements]