awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
refine_1 :
  ∀ (f : Perm (Subtype p)) (hf : Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f) (a : α)
    (hfa :
      Membership.mem (γ := Set α)
        (fixedPoints
          (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                      (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                    f) :
                Perm α) :
            (a : α) → α))
        a)
    (ha : p a), False
⊢ (↑(derangements (Subtype p)) : Type u_1) ≃
    { f : { f : Perm α // ∀ (a : α), ¬p a → Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a } //
      ∀ (a : α), Membership.mem (γ := Set α) (fixedPoints (⇑(↑f : Perm α) : (a : α) → α)) a → ¬p a }
have refine_2 : ∀ (f : Perm (Subtype p)),
  (∀ (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) →
    Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f
Tactic: refine (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf : Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f
a : α
hfa :
  Membership.mem (γ := Set α)
    (fixedPoints
      (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
        (a : α) → α))
    a
ha : p a
⊢ False
have refine_1 : (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = (↑(Subtype.mk (p := p) a ha) : α)
Tactic: refine hf ⟨a, ha⟩ (Subtype.ext ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf : Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f
a : α
hfa :
  Membership.mem (γ := Set α)
    (fixedPoints
      (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
        (a : α) → α))
    a
ha : p a
⊢ (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = (↑(Subtype.mk (p := p) a ha) : α)
have hfa₁ : (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = a
Tactic: simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm,
        Equiv.coe_fn_mk, Perm.ofSubtype_apply_of_mem _ ha] at hfa
Cleared hypotheses: hfa
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ False
have refine_2 : 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: refine hf _ ?_ ha
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ Membership.mem (γ := Set α)
    (fixedPoints
      (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
        (a : α) → α))
    a
have refine_2 : IsFixedPt (⇑((Perm.ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) a
Tactic: simp only [Perm.subtypeEquivSubtypePerm_apply_coe, mem_fixedPoints]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ (((Perm.ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f : Perm α) : (a : α) → α) a = a
have refine_2 : (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = a
Tactic: simp_rw [Perm.ofSubtype_apply_of_mem _ ha, hfa]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm α
⊢ (∃ (_ : ∀ (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
have 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
Tactic: simp_rw [exists_prop, ← forall_and, ← iff_iff_implies_and_implies]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ (∃ (_ : ∀ (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
have 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
Tactic: simp_rw [exists_prop, ← forall_and, ← iff_iff_implies_and_implies]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 : { 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 : α) → α) }
have 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 }
Tactic: refine Equiv.sumCongr ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 }
⊢ { 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 : α) → α) }
have 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 : α) → α) }
Tactic: refine Equiv.sumCongr ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
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 : α) → α)) ∅ }
have refine_1 : ∀ (f : Perm α),
  Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧
      Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a ↔
    Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}
Tactic: refine Equiv.sumCongr (subtypeEquivRight fun f => ?_) (subtypeEquivRight fun f => ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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}
⊢ { 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 : α) → α)) ∅ }
have refine_2 : ∀ (f : Perm α),
  Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) ↔
    Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) ∅
Tactic: refine Equiv.sumCongr (subtypeEquivRight fun f => ?_) (subtypeEquivRight fun f => ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
f : Perm α
⊢ Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧
      Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a ↔
    Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}
have 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
Tactic: rw [Set.eq_singleton_iff_unique_mem, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
f : Perm α
⊢ Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) ↔
    Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) ∅
have refine_2 : Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a} ∧ a ∉ fixedPoints (⇑f : (a : α) → α) ↔
  ∀ (x : α), x ∉ fixedPoints (⇑f : (a : α) → α)
Tactic: rw [Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
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)
have subtypeEquivRight : ∀ (x : Perm α),
  (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ Membership.mem (γ := Set α) (fixedPoints (⇑x : (a : α) → α)) a_1) ↔
    Eq (α := Set α) (fixedPoints (⇑x : (a : α) → α)) {a}
Tactic: refine
        Equiv.sumCongr ((derangements.subtypeEquiv _).trans <|
            subtypeEquivRight fun x => ?_).symm
          (subtypeEquivRight fun f => mem_derangements_iff_fixedPoints_eq_empty.symm)
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ Membership.mem (γ := Set α) (fixedPoints (⇑x : (a : α) → α)) a_1) ↔
    Eq (α := Set α) (fixedPoints (⇑x : (a : α) → α)) {a}
have 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
Tactic: rw [eq_comm, Set.ext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Set (Perm α)) (fiber none) ∅
have rw : ∀ (x : Perm α), x ∉ fiber none
Tactic: rw [Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
f : Perm α
hyp : Membership.mem (γ := Set (Perm α)) (fiber none) f
⊢ False
have 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
Tactic: rw [RemoveNone.mem_fiber] at hyp
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ False
have 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
Tactic: rcases hyp with ⟨F, F_derangement, F_none, _⟩
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ fiber (some a) = {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}}
have h : ∀ (f : Perm α),
  f ∈ fiber (some a) ↔
    Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) ↔
    Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
have h : f ∈ fiber (some a) →
  Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ f ∈ fiber (some a) ↔
    Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
have h₁ : Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f →
  f ∈ fiber (some a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) →
    Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
have 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
Tactic: rw [RemoveNone.mem_fiber]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (hypothesis)
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
⊢ Membership.mem (γ := Set α) {a} x
have x_fixed₁ : (removeNone F : (a : α) → α) x = x
Tactic: rw [mem_fixedPoints_iff] at x_fixed
Cleared hypotheses: x_fixed
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (hypothesis)
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
⊢ Membership.mem (γ := Set α) {a} x
have x_fixed₁ : some ((removeNone F : (a : α) → α) x) = some x
Tactic: apply_fun some at x_fixed
Cleared hypotheses: x_fixed
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ Membership.mem (γ := Set α) {a} x
have h : ∀ (Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
  Membership.mem (γ := Set α) {a} x
Tactic: rcases Fx : F (some x) with - | y
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ Membership.mem (γ := Set α) {a} x
have h₁ : ∀ (y : α) (Fx : (F : (a : Option α) → Option α) (some x) = some y), Membership.mem (γ := Set α) {a} x
Tactic: rcases Fx : F (some x) with - | y
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 α)
⊢ Membership.mem (γ := Set α) {a} x
have 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
Tactic: rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
Cleared hypotheses: x_fixed, Fx
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ Membership.mem (γ := Set α) {a} x
have h₁ : ∀ (x_fixed : some a = some x)
  (Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
  Membership.mem (γ := Set α) {a} x
Tactic: rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
Cleared hypotheses: x_fixed, Fx
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ Membership.mem (γ := Set α) {a} x
have h₂ : ∀ (x_fixed : a = x) (Fx : Eq (α := Option α) ((F : (a : Option α) → Option α) (some x) : Option α) (none : Option α)),
  Membership.mem (γ := Set α) {a} x
Tactic: rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
Cleared hypotheses: x_fixed, Fx