Prove nonempty induction on finsets

1 files changed, 23 insertions, 0 deletions

diff --git a/Nominal/Helpers/Finset.lean b/Nominal/Helpers/Finset.lean
new file mode 100644
index 0000000..1287c8e
--- /dev/null
+++ b/Nominal/Helpers/Finset.lean
@@ -0,0 +1,23 @@
+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