[GOAL]
α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
⊢ ∀ {x : α}, ↑f x ≠ x ↔ ↑(↑(permCongr e) f) (↑e x) ≠ ↑e x
[PROOFSTEP]
intro b
[GOAL]
α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
b : α
⊢ ↑f b ≠ b ↔ ↑(↑(permCongr e) f) (↑e b) ≠ ↑e b
[PROOFSTEP]
simp only [ne_eq, permCongr_apply, symm_apply_apply, EmbeddingLike.apply_eq_iff_eq]
[GOAL]
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑(derangements (Subtype p)) ≃ { f // ∀ (a : α), a ∈ fixedPoints ↑↑f → ¬p a }
[PROOFSTEP]
refine' (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ False
[PROOFSTEP]
refine' hf ⟨a, ha⟩ (Subtype.ext _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ ↑(↑f { val := a, property := ha }) = ↑{ val := a, property := ha }
[PROOFSTEP]
simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm, Equiv.coe_fn_mk, Perm.ofSubtype_apply_of_mem _ ha] at
  hfa 
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
ha : p a
hfa : ↑(↑f { val := a, property := ha }) = a
⊢ ↑(↑f { val := a, property := ha }) = ↑{ val := a, property := ha }
[PROOFSTEP]
assumption
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
⊢ (∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a) → f ∈ derangements (Subtype p)
[PROOFSTEP]
rintro hf ⟨a, ha⟩ hfa
[GOAL]
case refine'_2.mk
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a
a : α
ha : p a
hfa : ↑f { val := a, property := ha } = { val := a, property := ha }
⊢ False
[PROOFSTEP]
refine' hf _ _ ha
[GOAL]
case refine'_2.mk
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a
a : α
ha : p a
hfa : ↑f { val := a, property := ha } = { val := a, property := ha }
⊢ a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f)
[PROOFSTEP]
simp only [Perm.subtypeEquivSubtypePerm_apply_coe, mem_fixedPoints]
[GOAL]
case refine'_2.mk
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a
a : α
ha : p a
hfa : ↑f { val := a, property := ha } = { val := a, property := ha }
⊢ IsFixedPt (↑(↑Perm.ofSubtype f)) a
[PROOFSTEP]
dsimp [IsFixedPt]
[GOAL]
case refine'_2.mk
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a
a : α
ha : p a
hfa : ↑f { val := a, property := ha } = { val := a, property := ha }
⊢ ↑(↑Perm.ofSubtype f) a = a
[PROOFSTEP]
simp_rw [Perm.ofSubtype_apply_of_mem _ ha, hfa]
[GOAL]
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ (∃ _h, ∀ (a : α), a ∈ fixedPoints ↑f → ¬p a) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ↑f
[PROOFSTEP]
simp_rw [exists_prop, ← forall_and, ← iff_iff_implies_and_implies]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∈ fixedPoints ↑↑f } ⊕ { f // ¬a ∈ fixedPoints ↑↑f } ≃
    { f // fixedPoints ↑f ⊆ {a} ∧ a ∈ fixedPoints ↑f } ⊕ { f // fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f }
[PROOFSTEP]
refine' Equiv.sumCongr _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∈ fixedPoints ↑↑f } ≃ { f // fixedPoints ↑f ⊆ {a} ∧ a ∈ fixedPoints ↑f }
[PROOFSTEP]
exact subtypeSubtypeEquivSubtypeInter (fun x : Perm α => fixedPoints x ⊆ { a }) (a ∈ fixedPoints ·)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // ¬a ∈ fixedPoints ↑↑f } ≃ { f // fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f }
[PROOFSTEP]
exact subtypeSubtypeEquivSubtypeInter (fun x : Perm α => fixedPoints x ⊆ { a }) (¬a ∈ fixedPoints ·)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // fixedPoints ↑f ⊆ {a} ∧ a ∈ fixedPoints ↑f } ⊕ { f // fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f } ≃
    { f // fixedPoints ↑f = {a} } ⊕ { f // fixedPoints ↑f = ∅ }
[PROOFSTEP]
refine' Equiv.sumCongr (subtypeEquivRight fun f => _) (subtypeEquivRight fun f => _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ↑f ⊆ {a} ∧ a ∈ fixedPoints ↑f ↔ fixedPoints ↑f = {a}
[PROOFSTEP]
rw [Set.eq_singleton_iff_unique_mem, and_comm]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ a ∈ fixedPoints ↑f ∧ fixedPoints ↑f ⊆ {a} ↔ a ∈ fixedPoints ↑f ∧ ∀ (x : α), x ∈ fixedPoints ↑f → x = a
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f ↔ fixedPoints ↑f = ∅
[PROOFSTEP]
rw [Set.eq_empty_iff_forall_not_mem]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f ↔ ∀ (x : α), ¬x ∈ fixedPoints ↑f
[PROOFSTEP]
refine' ⟨fun h x hx => h.2 (h.1 hx ▸ hx), fun h => ⟨fun x hx => (h _ hx).elim, h _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // fixedPoints ↑f = {a} } ⊕ { f // fixedPoints ↑f = ∅ } ≃ ↑(derangements ↑{a}ᶜ) ⊕ ↑(derangements α)
[PROOFSTEP]
refine'
  Equiv.sumCongr ((derangements.subtypeEquiv (· ∈ ({ a }ᶜ : Set α))).trans <| subtypeEquivRight fun x => _).symm
    (subtypeEquivRight fun f => mem_derangements_iff_fixedPoints_eq_empty.symm)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), ¬a_1 ∈ {a}ᶜ ↔ a_1 ∈ fixedPoints ↑x) ↔ fixedPoints ↑x = {a}
[PROOFSTEP]
rw [eq_comm, Set.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), ¬a_1 ∈ {a}ᶜ ↔ a_1 ∈ fixedPoints ↑x) ↔ ∀ (x_1 : α), x_1 ∈ {a} ↔ x_1 ∈ fixedPoints ↑x
[PROOFSTEP]
simp_rw [Set.mem_compl_iff, Classical.not_not]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : Option α
f : Perm α
⊢ f ∈ fiber a ↔ ∃ F, F ∈ derangements (Option α) ∧ ↑F none = a ∧ removeNone F = f
[PROOFSTEP]
simp [RemoveNone.fiber, derangements]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ fiber none = ∅
[PROOFSTEP]
rw [Set.eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), ¬x ∈ fiber none
[PROOFSTEP]
intro f hyp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
f : Perm α
hyp : f ∈ fiber none
⊢ False
[PROOFSTEP]
rw [RemoveNone.mem_fiber] at hyp 
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
f : Perm α
hyp : ∃ F, F ∈ derangements (Option α) ∧ ↑F none = none ∧ removeNone F = f
⊢ False
[PROOFSTEP]
rcases hyp with ⟨F, F_derangement, F_none, _⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = none
right✝ : removeNone F = f
⊢ False
[PROOFSTEP]
exact F_derangement none F_none
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ fiber (some a) = {f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
ext f
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) ↔ f ∈ {f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) → f ∈ {f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
rw [RemoveNone.mem_fiber]
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ (∃ F, F ∈ derangements (Option α) ∧ ↑F none = some a ∧ removeNone F = f) → f ∈ {f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
rintro ⟨F, F_derangement, F_none, rfl⟩ x x_fixed
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : x ∈ fixedPoints ↑(removeNone F)
⊢ x ∈ {a}
[PROOFSTEP]
rw [mem_fixedPoints_iff] at x_fixed 
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : ↑(removeNone F) x = x
⊢ x ∈ {a}
[PROOFSTEP]
apply_fun some at x_fixed 
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : some (↑(removeNone F) x) = some x
⊢ x ∈ {a}
[PROOFSTEP]
cases' Fx : F (some x) with y
[GOAL]
case h.mp.intro.intro.intro.none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : some (↑(removeNone F) x) = some x
Fx : ↑F (some x) = none
⊢ x ∈ {a}
[PROOFSTEP]
rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed 
[GOAL]
case h.mp.intro.intro.intro.some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : some (↑(removeNone F) x) = some x
y : α
Fx : ↑F (some x) = some y
⊢ x ∈ {a}
[PROOFSTEP]
exfalso
[GOAL]
case h.mp.intro.intro.intro.some.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : some (↑(removeNone F) x) = some x
y : α
Fx : ↑F (some x) = some y
⊢ False
[PROOFSTEP]
rw [removeNone_some F ⟨y, Fx⟩] at x_fixed 
[GOAL]
case h.mp.intro.intro.intro.some.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : ↑F (some x) = some x
y : α
Fx : ↑F (some x) = some y
⊢ False
[PROOFSTEP]
exact F_derangement _ x_fixed
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ {f | fixedPoints ↑f ⊆ {a}} → f ∈ fiber (some a)
[PROOFSTEP]
intro h_opfp
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ f ∈ fiber (some a)
[PROOFSTEP]
use Equiv.Perm.decomposeOption.symm (some a, f)
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α) ∧
    ↑Perm.decomposeOption (↑Perm.decomposeOption.symm (some a, f)) = (some a, f)
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α)
[PROOFSTEP]
intro x
[GOAL]
case h.left
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : Option α
⊢ ↑(↑Perm.decomposeOption.symm (some a, f)) x ≠ x
[PROOFSTEP]
apply_fun fun x => Equiv.swap none (some a) x
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : Option α
⊢ (fun x => ↑(Equiv.swap none (some a)) x) (↑(↑Perm.decomposeOption.symm (some a, f)) x) ≠
    (fun x => ↑(Equiv.swap none (some a)) x) x
