awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₂ :
  ∀ (x_fixed : a = 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 : x = a) (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
y : α
Fx : (F : (a : Option α) → Option α) (some x) = some y
⊢ Membership.mem (γ := Set α) {a} x
have h : False
Tactic: exfalso
-- 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
y : α
Fx : (F : (a : Option α) → Option α) (some x) = some y
⊢ False
have h : ∀ (x_fixed : (F : (a : Option α) → Option α) (some x) = some x) (y : α)
  (Fx : (F : (a : Option α) → Option α) (some x) = some y), False
Tactic: rw [removeNone_some F ⟨y, Fx⟩] at x_fixed
Cleared hypotheses: x_fixed, y, Fx
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h_opfp : Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} f
⊢ f ∈ fiber (some a)
have 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)
Tactic: use Equiv.Perm.decomposeOption.symm (some a, f)
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h_opfp : Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {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)
have h : Membership.mem (α := Perm (Option α)) (γ := Set (Perm (Option α))) (derangements (Option α))
  ((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 α))
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 α
⊢ (((Equiv.symm Perm.decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (some a, f) : Perm (Option α)) :
        (a : Option α) → Option α)
      x ≠
    x
have 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)
Tactic: apply_fun fun x => Equiv.swap none (some a) x
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 α
⊢ 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)
have 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 α)
Tactic: simp only [Perm.decomposeOption_symm_apply, Perm.coe_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 α
⊢ 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 α)
have none : 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: rcases x with - | x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 (some a) : (a : Option α) → Option α)
        (comp (α := Option α) (β := Option α) (⇑(Equiv.swap Option.none (some a)) : (a : Option α) → Option α)
          (⇑(optionCongr f) : (a : Option α) → Option α) Option.none) :
      Option α)
    ((Equiv.swap Option.none (some a) : (a : Option α) → Option α) Option.none : Option α)
⊢ Ne (α := Option α)
    ((Equiv.swap Option.none (some a) : (a : Option α) → Option α)
        (comp (β := Option α) (⇑(Equiv.swap Option.none (some a)) : (a : Option α) → Option α)
          (⇑(optionCongr f) : (a : Option α) → Option α) x) :
      Option α)
    ((Equiv.swap Option.none (some a) : (a : Option α) → Option α) x : Option α)
have some : ∀ (x : α),
  Ne (α := Option α)
    ((Equiv.swap Option.none (some a) : (a : Option α) → Option α)
        (comp (β := Option α) (⇑(Equiv.swap Option.none (some a)) : (a : Option α) → Option α)
          (⇑(optionCongr f) : (a : Option α) → Option α) (some x)) :
      Option α)
    ((Equiv.swap Option.none (some a) : (a : Option α) → Option α) (some x) : Option α)
Tactic: rcases x with - | x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 : α
⊢ 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 α) (some x)) :
      Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
have some : Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
  ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
