awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
none :
  Ne (α := Option α)
    ((Equiv.swap Option.none (Option.some a) : (a : Option α) → Option α)
        (comp (α := Option α) (β := Option α) (⇑(Equiv.swap Option.none (Option.some a)) : (a : Option α) → Option α)
          (⇑(optionCongr f) : (a : Option α) → Option α) Option.none) :
      Option α)
    ((Equiv.swap Option.none (Option.some a) : (a : Option α) → Option α) Option.none : Option α)
some :
  ∀ (x : α),
    Ne (α := Option α)
      ((Equiv.swap Option.none (Option.some a) : (a : Option α) → Option α)
          (comp (β := Option α) (⇑(Equiv.swap Option.none (Option.some a)) : (a : Option α) → Option α)
            (⇑(optionCongr f) : (a : Option α) → Option α) (Option.some x)) :
        Option α)
      ((Equiv.swap Option.none (Option.some a) : (a : Option α) → Option α) (Option.some x) : Option α)
⊢ Ne (α := Option α)
    ((Equiv.swap Option.none (Option.some a) : (a : Option α) → Option α)
        (comp (β := Option α) (⇑(Equiv.swap Option.none (Option.some a)) : (a : Option α) → Option α)
          (⇑(optionCongr f) : (a : Option α) → Option α) x) :
      Option α)
    ((Equiv.swap Option.none (Option.some a) : (a : Option α) → Option α) x : Option α)

Tactic:
rcases x with - | x
-- 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
⊢ Ne (α := Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α)
        (comp (α := Option α) (β := Option α) (⇑(Equiv.swap none (some a)) : (a : Option α) → Option α)
          (⇑(optionCongr f) : (a : Option α) → Option α) none) :
      Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) none : Option α)

Tactic:
simp
-- 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 : α
some :
  Ne (α := Option α) (Option.some ((f : (a : α) → α) x) : Option α)
    ((Equiv.swap none (Option.some a) : (a : Option α) → Option α) (Option.some x) : Option α)
⊢ Ne (α := Option α)
    ((Equiv.swap none (Option.some a) : (a : Option α) → Option α)
        (comp (β := Option α) (⇑(Equiv.swap none (Option.some a)) : (a : Option α) → Option α)
          (⇑(optionCongr f) : (a : Option α) → Option α) (Option.some x)) :
      Option α)
    ((Equiv.swap none (Option.some a) : (a : Option α) → Option α) (Option.some x) : Option α)

Tactic:
simp only [comp, optionCongr_apply, Option.map_some, swap_apply_self]

Premises used: Equiv.swap_apply_self, Function.comp, Equiv.optionCongr_apply, Option.map_some
-- 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 : α
pos :
  ∀ (x_vs_a : x = a),
    Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
      ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
neg :
  ∀ (x_vs_a : ¬x = a),
    Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
      ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
⊢ Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)

Tactic:
by_cases x_vs_a : x = a
-- 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 : α
x_vs_a : x = a
pos : Ne (α := Option α) (some ((f : (a : α) → α) a) : Option α) (none : Option α)
⊢ Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)

Tactic:
rw [x_vs_a, swap_apply_right]

Premises used: Equiv.swap_apply_right
-- 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 : α
x_vs_a : x = a
⊢ Ne (α := Option α) (some ((f : (a : α) → α) a) : Option α) (none : Option α)

Tactic:
apply Option.some_ne_none

Premises used: Option.some_ne_none
-- 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 : α
x_vs_a : ¬x = a
⊢ some x ≠ none

Tactic:
have ne_1 : some x ≠ none := Option.some_ne_none _
-- 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 : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
⊢ some x ≠ some a

Tactic:
have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
-- 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 : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
neg : (f : (a : α) → α) x ≠ x
⊢ Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)

Tactic:
rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]

Premises used: Function.Injective.ne_iff, Equiv.swap_apply_of_ne_of_ne, Option.some_injective
-- 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 : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
contra : (f : (a : α) → α) x = x
⊢ False

Tactic:
x_vs_a (h_opfp contra)
-- 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 : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
contra : (f : (a : α) → α) x = x
⊢ False

