no goals
α✝ : Type ?u.1538
α : Type u_1
β : Type u_2
inst✝¹ : Fintype β
f : α → β
inst✝ : Fintype ↑(classes (ker f))
⊢ Fintype.card ↑(classes (ker f)) ≤ Fintype.card β
classical exact
    le_trans (Set.card_le_of_subset (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)
no goals
α✝ : Type ?u.1538
α : Type u_1
β : Type u_2
inst✝¹ : Fintype β
f : α → β
inst✝ : Fintype ↑(classes (ker f))
⊢ Fintype.card ↑(classes (ker f)) ≤ Fintype.card β
exact
le_trans (Set.card_le_of_subset (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)