[PROOFSTEP]
simp only [Perm.decomposeOption_symm_apply, swap_apply_self, Perm.coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : Option α
⊢ ↑(Equiv.swap none (some a)) ((↑(Equiv.swap none (some a)) ∘ ↑(optionCongr f)) x) ≠ ↑(Equiv.swap none (some a)) x
[PROOFSTEP]
cases' x with x
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑(Equiv.swap none (some a)) ((↑(Equiv.swap none (some a)) ∘ ↑(optionCongr f)) none) ≠ ↑(Equiv.swap none (some a)) none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
⊢ ↑(Equiv.swap none (some a)) ((↑(Equiv.swap none (some a)) ∘ ↑(optionCongr f)) (some x)) ≠
    ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
simp only [comp, optionCongr_apply, Option.map_some', swap_apply_self]
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
by_cases x_vs_a : x = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
rw [x_vs_a, swap_apply_right]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (↑f a) ≠ none
[PROOFSTEP]
apply Option.some_ne_none
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
have ne_1 : some x ≠ none := Option.some_ne_none _
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ ↑f x ≠ x
[PROOFSTEP]
intro contra
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
contra : ↑f x = x
⊢ False
[PROOFSTEP]
exact x_vs_a (h_opfp contra)
[GOAL]
case h.right
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption (↑Perm.decomposeOption.symm (some a, f)) = (some a, f)
[PROOFSTEP]
rw [apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ↑(derangements (Option α)) ≃ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
have fiber_none_is_false : Equiv.RemoveNone.fiber (@none α) → False :=
  by
  rw [Equiv.RemoveNone.fiber_none]
  exact IsEmpty.false
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ↑(Equiv.RemoveNone.fiber none) → False
[PROOFSTEP]
rw [Equiv.RemoveNone.fiber_none]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ↑∅ → False
[PROOFSTEP]
exact IsEmpty.false
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ↑(Equiv.RemoveNone.fiber none) → False
⊢ ↑(derangements (Option α)) ≃ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
calc
  derangements (Option α) ≃ Equiv.Perm.decomposeOption '' derangements (Option α) := Equiv.image _ _
  _ ≃ Σ a : Option α, ↥(Equiv.RemoveNone.fiber a) := (setProdEquivSigma _)
  _ ≃ Σ a : α, ↥(Equiv.RemoveNone.fiber (some a)) := (sigmaOptionEquivOfSome _ fiber_none_is_false)
  _ ≃ Σ a : α, {f : Perm α | fixedPoints f ⊆ { a }} :=
    by
    simp_rw [Equiv.RemoveNone.fiber_some]
    rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ↑(Equiv.RemoveNone.fiber none) → False
⊢ (a : α) × ↑(Equiv.RemoveNone.fiber (some a)) ≃ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
simp_rw [Equiv.RemoveNone.fiber_some]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ↑(Equiv.RemoveNone.fiber none) → False
⊢ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}} ≃ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
rfl
