From f29a29d9bf776f2ad798cb4719dba60c00bc1fcf Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Sun, 29 Oct 2023 17:45:47 +0100
Subject: [PATCH] resolve sorry in lengthAdd using Finset.sum_insert

---
 Bml/Setsimp.lean | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/Bml/Setsimp.lean b/Bml/Setsimp.lean
index 3e7d8d3..369a3ae 100644
--- a/Bml/Setsimp.lean
+++ b/Bml/Setsimp.lean
@@ -22,14 +22,10 @@ theorem sdiff_singleton_is_erase {X : Finset Formula} {ϕ : Formula} : X \ {ϕ}
 theorem lengthAdd {X : Finset Formula} :
     ∀ {ϕ} (h : ϕ ∉ X), lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ :=
   by
-  induction X using Finset.induction_on
-  · unfold lengthOfSet
-    simp
-  case insert ψ Y psiNotInY IH =>
-    unfold lengthOfSet at *
-    intro ϕ h
-    simp
-    sorry -- finish
+  intro psi notin
+  unfold lengthOfSet
+  rw [Finset.sum_insert notin]
+  apply Nat.add_comm
 
 @[simp]
 theorem lengthOf_insert_leq_plus {X : Finset Formula} {ϕ : Formula} :