Theorem: card_lehmer_eq_factorial (Bruhat/Lehmer.lean)

State before:
n : ℕ
⊢ Fintype.card { g // ⇑g ≤ ⇑(truncate id n) } = n !
Tactic:
rw [Fintype.card_of_bijective (le_truncate_equiv_prod_fin _ _).bijective]
State after:
n : ℕ
⊢ Fintype.card ((i : Fin n) → Fin (id ↑i + 1)) = n !

State before:
n : ℕ
⊢ Fintype.card ((i : Fin n) → Fin (id ↑i + 1)) = n !
Tactic:
simp only [id_eq, Fintype.card_pi, Fintype.card_fin]
State after:
n : ℕ
⊢ (Finset.prod Finset.univ fun x => ↑x + 1) = n !

State before:
n : ℕ
⊢ (Finset.prod Finset.univ fun x => ↑x + 1) = n !
Tactic:
rw [← Finset.prod_range_add_one_eq_factorial n]
State after:
n : ℕ
⊢ (Finset.prod Finset.univ fun x => ↑x + 1) = Finset.prod (Finset.range n) fun x => x + 1

State before:
n : ℕ
⊢ (Finset.prod Finset.univ fun x => ↑x + 1) = Finset.prod (Finset.range n) fun x => x + 1
Tactic:
exact Fin.prod_univ_eq_prod_range Nat.succ n
State after:
no goals