case h
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) ↔ f ∈ {f | fixedPoints ↑f ⊆ {a}}
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
⊢ fiber (some a) = {f | fixedPoints ↑f ⊆ {a}}
ext f
case h.mp
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) → f ∈ {f | fixedPoints ↑f ⊆ {a}}

case h.mpr
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ {f | fixedPoints ↑f ⊆ {a}} → f ∈ fiber (some a)
case h
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) ↔ f ∈ {f | fixedPoints ↑f ⊆ {a}}
constructor
case h.mp
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ (∃ F, F ∈ derangements (Option α) ∧ ↑F none = some a ∧ removeNone F = f) → f ∈ {f | fixedPoints ↑f ⊆ {a}}
case h.mp
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) → f ∈ {f | fixedPoints ↑f ⊆ {a}}
rw [RemoveNone.mem_fiber]
case h.mp.intro.intro.intro
α : Type u_1
β : Type ?u.81438
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}
case h.mp
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ (∃ F, F ∈ derangements (Option α) ∧ ↑F none = some a ∧ removeNone F = f) → f ∈ {f | fixedPoints ↑f ⊆ {a}}
rintro ⟨F, F_derangement, F_none, rfl⟩ x x_fixed
case h.mp.intro.intro.intro
α : Type u_1
β : Type ?u.81438
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}
case h.mp.intro.intro.intro
α : Type u_1
β : Type ?u.81438
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}
rw [mem_fixedPoints_iff] at x_fixed
case h.mp.intro.intro.intro
α : Type u_1
β : Type ?u.81438
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}
case h.mp.intro.intro.intro
α : Type u_1
β : Type ?u.81438
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}
apply_fun some  at x_fixed
case h.mp.intro.intro.intro.none
α : Type u_1
β : Type ?u.81438
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}

case h.mp.intro.intro.intro.some
α : Type u_1
β : Type ?u.81438
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}
case h.mp.intro.intro.intro
α : Type u_1
β : Type ?u.81438
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}
cases' Fx : F (some x) with y
no goals
case h.mp.intro.intro.intro.none
α : Type u_1
β : Type ?u.81438
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}
rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
case h.mp.intro.intro.intro.some.h
α : Type u_1
β : Type ?u.81438
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
case h.mp.intro.intro.intro.some
α : Type u_1
β : Type ?u.81438
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}
exfalso
case h.mp.intro.intro.intro.some.h
α : Type u_1
β : Type ?u.81438
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
case h.mp.intro.intro.intro.some.h
α : Type u_1
β : Type ?u.81438
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
rw [removeNone_some F ⟨y, Fx⟩] at x_fixed
no goals
case h.mp.intro.intro.intro.some.h
α : Type u_1
β : Type ?u.81438
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
exact F_derangement _ x_fixed
case h.mpr
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ f ∈ fiber (some a)
case h.mpr
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ {f | fixedPoints ↑f ⊆ {a}} → f ∈ fiber (some a)
intro h_opfp
case h.mpr
α : Type u_1
β : Type ?u.81438
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)
case h.mpr
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ f ∈ fiber (some a)
use Equiv.Perm.decomposeOption.symm (some a, f)
case h.mpr.left
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α)

case h.mpr.right
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption (↑Perm.decomposeOption.symm (some a, f)) = (some a, f)
case h.mpr
α : Type u_1
β : Type ?u.81438
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)
constructor
case h.mpr.left
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : Option α
⊢ ↑(↑Perm.decomposeOption.symm (some a, f)) x ≠ x
case h.mpr.left
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α)
intro x
α : Type u_1
β : Type ?u.81438
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
case h.mpr.left
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : Option α
⊢ ↑(↑Perm.decomposeOption.symm (some a, f)) x ≠ x
apply_fun fun x => Equiv.swap none (some a) x
α : Type u_1
β : Type ?u.81438
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
α : Type u_1
β : Type ?u.81438
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
simp only [Perm.decomposeOption_symm_apply, swap_apply_self, Perm.coe_mul]
case none
α : Type u_1
β : Type ?u.81438
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

case some
α : Type u_1
β : Type ?u.81438
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)
α : Type u_1
β : Type ?u.81438
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
cases' x with x
case some
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
case some
α : Type u_1
β : Type ?u.81438
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)
simp only [comp, optionCongr_apply, Option.map_some', swap_apply_self]
case pos
α : Type u_1
β : Type ?u.81438
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)

case neg
α : Type u_1
β : Type ?u.81438
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)
case some
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
by_cases x_vs_a : x = a
case neg
α : Type u_1
β : Type ?u.81438
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)
case neg
α : Type u_1
β : Type ?u.81438
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)
have ne_1 : some x ≠ none := Option.some_ne_none _
case neg
α : Type u_1
β : Type ?u.81438
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)
case neg
α : Type u_1
β : Type ?u.81438
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)
have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
case neg
α : Type u_1
β : Type ?u.81438
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
case neg
α : Type u_1
β : Type ?u.81438
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)
rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
case neg
α : Type u_1
β : Type ?u.81438
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
case neg
α : Type u_1
β : Type ?u.81438
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
intro contra
no goals
case neg
α : Type u_1
β : Type ?u.81438
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
exact x_vs_a (h_opfp contra)
no goals
case none
α : Type u_1
β : Type ?u.81438
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
simp
case pos
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (↑f a) ≠ none
case pos
α : Type u_1
β : Type ?u.81438
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)
rw [x_vs_a, swap_apply_right]
no goals
case pos
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (↑f a) ≠ none
apply Option.some_ne_none
no goals
case h.mpr.right
α : Type u_1
β : Type ?u.81438
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption (↑Perm.decomposeOption.symm (some a, f)) = (some a, f)
rw [apply_symm_apply]