awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (hypothesis)
Goal:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card (↑{a}ᶜ : Type) = card (Fin n)
⊢ card (↑(derangements (Fin (n + 2))) : Type) =
    (n + 1) * card (↑(derangements (Fin n)) : Type) + (n + 1) * card (↑(derangements (Fin (n + 1))) : Type)
have h2 : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  (↑(numDerangements (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n
⊢ (↑(numDerangements (n + 1 + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * (↑(numDerangements (n + 1)) : ℤ) - HPow.hPow (α := ℤ) (-1) (n + 1)
have 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
Tactic: simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
⊢ (↑(numDerangements (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n
have zero : (↑(numDerangements (HAdd.hAdd (α := ℕ) 0 1)) : ℤ) =
  HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1 * (↑(numDerangements 0) : ℤ) - HPow.hPow (α := ℤ) (β := ℕ) (-1) 0
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
zero :
  (↑(numDerangements (HAdd.hAdd (α := ℕ) 0 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1 * (↑(numDerangements 0) : ℤ) - HPow.hPow (α := ℤ) (β := ℕ) (-1) 0
⊢ (↑(numDerangements (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n
have succ : ∀ (n : ℕ)
  (hn :
    (↑(numDerangements (n + 1)) : ℤ) =
      HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n),
  (↑(numDerangements (n + 1 + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * (↑(numDerangements (n + 1)) : ℤ) - HPow.hPow (α := ℤ) (-1) (n + 1)
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
⊢ card (↑(derangements (Fin n)) : Type) = numDerangements n
have ind : ∀ (n : ℕ) (hyp : ∀ m < n, card (↑(derangements (Fin m)) : Type) = numDerangements m),
  card (↑(derangements (Fin n)) : Type) = numDerangements n
Tactic: induction n using Nat.strongRecOn with | ind n hyp => _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hyp : ∀ m < n, card (↑(derangements (Fin m)) : Type) = numDerangements m
⊢ card (↑(derangements (Fin n)) : Type) = numDerangements n
have ind : ∀ (hyp : ∀ m < 0, card (↑(derangements (Fin m)) : Type) = numDerangements m),
  card (↑(derangements (Fin 0)) : Type) = numDerangements 0
Tactic: rcases n with _ | _ | n
Cleared hypotheses: n, hyp
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hyp : ∀ m < n, card (↑(derangements (Fin m)) : Type) = numDerangements m
ind :
  ∀ (hyp : ∀ m < 0, card (↑(derangements (Fin m)) : Type) = numDerangements m),
    card (↑(derangements (Fin 0)) : Type) = numDerangements 0
⊢ card (↑(derangements (Fin n)) : Type) = numDerangements n
have ind₁ : ∀ (hyp : ∀ m < HAdd.hAdd (α := ℕ) 0 1, card (↑(derangements (Fin m)) : Type) = numDerangements m),
  card (↑(derangements (Fin (HAdd.hAdd (α := ℕ) 0 1))) : Type) = numDerangements (HAdd.hAdd (α := ℕ) 0 1)
Tactic: rcases n with _ | _ | n
Cleared hypotheses: n, hyp
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hyp : ∀ m < n, card (↑(derangements (Fin m)) : Type) = numDerangements m
ind :
  ∀ (hyp : ∀ m < 0, card (↑(derangements (Fin m)) : Type) = numDerangements m),
    card (↑(derangements (Fin 0)) : Type) = numDerangements 0
ind₁ :
  ∀ (hyp : ∀ m < HAdd.hAdd (α := ℕ) 0 1, card (↑(derangements (Fin m)) : Type) = numDerangements m),
    card (↑(derangements (Fin (HAdd.hAdd (α := ℕ) 0 1))) : Type) = numDerangements (HAdd.hAdd (α := ℕ) 0 1)
⊢ card (↑(derangements (Fin n)) : Type) = numDerangements n
have ind₂ : ∀ (n : ℕ) (hyp : ∀ m < n + 1 + 1, card (↑(derangements (Fin m)) : Type) = numDerangements m),
  card (↑(derangements (Fin (n + 1 + 1))) : Type) = numDerangements (n + 1 + 1)
Tactic: rcases n with _ | _ | n
Cleared hypotheses: n, hyp
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hyp : ∀ m < n + 1 + 1, card (↑(derangements (Fin m)) : Type) = numDerangements m
⊢ card (↑(derangements (Fin (n + 1 + 1))) : Type) = numDerangements (n + 1 + 1)
have ind : n + 1 < n + 1 + 1
Tactic: rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp, hyp]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hyp : ∀ m < n + 1 + 1, card (↑(derangements (Fin m)) : Type) = numDerangements m
ind : n + 1 < n + 1 + 1
⊢ card (↑(derangements (Fin (n + 1 + 1))) : Type) = numDerangements (n + 1 + 1)
have ind₁ : n < n + 1 + 1
Tactic: rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp, hyp]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
⊢ card.{u_2} (↑(derangements α) : Type u_2) = numDerangements (card α)
have rw : card (↑(derangements (Fin (card α))) : Type) = numDerangements (card α)
Tactic: rw [← card_derangements_invariant (card_fin _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
⊢ Eq (α := ℤ) (↑(numDerangements (n + 1)) : ℤ)
    (∑ k ∈ Finset.range (n + 1 + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n + 1 - k)) : ℤ))
have succ : ∀ x ∈ Finset.range (n + 1),
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
Tactic: rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
      Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg,
      add_left_inj, Finset.sum_congr rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (hypothesis)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have h_le : x ≤ n
Tactic: have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have succ : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
  HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
Tactic: rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have succ₁ : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
  HPow.hPow (α := ℤ) (-1) x * (↑((x + 1 + (n - x)) * (x + 1).ascFactorial (n - x)) : ℤ)
Tactic: rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
succ₁ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1 + (n - x)) * (x + 1).ascFactorial (n - x)) : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have succ₂ : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
  HPow.hPow (α := ℤ) (-1) x * (↑((x + (n - x) + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
Tactic: rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
succ₁ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1 + (n - x)) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₂ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + (n - x) + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have succ₃ : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
  HPow.hPow (α := ℤ) (-1) x * (↑((n + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
Tactic: rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
succ₁ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1 + (n - x)) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₂ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + (n - x) + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₃ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((n + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have succ₄ : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
  HPow.hPow (α := ℤ) (-1) x * HMul.hMul (α := ℤ) (↑(n + 1) : ℤ) (↑((x + 1).ascFactorial (n - x)) : ℤ)
Tactic: rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
succ₁ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1 + (n - x)) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₂ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + (n - x) + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₃ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((n + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₄ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * HMul.hMul (α := ℤ) (↑(n + 1) : ℤ) (↑((x + 1).ascFactorial (n - x)) : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have succ₅ : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
  HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * (↑((x + 1).ascFactorial (n - x)) : ℤ))
Tactic: rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
succ₁ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1 + (n - x)) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₂ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + (n - x) + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₃ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((n + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₄ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * HMul.hMul (α := ℤ) (↑(n + 1) : ℤ) (↑((x + 1).ascFactorial (n - x)) : ℤ)
succ₅ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * (↑((x + 1).ascFactorial (n - x)) : ℤ))
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have succ₆ : HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
  HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * (↑((x + 1).ascFactorial (n - x)) : ℤ))
Tactic: rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
succ₁ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1 + (n - x)) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₂ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + (n - x) + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₃ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((n + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₄ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * HMul.hMul (α := ℤ) (↑(n + 1) : ℤ) (↑((x + 1).ascFactorial (n - x)) : ℤ)
succ₅ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * (↑((x + 1).ascFactorial (n - x)) : ℤ))
succ₆ :
  HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * (↑((x + 1).ascFactorial (n - x)) : ℤ))
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
have succ₇ : HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
  HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑((x + 1).ascFactorial (n - x)) : ℤ))
Tactic: rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
have zero : Eq (α := ℤ) (↑(numDerangements 0) : ℤ)
  (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (0 - k)) : ℤ))
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
      Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg,
      add_left_inj, Finset.sum_congr rfl]
    -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
    intro x hx
    have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
    rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Derangements.Finite (goal)
Goal:
n : ℕ
zero :
  Eq (α := ℤ) (↑(numDerangements 0) : ℤ)
    (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (0 - k)) : ℤ))
⊢ Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
have succ : ∀ (n : ℕ)
  (hn :
    Eq (α := ℤ) (↑(numDerangements n) : ℤ)
      (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))),
  Eq (α := ℤ) (↑(numDerangements (n + 1)) : ℤ)
    (∑ k ∈ Finset.range (n + 1 + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n + 1 - k)) : ℤ))
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
      Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg,
      add_left_inj, Finset.sum_congr rfl]
    -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
    intro x hx
    have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
    rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
adj adj' : V → V → Bool
⊢ Eq.{u_1 + 1} (α := Digraph V) ((fun (x : V → V → Bool) ↦ ({ Adj := fun (v w : V) ↦ x v w = true } : Digraph V)) adj)
      ((fun (x : V → V → Bool) ↦ ({ Adj := fun (v w : V) ↦ x v w = true } : Digraph V)) adj') →
    adj = adj'
have simp_rw : (Eq.{u_1 + 1} (α := V → V → Prop) (fun (v w : V) ↦ adj v w = true) fun (v w : V) ↦ adj' v w = true) → adj = adj'
Tactic: simp_rw [mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
adj adj' : V → V → Bool
h : Eq.{u_1 + 1} (α := V → V → Prop) (fun (v w : V) ↦ adj v w = true) fun (v w : V) ↦ adj' v w = true
⊢ adj = adj'
have h₁ : ∀ (v w : V), adj v w = adj' v w
Tactic: funext v w
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
have refine : Surjective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
Tactic: refine ⟨Embedding.injective _, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
G : Digraph V
⊢ ∃ (a : V → V → Bool), (Digraph.mk' : (a : V → V → Bool) → Digraph V) a = G
have h : ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) = G
Tactic: use fun v w ↦ G.Adj v w
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
G : Digraph V
⊢ ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) = G
have h : ∀ (v w : V),
  Digraph.Adj ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) v w ↔ G.Adj v w
Tactic: ext v w