α : Type ?u.2521
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)))
α : Type ?u.2521
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
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]
α : Type ?u.2521
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)))
α : Type ?u.2521
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)))
have h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1))) := by simp only [card_fin, card_option]
no goals
α : Type ?u.2521
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)))
simp only [card_derangements_invariant h2,
  card_congr
    (@derangementsRecursionEquiv (Fin (n + 1))
      _),card_sigma,
  card_sum, card_derangements_invariant (h1 _), Finset.sum_const, nsmul_eq_mul, Finset.card_fin,
  mul_add, Nat.cast_id]
α : Type ?u.2521
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
a : Fin (n + 1)
⊢ card ↑({a}ᶜ) = card (Fin n)
α : Type ?u.2521
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ∀ (a : Fin (n + 1)), card ↑({a}ᶜ) = card (Fin n)
intro a
no goals
α : Type ?u.2521
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
a : Fin (n + 1)
⊢ card ↑({a}ᶜ) = card (Fin n)
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]
no goals
α : Type ?u.2521
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑({a}ᶜ) = card (Fin n)
⊢ card (Fin (n + 2)) = card (Option (Fin (n + 1)))
simp only [card_fin, card_option]