Tactic:
exact x_vs_a (h_opfp contra)
-- 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 h₁ : (some a, f) = (some a, f)
⊢ (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:
rw [apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
rw : ∀ (a : (↑∅ : Type u_1)), False
⊢ ∀ (a : (↑(Equiv.RemoveNone.fiber none) : Type u_1)), False

Tactic:
rw [Equiv.RemoveNone.fiber_none]

Premises used: derangements.Equiv.RemoveNone.fiber_none
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
⊢ ∀ (a : (↑∅ : Type u_1)), False

Tactic:
IsEmpty.false

Premises used: IsEmpty.false
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
⊢ ∀ (a : (↑∅ : Type u_1)), False

Tactic:
exact IsEmpty.false

Premises used: IsEmpty.false
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
⊢ ∀ (a : (↑(Equiv.RemoveNone.fiber none) : Type u_1)), False

Tactic:
have fiber_none_is_false : Equiv.RemoveNone.fiber (@none α) → False := by
    rw [Equiv.RemoveNone.fiber_none]
    exact IsEmpty.false
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
fiber_none_is_false : ∀ (a : (↑(Equiv.RemoveNone.fiber none) : Type u_1)), False
simp_rw :
  (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1) ≃
    (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1)
⊢ (a : α) × (↑(Equiv.RemoveNone.fiber (some a)) : Type u_1) ≃
    (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1)

Tactic:
simp_rw [Equiv.RemoveNone.fiber_some]

Premises used: derangements.Equiv.RemoveNone.fiber_some
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
fiber_none_is_false : ∀ (a : (↑(Equiv.RemoveNone.fiber none) : Type u_1)), False
⊢ (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1) ≃
    (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
fiber_none_is_false : ∀ (a : (↑(Equiv.RemoveNone.fiber none) : Type u_1)), False
derangements :
  (a : α) × (↑(Equiv.RemoveNone.fiber (some a)) : Type u_1) ≃
    (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1)
⊢ (↑(_root_.derangements (Option α)) : Type u_1) ≃
    (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1)

Tactic:
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

Premises used: Equiv.Perm.decomposeOption, Equiv.setProdEquivSigma, Equiv.Perm, Equiv.image, derangements, Equiv.sigmaOptionEquivOfSome, Option
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
this : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)
simp_rw : Tendsto (fun (n : ℕ) ↦ s (n + 1)) atTop (𝓝 (Real.exp (-1)))
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ)) atTop (𝓝 (Real.exp (-1)))

Tactic:
simp_rw [this]
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
this : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)
rw :
  Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)) atTop (𝓝 (Real.exp (-1)))
⊢ Tendsto (fun (n : ℕ) ↦ s (n + 1)) atTop (𝓝 (Real.exp (-1)))

Tactic:
rw [tendsto_add_atTop_iff_nat
      (f := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]

Premises used: Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
this : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)
h : HasSum (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (-1) i / (↑i.factorial : ℝ)) (Real.exp (-1))
⊢ Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)) atTop (𝓝 (Real.exp (-1)))

Tactic:
apply HasSum.tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
this : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)
h : HasSum (α := ℝ) (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (-1) i / (↑i.factorial : ℝ)) (exp (-1))
⊢ HasSum (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (-1) i / (↑i.factorial : ℝ)) (Real.exp (-1))

Tactic:
rw [Real.exp_eq_exp_ℝ]

Premises used: Real.exp_eq_exp_ℝ
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
this : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)
⊢ HasSum (α := ℝ) (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (-1) i / (↑i.factorial : ℝ)) (exp (-1))

Tactic:
expSeries_div_hasSum_exp (-1 : ℝ)

Premises used: NormedSpace.expSeries_div_hasSum_exp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
this : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)
⊢ HasSum (α := ℝ) (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (-1) i / (↑i.factorial : ℝ)) (exp (-1))

Tactic:
exact expSeries_div_hasSum_exp (-1 : ℝ)

