case h
α : Type ?u.13112
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hyp : ∀ (m : ℕ), m < n → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n
α : Type ?u.13112
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ card ↑(derangements (Fin n)) = numDerangements n
induction' n using Nat.strong_induction_on with n hyp
case h.zero
α : Type ?u.13112
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin Nat.zero)) = numDerangements Nat.zero

case h.succ.zero
α : Type ?u.13112
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)

case h.succ.succ
α : Type ?u.13112
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))
case h
α : Type ?u.13112
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hyp : ∀ (m : ℕ), m < n → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n
rcases n with _ | _ | n
no goals
case h.succ.succ
α : Type ?u.13112
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))
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 _)]
case h.zero
α : Type ?u.13112
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
case h.zero
α : Type ?u.13112
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin Nat.zero)) = numDerangements Nat.zero
convert_to card ↑{ f : Perm (Fin 0) | ∀ (x : Fin 0), f x ≠ x }  = _ using 2
no goals
case h.zero
α : Type ?u.13112
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
rfl
case h.succ.zero
α : Type ?u.13112
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)
case h.succ.zero
α : Type ?u.13112
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)
convert_to card ↑{ f : Perm (Fin 1) | ∀ (x : Fin 1), f x ≠ x }  = _ using 2
no goals
case h.succ.zero
α : Type ?u.13112
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)
rfl