awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf :
  ∀ (a : α),
    Membership.mem (γ := Set α)
        (fixedPoints
          (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                      (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                    f) :
                Perm α) :
            (a : α) → α))
        a →
      ¬p a
a : α
ha : p a
hfa : (f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha) = Subtype.mk (p := p) a ha
refine_2 : IsFixedPt (⇑((Perm.ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) a
⊢ Membership.mem (γ := Set α)
    (fixedPoints
      (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
        (a : α) → α))
    a

Tactic:
simp only [Perm.subtypeEquivSubtypePerm_apply_coe, mem_fixedPoints]

Premises used: Equiv.Perm.subtypeEquivSubtypePerm_apply_coe, Function.mem_fixedPoints
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf :
  ∀ (a : α),
    Membership.mem (γ := Set α)
        (fixedPoints
          (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                      (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                    f) :
                Perm α) :
            (a : α) → α))
        a →
      ¬p a
a : α
ha : p a
hfa : (f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha) = Subtype.mk (p := p) a ha
refine_2 : (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = a
⊢ (((Perm.ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) a = a

Tactic:
simp_rw [Perm.ofSubtype_apply_of_mem _ ha, hfa]

Premises used: Equiv.Perm.ofSubtype_apply_of_mem
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm α
simp_rw :
  ((∀ (a : α), ¬p a → Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a) ∧
      ∀ (a : α), Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a → ¬p a) ↔
    ∀ (a : α), ¬p a ↔ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
simp_rw₁ :
  (∀ (x : α),
      (¬p x → Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x) ∧
        (Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x → ¬p x)) ↔
    ∀ (a : α), ¬p a ↔ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
⊢ (∃ (_ : ∀ (a : α), ¬p a → Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a),
      ∀ (a : α), Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a → ¬p a) ↔
    ∀ (a : α), ¬p a ↔ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a

Tactic:
simp_rw [exists_prop, ← forall_and, ← iff_iff_implies_and_implies]

Premises used: iff_iff_implies_and_implies, exists_prop, forall_and
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
refine_1 :
  { f : { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} } //
      Membership.mem (γ := Set α) (fixedPoints (⇑(↑f : Perm α) : (a : α) → α)) a } ≃
    { f : Perm α //
      Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧
        Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a }
refine_2 :
  { f : { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} } //
      a ∉ fixedPoints (⇑(↑f : Perm α) : (a : α) → α) } ≃
    { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) }
⊢ { f : { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} } //
        Membership.mem (γ := Set α) (fixedPoints (⇑(↑f : Perm α) : (a : α) → α)) a } ⊕
      { f : { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} } //
        a ∉ fixedPoints (⇑(↑f : Perm α) : (a : α) → α) } ≃
    { f : Perm α //
        Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧
          Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a } ⊕
      { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) }

Tactic:
refine Equiv.sumCongr ?_ ?_

Premises used: Equiv.sumCongr
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
⊢ { f : { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} } //
      Membership.mem (γ := Set α) (fixedPoints (⇑(↑f : Perm α) : (a : α) → α)) a } ≃
    { f : Perm α //
      Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧
        Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a }

Tactic:
exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (a ∈ fixedPoints ·)

Premises used: Function.fixedPoints, Membership.mem, HasSubset.Subset, Equiv.subtypeSubtypeEquivSubtypeInter, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
⊢ { f : { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} } //
      a ∉ fixedPoints (⇑(↑f : Perm α) : (a : α) → α) } ≃
    { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) }

Tactic:
exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (a ∉ fixedPoints ·)

Premises used: Function.fixedPoints, Membership.mem, HasSubset.Subset, Equiv.subtypeSubtypeEquivSubtypeInter, Singleton.singleton, DFunLike.coe, Not
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
refine_1 :
  ∀ (f : Perm α),
    Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧
        Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a ↔
      Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}
refine_2 :
  ∀ (f : Perm α),
    Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) ↔
      Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) ∅
