import Mathlib.Tactic

namespace Finset.Nonempty

theorem induction
  {α : Type} {motive : Finset α → Prop} [DecidableEq α]
  (single : ∀ (a : α), motive {a})
  (insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s))
  : ∀ s, Finset.Nonempty s → motive s := by
  intro S
  induction' S using Finset.induction
  · simp
  · expose_names
    intro _
    by_cases h : (Finset.Nonempty s)
    · apply insert
      · assumption
      · apply h_1; assumption
    · simp at h
      rw [h]
      apply single

end Finset.Nonempty