α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), ¬x ∈ fiber none
α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
⊢ fiber none = ∅
rw [Set.eq_empty_iff_forall_not_mem]
α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
f : Perm α
hyp : f ∈ fiber none
⊢ False
α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), ¬x ∈ fiber none
intro f hyp
α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
f : Perm α
hyp : ∃ F, F ∈ derangements (Option α) ∧ ↑F none = none ∧ removeNone F = f
⊢ False
α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
f : Perm α
hyp : f ∈ fiber none
⊢ False
rw [RemoveNone.mem_fiber] at hyp
case intro.intro.intro
α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = none
right✝ : removeNone F = f
⊢ False
α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
f : Perm α
hyp : ∃ F, F ∈ derangements (Option α) ∧ ↑F none = none ∧ removeNone F = f
⊢ False
rcases hyp with ⟨F, F_derangement, F_none, _⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.80928
inst✝ : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = none
right✝ : removeNone F = f
⊢ False
exact F_derangement none F_none