Premises used: NormedSpace.expSeries_div_hasSum_exp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
suffices : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ)) atTop (𝓝 (Real.exp (-1)))

Tactic:
suffices ∀ n : ℕ, (numDerangements n : ℝ) / n.factorial = s (n + 1) by
    simp_rw [this]
    -- shift the function by 1, and then use the fact that the partial sums
    -- converge to the infinite sum
    rw [tendsto_add_atTop_iff_nat
      (f := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
    apply HasSum.tendsto_sum_nat
    -- there's no specific lemma for ℝ that ∑ x^k/k! sums to exp(x), but it's
    -- true in more general fields, so use that lemma
    rw [Real.exp_eq_exp_ℝ]
    exact expSeries_div_hasSum_exp (-1 : ℝ)
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n : ℕ
rw :
  HDiv.hDiv (α := ℝ)
      (↑(∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ)) : ℝ)
      (↑n.factorial : ℝ) =
    s (n + 1)
⊢ HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)

Tactic:
rw [← Int.cast_natCast, numDerangements_sum]

Premises used: Int.cast_natCast, numDerangements_sum
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n : ℕ
push_cast :
  HDiv.hDiv (α := ℝ) (∑ x ∈ Finset.range (n + 1), HPow.hPow (α := ℝ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℝ))
      (↑n.factorial : ℝ) =
    s (n + 1)
⊢ HDiv.hDiv (α := ℝ)
      (↑(∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ)) : ℝ)
      (↑n.factorial : ℝ) =
    s (n + 1)

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n : ℕ
rw :
  ∑ i ∈ Finset.range (n + 1), HPow.hPow (α := ℝ) (-1) i * (↑((i + 1).ascFactorial (n - i)) : ℝ) / (↑n.factorial : ℝ) =
    s (n + 1)
⊢ HDiv.hDiv (α := ℝ) (∑ x ∈ Finset.range (n + 1), HPow.hPow (α := ℝ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℝ))
      (↑n.factorial : ℝ) =
    s (n + 1)

Tactic:
rw [Finset.sum_div]

Premises used: Finset.sum_div
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), HPow.hPow (α := ℝ) (-1) i * (↑((i + 1).ascFactorial (n - i)) : ℝ) / (↑n.factorial : ℝ) =
    s (n + 1)

Tactic:
Finset.sum_congr (refl _) ?_

Premises used: refl, Finset.sum_congr
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n : ℕ
refine :
  ∀ x ∈ Finset.range (n + 1),
    HPow.hPow (α := ℝ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℝ) / (↑n.factorial : ℝ) =
      HPow.hPow (α := ℝ) (-1) x / (↑x.factorial : ℝ)
⊢ ∑ i ∈ Finset.range (n + 1), HPow.hPow (α := ℝ) (-1) i * (↑((i + 1).ascFactorial (n - i)) : ℝ) / (↑n.factorial : ℝ) =
    s (n + 1)

Tactic:
refine Finset.sum_congr (refl _) ?_

Premises used: refl, Finset.sum_congr
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ k ≤ n

