[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
[PROOFSTEP]
have h1 : ∀ a : Fin (n + 1), card ({ a }ᶜ : Set (Fin (n + 1))) = card (Fin n) :=
  by
  intro a
  simp only [Fintype.card_fin, Finset.card_fin, Fintype.card_ofFinset, Finset.filter_ne' _ a,
    Set.mem_compl_singleton_iff, Finset.card_erase_of_mem (Finset.mem_univ a), add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
a : Fin (n + 1)
⊢ card ↑{a}ᶜ = card (Fin n)
[PROOFSTEP]
simp only [Fintype.card_fin, Finset.card_fin, Fintype.card_ofFinset, Finset.filter_ne' _ a, Set.mem_compl_singleton_iff,
  Finset.card_erase_of_mem (Finset.mem_univ a), add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
[PROOFSTEP]
have h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1))) := by
  simp only [card_fin, card_option]
    -- rewrite the LHS and substitute in our fintype-level equivalence
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
⊢ card (Fin (n + 2)) = card (Option (Fin (n + 1)))
[PROOFSTEP]
simp only [card_fin, card_option]
  -- rewrite the LHS and substitute in our fintype-level equivalence
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1)))
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ↑(numDerangements (Nat.zero + 1)) = (↑Nat.zero + 1) * ↑(numDerangements Nat.zero) - (-1) ^ Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ ↑(numDerangements (Nat.succ n + 1)) = (↑(Nat.succ n) + 1) * ↑(numDerangements (Nat.succ n)) - (-1) ^ Nat.succ n
[PROOFSTEP]
simp only [numDerangements_add_two, hn, pow_succ, Int.ofNat_mul, Int.ofNat_add, Int.ofNat_succ]
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ (↑n + 1) * (↑(numDerangements n) + ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n) - -1 * (-1) ^ n
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ card ↑(derangements (Fin n)) = numDerangements n
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n hyp
[GOAL]
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hyp : ∀ (m : ℕ), m < n → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n
[PROOFSTEP]
rcases n with _ | _ | n
[GOAL]
case h.zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin Nat.zero)) = numDerangements Nat.zero
[PROOFSTEP]
convert_to card ↑{f : Perm (Fin 0) | ∀ (x : Fin 0), f x ≠ x} = _ using 2
[GOAL]
case h.zero.convert_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑{f | ∀ (x : Fin 0), ↑f x ≠ x} = numDerangements Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ.zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.succ Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (Nat.succ Nat.zero))) = numDerangements (Nat.succ Nat.zero)
[PROOFSTEP]
convert_to card ↑{f : Perm (Fin 1) | ∀ (x : Fin 1), f x ≠ x} = _ using 2
[GOAL]
case h.succ.zero.convert_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.succ Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑{f | ∀ (x : Fin 1), ↑f x ≠ x} = numDerangements (Nat.succ Nat.zero)
[PROOFSTEP]
rfl
  -- knock out cases 0 and 1
    -- now we have n ≥ 2. rewrite everything in terms of card_derangements, so that we can use
    -- `card_derangements_fin_add_two`
[GOAL]
case h.succ.succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hyp : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (Nat.succ (Nat.succ n)))) = numDerangements (Nat.succ (Nat.succ n))
[PROOFSTEP]
rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp _ (Nat.lt_add_of_pos_right zero_lt_two),
  hyp _ (lt_add_one _)]
[GOAL]
α✝ : Type u_1
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements α) = numDerangements (card α)
[PROOFSTEP]
rw [← card_derangements_invariant (card_fin _)]
[GOAL]
α✝ : Type u_1
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)
[PROOFSTEP]
exact card_derangements_fin_eq_numDerangements
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ↑(numDerangements Nat.zero) = ∑ k in Finset.range (Nat.zero + 1), (-1) ^ k * ↑(Nat.ascFactorial k (Nat.zero - k))
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
⊢ ↑(numDerangements (Nat.succ n)) =
    ∑ k in Finset.range (Nat.succ n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (Nat.succ n - k))
[PROOFSTEP]
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)
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
[PROOFSTEP]
intro x hx
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
[PROOFSTEP]
have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
[PROOFSTEP]
rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_tsub_cancel_of_le h_le, Int.ofNat_mul, Int.ofNat_succ, mul_left_comm]
