From 6dc12564566a00f24c1e03f83aa80b897ca71f56 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Mon, 20 Oct 2025 19:41:14 +0200
Subject: Prove nonempty induction on finsets

---
 Nominal/Helpers/Finset.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 Nominal/Helpers/Finset.lean

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
-- 
cgit v1.3.1