Lagrange's theorem (group order divides)

import Mathlib

theorem lagrange_thm {G : Type*} [Group G] [Fintype G] (H : Subgroup G) [Fintype H] : Fintype.card H ∣ Fintype.card G := by
  rw [← Nat.card_eq_fintype_card, ← Nat.card_eq_fintype_card]
  exact Subgroup.card_subgroup_dvd_card H