Tactic:
have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
rw :
  HPow.hPow (α := ℝ) (-1) k * (↑(n.factorial / k.factorial) : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
⊢ HPow.hPow (α := ℝ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)

Tactic:
rw [Nat.ascFactorial_eq_div, add_tsub_cancel_of_le h_le]

Premises used: Nat.ascFactorial_eq_div, add_tsub_cancel_of_le
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
push_cast :
  HPow.hPow (α := ℝ) (-1) k * HDiv.hDiv (α := ℝ) (↑n.factorial : ℝ) (↑k.factorial : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
⊢ HPow.hPow (α := ℝ) (-1) k * (↑(n.factorial / k.factorial) : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)

Tactic:
push_cast [Nat.factorial_dvd_factorial h_le]

Premises used: Nat.factorial_dvd_factorial
-- Module: Mathlib.Combinatorics.Derangements.Exponential
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ HPow.hPow (α := ℝ) (-1) k * HDiv.hDiv (α := ℝ) (↑n.factorial : ℝ) (↑k.factorial : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)

Tactic:
field
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Fintype β
inst_3 : DecidableEq β
h : card α = card β
⊢ card.{u_2} (↑(derangements α) : Type u_2) = card.{u_3} (↑(derangements β) : Type u_3)

Tactic:
Fintype.card_congr (Equiv.derangementsCongr <| equivOfCardEq h)

Premises used: Fintype.card_congr, Equiv.derangementsCongr, Fintype.equivOfCardEq
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
a : Fin (n + 1)
rw : card (Fin (n + 1)) - card (↑{a} : Type) = card (Fin n)
⊢ card (↑{a}ᶜ : Type) = card (Fin n)

Tactic:
rw [Fintype.card_compl_set]

Premises used: Fintype.card_compl_set
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
a : Fin (n + 1)
⊢ card (Fin (n + 1)) - card (↑{a} : Type) = card (Fin n)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
⊢ ∀ (a : Fin (n + 1)), card (↑{a}ᶜ : Type) = card (Fin n)

Tactic:
have h1 : ∀ a : Fin (n + 1), card ({a}ᶜ : Set (Fin (n + 1))) = card (Fin n) := by
    intro a
    rw [Fintype.card_compl_set]
    simp
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card (↑{a}ᶜ : Type) = card (Fin n)
⊢ card (Fin (n + 2)) = card (Option (Fin (n + 1)))

Tactic:
simp only [card_fin, card_option]

Premises used: Fintype.card_fin, Fintype.card_option
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card (↑{a}ᶜ : Type) = card (Fin n)
⊢ card (Fin (n + 2)) = card (Option (Fin (n + 1)))

Tactic:
have h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1))) := by simp only [card_fin, card_option]
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card (↑{a}ᶜ : Type) = card (Fin n)
h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1)))
⊢ card (↑(derangements (Fin (n + 2))) : Type) =
    (n + 1) * card (↑(derangements (Fin n)) : Type) + (n + 1) * card (↑(derangements (Fin (n + 1))) : Type)

Tactic:
simp only [card_derangements_invariant h2,
    card_congr
      (@derangementsRecursionEquiv (Fin (n + 1))
        _), -- push the cardinality through the Σ and ⊕ so that we can use `card_n`
    card_sigma,
    card_sum, card_derangements_invariant (h1 _), Finset.sum_const, nsmul_eq_mul, Finset.card_fin,
    mul_add, Nat.cast_id]

Premises used: Fintype.card_congr, derangements.derangementsRecursionEquiv, Nat.cast_id, card_derangements_invariant, Fintype.card_sigma, Finset.card_fin, nsmul_eq_mul, mul_add, Fintype.card_sum, Finset.sum_const
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
⊢ numDerangements 0 = 1

Tactic:
rfl

Premises used: numDerangements, rfl
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
⊢ numDerangements 1 = 0

Tactic:
rfl

Premises used: numDerangements, rfl
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
⊢ numDerangements (n + 2) = (n + 1) * (numDerangements n + numDerangements (n + 1))

Tactic:
rfl

Premises used: numDerangements, rfl
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
⊢ (↑(numDerangements (HAdd.hAdd (α := ℕ) 0 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1 * (↑(numDerangements 0) : ℤ) - HPow.hPow (α := ℤ) (β := ℕ) (-1) 0

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hn :
  (↑(numDerangements (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) *
      ((↑(numDerangements n) : ℤ) +
        (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n)) =
    (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) + 1) *
        (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n) -
      HPow.hPow (α := ℤ) (-1) n * -1
⊢ (↑(numDerangements (n + 1 + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * (↑(numDerangements (n + 1)) : ℤ) - HPow.hPow (α := ℤ) (-1) (n + 1)

Tactic:
simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]

Premises used: Int.natCast_add, numDerangements_add_two, pow_succ, Int.natCast_mul
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hn :
  (↑(numDerangements (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) *
      ((↑(numDerangements n) : ℤ) +
        (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n)) =
    (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) + 1) *
        (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n) -
      HPow.hPow (α := ℤ) (-1) n * -1

Tactic:
ring