⊢ { f : Perm α //
        Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧
          Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a } ⊕
      { f : Perm α // Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) } ≃
    { f : Perm α // Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} } ⊕
      { f : Perm α // Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) ∅ }

Tactic:
refine Equiv.sumCongr (subtypeEquivRight fun f => ?_) (subtypeEquivRight fun f => ?_)

Premises used: Equiv.subtypeEquivRight, Equiv.sumCongr
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
f : Perm α
refine_1 :
  Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a ∧
      Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ↔
    Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a ∧
      ∀ (x : α), Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x → x = a
⊢ Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧
      Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a ↔
    Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}

Tactic:
rw [Set.eq_singleton_iff_unique_mem, and_comm]

Premises used: and_comm, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
f : Perm α
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a ∧
      Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ↔
    Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a ∧
      ∀ (x : α), Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) x → x = a

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
f : Perm α
refine_2 :
  Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) ↔
    ∀ (x : α), x ∉ fixedPoints (⇑f : (a : α) → α)
⊢ Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) ↔
    Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
f : Perm α
⊢ Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) ↔
    ∀ (x : α), x ∉ fixedPoints (⇑f : (a : α) → α)

Tactic:
⟨fun h x hx => h.2 (h.1 hx ▸ hx), fun h => ⟨fun x hx => (h _ hx).elim, h _⟩⟩

Premises used: False.elim, Eq.rec, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
f : Perm α
⊢ Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) ↔
    ∀ (x : α), x ∉ fixedPoints (⇑f : (a : α) → α)

Tactic:
exact ⟨fun h x hx => h.2 (h.1 hx ▸ hx), fun h => ⟨fun x hx => (h _ hx).elim, h _⟩⟩
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
subtypeEquivRight :
  ∀ (x : Perm α),
    (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ Membership.mem (γ := Set α) (fixedPoints (⇑x : (a : α) → α)) a_1) ↔
      Eq (α := Set α) (fixedPoints (⇑x : (a : α) → α)) {a}