Tactic: simp only [comp, optionCongr_apply, Option.map_some, swap_apply_self]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 : α
⊢ Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
have pos : ∀ (x_vs_a : x = a),
  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
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 α)
⊢ Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
have neg : ∀ (x_vs_a : ¬x = a),
  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
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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 : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
have pos : Ne (α := Option α) (some ((f : (a : α) → α) a) : Option α) (none : Option α)
Tactic: rw [x_vs_a, swap_apply_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (hypothesis)
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 : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
have ne_1 : some x ≠ none
Tactic: have ne_1 : some x ≠ none := Option.some_ne_none _
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (hypothesis)
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 (α := Option α) (some ((f : (a : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
have ne_2 : some x ≠ some a
Tactic: have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
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
⊢ Ne (α := Option α) (some ((f : (a : α) → α) x) : Option α)
    ((Equiv.swap none (some a) : (a : Option α) → Option α) (some x) : Option α)
have neg : (f : (a : α) → α) x ≠ x
Tactic: rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
f : Perm α
h_opfp : Membership.mem (γ := Set (Perm α)) {f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {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)
have h : (some a, f) = (some a, f)
Tactic: rw [apply_symm_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
⊢ ∀ (a : (↑(Equiv.RemoveNone.fiber none) : Type u_1)), False
have rw : ∀ (a : (↑∅ : Type u_1)), False
Tactic: rw [Equiv.RemoveNone.fiber_none]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
⊢ (↑(derangements (Option α)) : Type u_1) ≃
    (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1)
have fiber_none_is_false : ∀ (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
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
fiber_none_is_false : ∀ (a : (↑(Equiv.RemoveNone.fiber none) : Type u_1)), False
⊢ (a : α) × (↑(Equiv.RemoveNone.fiber (some a)) : Type u_1) ≃
    (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1)
have 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)
Tactic: simp_rw [Equiv.RemoveNone.fiber_some]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
fiber_none_is_false : ∀ (a : (↑(Equiv.RemoveNone.fiber none) : Type u_1)), False
⊢ (↑(derangements (Option α)) : Type u_1) ≃
    (a : α) × (↑{f : Perm α | Subset (α := Set α) (fixedPoints (⇑f : (a : α) → α)) {a}} : Type u_1)
have derangements : (a : α) × (↑(Equiv.RemoveNone.fiber (some a)) : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
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)
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ)) atTop (𝓝 (Real.exp (-1)))
have simp_rw : Tendsto (fun (n : ℕ) ↦ s (n + 1)) atTop (𝓝 (Real.exp (-1)))
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
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)
⊢ Tendsto (fun (n : ℕ) ↦ s (n + 1)) atTop (𝓝 (Real.exp (-1)))
have rw : Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)) atTop (𝓝 (Real.exp (-1)))
Tactic: rw [tendsto_add_atTop_iff_nat
      (f := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
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)
⊢ Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)) atTop (𝓝 (Real.exp (-1)))
have h : HasSum (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (-1) i / (↑i.factorial : ℝ)) (Real.exp (-1))
Tactic: apply HasSum.tendsto_sum_nat
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
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 : ℝ)) (Real.exp (-1))
have h : HasSum (α := ℝ) (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (-1) i / (↑i.factorial : ℝ)) (exp (-1))
Tactic: rw [Real.exp_eq_exp_ℝ]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ)) atTop (𝓝 (Real.exp (-1)))
have suffices : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 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 : ℝ)
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(numDerangements n) : ℝ) (↑n.factorial : ℝ) = s (n + 1)
have rw : HDiv.hDiv (α := ℝ)
    (↑(∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ)) : ℝ)
    (↑n.factorial : ℝ) =
  s (n + 1)
Tactic: rw [← Int.cast_natCast, numDerangements_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n : ℕ
⊢ HDiv.hDiv (α := ℝ)
      (↑(∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ)) : ℝ)
      (↑n.factorial : ℝ) =
    s (n + 1)
have push_cast : HDiv.hDiv (α := ℝ) (∑ x ∈ Finset.range (n + 1), HPow.hPow (α := ℝ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℝ))
    (↑n.factorial : ℝ) =
  s (n + 1)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (∑ x ∈ Finset.range (n + 1), HPow.hPow (α := ℝ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℝ))
      (↑n.factorial : ℝ) =
    s (n + 1)
have rw : ∑ i ∈ Finset.range (n + 1), HPow.hPow (α := ℝ) (-1) i * (↑((i + 1).ascFactorial (n - i)) : ℝ) / (↑n.factorial : ℝ) =
  s (n + 1)
Tactic: rw [Finset.sum_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
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)
have refine : ∀ x ∈ Finset.range (n + 1),
  HPow.hPow (α := ℝ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) x / (↑x.factorial : ℝ)
Tactic: refine Finset.sum_congr (refl _) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (hypothesis)
Goal:
s : ℕ → ℝ := fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ HPow.hPow (α := ℝ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
have h_le : k ≤ n
Tactic: have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
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 * (↑((k + 1).ascFactorial (n - k)) : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
have rw : HPow.hPow (α := ℝ) (-1) k * (↑(n.factorial / k.factorial) : ℝ) / (↑n.factorial : ℝ) =
  HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
Tactic: rw [Nat.ascFactorial_eq_div, add_tsub_cancel_of_le h_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Exponential (goal)
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 * (↑(n.factorial / k.factorial) : ℝ) / (↑n.factorial : ℝ) =
    HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
have push_cast : HPow.hPow (α := ℝ) (-1) k * HDiv.hDiv (α := ℝ) (↑n.factorial : ℝ) (↑k.factorial : ℝ) / (↑n.factorial : ℝ) =
  HPow.hPow (α := ℝ) (-1) k / (↑k.factorial : ℝ)
Tactic: push_cast [Nat.factorial_dvd_factorial h_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
a : Fin (n + 1)
⊢ card (↑{a}ᶜ : Type) = card (Fin n)
have rw : card (Fin (n + 1)) - card (↑{a} : Type) = card (Fin n)
Tactic: rw [Fintype.card_compl_set]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (hypothesis)
Goal:
n : ℕ
⊢ card (↑(derangements (Fin (n + 2))) : Type) =
    (n + 1) * card (↑(derangements (Fin n)) : Type) + (n + 1) * card (↑(derangements (Fin (n + 1))) : Type)
have h1 : ∀ (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