⊢ { f : Perm α // Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} } ⊕
      { f : Perm α // Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) ∅ } ≃
    (↑(derangements (↑{a}ᶜ : Type u_1)) : Type u_1) ⊕ (↑(derangements α) : Type u_1)

Tactic:
refine
        Equiv.sumCongr ((derangements.subtypeEquiv _).trans <|
            subtypeEquivRight fun x => ?_).symm
          (subtypeEquivRight fun f => mem_derangements_iff_fixedPoints_eq_empty.symm)

Premises used: derangements.subtypeEquiv, mem_derangements_iff_fixedPoints_eq_empty, Equiv.trans, Equiv.subtypeEquivRight, Equiv.sumCongr, Equiv.symm, Iff.symm
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
x : Perm α
rw :
  (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ Membership.mem (γ := Set α) (fixedPoints (⇑x : (a : α) → α)) a_1) ↔
    ∀ (x_1 : α), Membership.mem (γ := Set α) {a} x_1 ↔ Membership.mem (γ := Set α) (fixedPoints (⇑x : (a : α) → α)) x_1
⊢ (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ Membership.mem (γ := Set α) (fixedPoints (⇑x : (a : α) → α)) a_1) ↔
    Eq (α := Set α) (fixedPoints (⇑x : (a : α) → α)) {a}

Tactic:
rw [eq_comm, Set.ext_iff]

Premises used: eq_comm, Set.ext_iff
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : Option α
f : Perm α
⊢ f ∈ fiber a ↔
    ∃ (F : Perm (Option α)),
      Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F ∧
        (F : (a : Option α) → Option α) none = a ∧ removeNone F = f

Tactic:
simp [RemoveNone.fiber, derangements]

Premises used: derangements, derangements.Equiv.RemoveNone.fiber
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
rw : ∀ (x : Perm α), x ∉ fiber none
⊢ Eq.{u_1 + 1} (α := Set (Perm α)) (fiber none) ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
f : Perm α
hyp : Membership.mem (γ := Set (Perm α)) (fiber none) f
⊢ ∃ (F : Perm (Option α)),
    Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F ∧
      Eq (α := Option α) ((F : (a : Option α) → Option α) none : Option α) (none : Option α) ∧ removeNone F = f

Tactic:
rw [RemoveNone.mem_fiber] at hyp

Premises used: derangements.Equiv.RemoveNone.mem_fiber
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
f : Perm α
hyp :
  ∃ (F : Perm (Option α)),
    Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F ∧
      Eq (α := Option α) ((F : (a : Option α) → Option α) none : Option α) (none : Option α) ∧ removeNone F = f
rcases :
  ∀ (F : Perm (Option α)) (F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F)
    (F_none : Eq (α := Option α) ((F : (a : Option α) → Option α) none : Option α) (none : Option α)),
    removeNone F = f → False
⊢ False

Tactic:
rcases hyp with ⟨F, F_derangement, F_none, _⟩
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : Eq (α := Option α) ((F : (a : Option α) → Option α) none : Option α) (none : Option α)
right : removeNone F = f
⊢ False

Tactic:
F_derangement none F_none

Premises used: Option.none
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : Eq (α := Option α) ((F : (a : Option α) → Option α) none : Option α) (none : Option α)
right : removeNone F = f
⊢ False

Tactic:
exact F_derangement none F_none

Premises used: Option.none
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
h :
  ∀ (f : Perm α),
    f ∈ fiber (some a) ↔
      Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
⊢ fiber (some a) = {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}}

Tactic:
ext f
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h :
  f ∈ fiber (some a) →
    Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
h₁ :
  Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f →
    f ∈ fiber (some a)
⊢ f ∈ fiber (some a) ↔
    Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h :
  (∃ (F : Perm (Option α)),
      Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F ∧
        (F : (a : Option α) → Option α) none = some a ∧ removeNone F = f) →
    Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
⊢ f ∈ fiber (some a) →
    Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f

Tactic:
rw [RemoveNone.mem_fiber]

Premises used: derangements.Equiv.RemoveNone.mem_fiber
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : (F : (a : Option α) → Option α) none = some a
x : α
x_fixed : Membership.mem (γ := Set α) (fixedPoints (⇑(removeNone F) : (a : α) → α)) x
⊢ (removeNone F : (a : α) → α) x = x

Tactic:
rw [mem_fixedPoints_iff] at x_fixed

Premises used: Function.mem_fixedPoints_iff
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : (F : (a : Option α) → Option α) none = some a
x : α
x_fixed : (removeNone F : (a : α) → α) x = x
⊢ some ((removeNone F : (a : α) → α) x) = some x

Tactic:
apply_fun some at x_fixed

Premises used: Option.some
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : (F : (a : Option α) → Option α) none = some a
x : α
x_fixed : some ((removeNone F : (a : α) → α) x) = some x
h :
  ∀ (Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
    Membership.mem (γ := Set α) {a} x
h₁ : ∀ (y : α) (Fx : (F : (a : Option α) → Option α) (some x) = some y), Membership.mem (γ := Set α) {a} x
⊢ Membership.mem (γ := Set α) {a} x

Tactic:
rcases Fx : F (some x) with - | y

Premises used: Option.some, DFunLike.coe
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : (F : (a : Option α) → Option α) none = some a
x : α
x_fixed : some ((removeNone F : (a : α) → α) x) = some x
Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)
h :
  ∀ (x_fixed : (F : (a : Option α) → Option α) none = some x)
    (Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
    Membership.mem (γ := Set α) {a} x
h₁ :
  ∀ (x_fixed : some a = some x)
    (Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
    Membership.mem (γ := Set α) {a} x
h₂ :
  ∀ (x_fixed : a = x) (Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
    Membership.mem (γ := Set α) {a} x
h₃ h₄ h₅ h₆ :
  ∀ (x_fixed : x = a) (Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
    Membership.mem (γ := Set α) {a} x
⊢ Membership.mem (γ := Set α) {a} x

Tactic:
rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed

Premises used: eq_comm, Equiv.removeNone_none, Option.some_inj
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : (F : (a : Option α) → Option α) none = some a
x : α
x_fixed : some ((removeNone F : (a : α) → α) x) = some x
y : α
Fx : (F : (a : Option α) → Option α) (some x) = some y
h : False
⊢ Membership.mem (γ := Set α) {a} x

Tactic:
exfalso
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : (F : (a : Option α) → Option α) none = some a
x : α
x_fixed : some ((removeNone F : (a : α) → α) x) = some x
y : α
Fx : (F : (a : Option α) → Option α) (some x) = some y
h :
  ∀ (x_fixed : (F : (a : Option α) → Option α) (some x) = some x) (y : α)
    (Fx : (F : (a : Option α) → Option α) (some x) = some y), False
⊢ False

Tactic:
rw [removeNone_some F ⟨y, Fx⟩] at x_fixed

Premises used: Exists.intro, Equiv.removeNone_some
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : (F : (a : Option α) → Option α) none = some a
x : α
x_fixed : (F : (a : Option α) → Option α) (some x) = some x
y : α
Fx : (F : (a : Option α) → Option α) (some x) = some y
⊢ False

Tactic:
F_derangement _ x_fixed
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : Membership.mem (γ := Set (Perm (Option α))) (derangements (Option α)) F
F_none : (F : (a : Option α) → Option α) none = some a
x : α
x_fixed : (F : (a : Option α) → Option α) (some x) = some x
y : α
Fx : (F : (a : Option α) → Option α) (some x) = some y
⊢ False

Tactic:
exact F_derangement _ x_fixed
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h_opfp : Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
h :
  Membership.mem (α := Perm (Option α)) (γ := Set (Perm (Option α))) (derangements (Option α))
      ((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) ∧
    (Perm.decomposeOption : (a : Perm (Option α)) → Option α × Perm α)
        ((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) =
      (some a, f)
⊢ f ∈ fiber (some a)

Tactic:
use Equiv.Perm.decomposeOption.symm (some a, f)

Premises used: Equiv.Perm.decomposeOption, Option.some, Prod.mk, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h_opfp : Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
h :
  Membership.mem (α := Perm (Option α)) (γ := Set (Perm (Option α))) (derangements (Option α))
    ((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α))
h₁ :
  (Perm.decomposeOption : (a : Perm (Option α)) → Option α × Perm α)
      ((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) =
    (some a, f)
⊢ Membership.mem (α := Perm (Option α)) (γ := Set (Perm (Option α))) (derangements (Option α))
      ((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) ∧
    (Perm.decomposeOption : (a : Perm (Option α)) → Option α × Perm α)
        ((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) =
      (some a, f)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h_opfp : Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
x : Option α
apply_fun :
  Ne.{u_1 + 1} (α := Option α)
    ((fun (x : Option α) ↦ ((Equiv.swap none (some a) : (a : Option α) → Option α) x : Option α))
      ((((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) :
          (a : Option α) → Option α)
        x))
    ((fun (x : Option α) ↦ ((Equiv.swap none (some a) : (a : Option α) → Option α) x : Option α)) x)
⊢ (((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) :
        (a : Option α) → Option α)
      x ≠
    x

Tactic:
apply_fun fun x => Equiv.swap none (some a) x

Premises used: Equiv.swap, Option.some, Option.none, DFunLike.coe
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h_opfp : Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
x : Option α
simp :
  Ne (α := Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α)
        (comp (β := Option α) (⇑(Equiv.swap none (some a)) : (a : Option α) → Option α)
          (⇑(optionCongr f) : (a : Option α) → Option α) x) :
      Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) x : Option α)
⊢ Ne.{u_1 + 1} (α := Option α)
    ((fun (x : Option α) ↦ ((Equiv.swap none (some a) : (a : Option α) → Option α) x : Option α))
      ((((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) :
          (a : Option α) → Option α)
        x))
    ((fun (x : Option α) ↦ ((Equiv.swap none (some a) : (a : Option α) → Option α) x : Option α)) x)

Tactic:
simp only [Perm.decomposeOption_symm_apply, Perm.coe_mul]

Premises used: Equiv.Perm.coe_mul, Equiv.Perm.decomposeOption_symm_apply