diff --git a/Qpf/Examples/_02_Tree.lean b/Qpf/Examples/_02_Tree.lean
index 0a19b15..a0f0745 100644
--- a/Qpf/Examples/_02_Tree.lean
+++ b/Qpf/Examples/_02_Tree.lean
@@ -1,6 +1,5 @@
 import Qpf
 import Qpf.Examples._01_List
-import Qpf.Macro.Tactic.FinDestr
 
 open MvQPF
 
diff --git a/Qpf/Macro/Tactic/FinDestr.lean b/Qpf/Macro/Tactic/FinDestr.lean
deleted file mode 100644
index 29020ab..0000000
--- a/Qpf/Macro/Tactic/FinDestr.lean
+++ /dev/null
@@ -1,91 +0,0 @@
-import Std.Tactic.PermuteGoals
-import Qpf.MathlibPort.Fin2
-
-/-!
-  `fin_destr i`, where `i` identifies a local hypothesis of type `Fin2 n` will break the current
-  goal into `n` separate goals, where in each `i` is replaced by a concrete `Fin2 n` term
-
-  TODO: replace with `fin_cases` after Mathlib is updated to a version that has it available
--/
-
-open Lean Syntax Elab Elab.Tactic Meta
-
-def elabFinDestrAux (i_stx : TSyntax `ident) : TacticM Unit := do
-  let n ← mkFreshExprMVar (mkConst ``Nat) (kind:=MetavarKind.synthetic);
-
-  try {
-    let u ← mkFreshLevelMVar;
-    let us := [u]
-    let finTyp := mkApp (mkConst ``PFin2 us) n
-
-    -- Ensure the `i_stx` term has type `finType`, causing the `n` metavar to unify
-    let _ ← elabTermEnsuringType i_stx finTyp false;
-    Term.synthesizeSyntheticMVarsNoPostponing
-  } catch _ => {
-    let finTyp := mkApp (mkConst ``Fin2) n
-
-    -- Ensure the `i_stx` term has type `finType`, causing the `n` metavar to unify
-    let _ ← elabTermEnsuringType i_stx finTyp false;
-    Term.synthesizeSyntheticMVarsNoPostponing
-  }
-
-  let n ← match (← getExprMVarAssignment? n.mvarId!) with
-  | none    => throwErrorAt i_stx "{i_stx} must be of type `Fin2 0` or `Fin2 (Nat.succ n)`"
-  | some v  => whnf v
-
-  -- dbg_trace n
-
-  if let some n := n.natLit? then
-    let rec genTactic : Nat → TacticM (TSyntax `tactic)
-    | 0   =>  `(tactic| cases $i_stx:ident)
-    | n+1 => do
-              let tct ← genTactic n
-              `(tactic| (cases $i_stx:ident; swap; rename_i $i_stx:ident; $tct:tactic))
-
-    -- dbg_trace (←genTactic n)
-    evalTactic <|← genTactic n
-
-  else
-    let rec genTacticExpr : Expr → TacticM (Option <| TSyntax `tactic)
-      | Expr.const ``Nat.zero .. =>
-        `(tactic| cases $i_stx:ident)
-
-      | Expr.app (Expr.const ``Nat.succ ..) n .. => do
-          match ←genTacticExpr n with
-          | none      => `(tactic| cases $i_stx:ident)
-          | some tct  => `(tactic| (cases $i_stx:ident; swap; rename_i $i_stx:ident; $tct:tactic))
-      | _ => pure none
-
-    match ←genTacticExpr n with
-    | some tct => evalTactic tct
-    | none     => throwErrorAt i_stx "{i_stx} must be of type `Fin2 0` or `Fin2 (Nat.succ n)`"
-
-
-
-elab "fin_destr_one " i:ident : tactic => do
-  withMainContext <|
-    elabFinDestrAux i
-
-syntax "fin_destr' " ident* : tactic
-macro_rules
-| `(tactic| fin_destr' $i:ident $is:ident*) => `(tactic| fin_destr_one $i <;> dsimp (config := {failIfUnchanged := false}) <;> fin_destr' $is:ident*)
-| `(tactic| fin_destr') => `(tactic| skip)
-
-syntax "fin_destr " ident* : tactic
-macro_rules
-| `(tactic| fin_destr $i:ident $is:ident*) => `(tactic|
-      fin_destr' $i:ident $is:ident*
-      <;> try fin_destr
-    )
-
-| `(tactic| fin_destr) => `(tactic|
-      first
-      | intro i;  fin_destr i
-      | funext i; fin_destr i
-  )
-
-
-syntax "vec_eq " (tactic)? : tactic
-macro_rules
-| `(tactic| vec_eq) => `(tactic| vec_eq trivial)
-| `(tactic| vec_eq $tct:tactic ) => `(tactic| funext i; fin_destr i <;> $tct:tactic)
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean b/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean
index 6f5fccf..6e535a7 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean
@@ -2,7 +2,6 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
 import Qpf.Util
-import Qpf.Macro.Tactic.FinDestr
 import Qpf.PFunctor.Multivariate.Basic
 
 namespace MvQPF
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
index 7ce3ae8..a10d949 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
@@ -6,7 +6,6 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
 import Qpf.Util
-import Qpf.Macro.Tactic.FinDestr
 import Qpf.Qpf.Multivariate.Basic
 
 namespace MvQPF
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean
index ed38397..01a7f74 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean
@@ -5,7 +5,6 @@
 import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
-import Qpf.Macro.Tactic.FinDestr
 import Qpf.Util
 import Qpf.Qpf.Multivariate.Basic
 
diff --git a/Qpf/Qpf/Multivariate/ofPolynomial.lean b/Qpf/Qpf/Multivariate/ofPolynomial.lean
index 734a3b8..16e5de5 100644
--- a/Qpf/Qpf/Multivariate/ofPolynomial.lean
+++ b/Qpf/Qpf/Multivariate/ofPolynomial.lean
@@ -1,22 +1,21 @@
 import Mathlib.Data.QPF.Multivariate.Basic
 import Qpf.Util
-import Qpf.Macro.Tactic.FinDestr
 
 /-!
-  This file provides a way to show some typefunction `F` is a QPF by establishing an isomorphism 
+  This file provides a way to show some typefunction `F` is a QPF by establishing an isomorphism
   to some polynomial functor `P`
 
   This is especially useful to show functoriality of external type functions, which are not
   easily redefined in terms of `MvPFunctor`
 -/
 
-namespace MvFunctor 
+namespace MvFunctor
   /-- If `F` is isomorphic to a MvFunctor `F'`, then `F` is also a MvFunctor -/
   def ofIsomorphism {F : TypeFun n}
                     (F' : TypeFun n)
                     [q : MvFunctor F']
-                    (box    : ∀{α}, F α → F' α) 
-                    (unbox  : ∀{α}, F' α → F α) 
+                    (box    : ∀{α}, F α → F' α)
+                    (unbox  : ∀{α}, F' α → F α)
                   : MvFunctor F
     where
       map f a     := unbox <| q.map f <| box a
@@ -24,15 +23,15 @@ end MvFunctor
 
 namespace MvQPF
   /-- If `F` is isomorphic to a QPF `F'`, then `F` is also a QPF -/
-  def ofIsomorphism {F : TypeFun n} 
+  def ofIsomorphism {F : TypeFun n}
                     (F' : TypeFun n)
                     [functor' : MvFunctor F']
                     [functor : MvFunctor F]
                     [q : MvQPF F']
-                    (box    : ∀{α}, F α → F' α) 
-                    (unbox  : ∀{α}, F' α → F α) 
+                    (box    : ∀{α}, F α → F' α)
+                    (unbox  : ∀{α}, F' α → F α)
                     (box_unbox_id : ∀{α} (x : F' α), box (unbox x) = x)
-                    (unbox_box_id : ∀{α} (x : F α), unbox (box x) = x 
+                    (unbox_box_id : ∀{α} (x : F α), unbox (box x) = x
                                   := by intros; rfl
                                 )
                     (map_eq : ∀ (α β : TypeVec n) (f : TypeVec.Arrow α β) (a : F α), functor.map f a = (unbox <| functor'.map f <| box a) := by intros; rfl)
@@ -41,19 +40,19 @@ namespace MvQPF
       P           := q.P
       abs         := unbox ∘ q.abs
       repr        := q.repr ∘ box
-      abs_repr    := by 
-                      intros  
+      abs_repr    := by
+                      intros
                       simp only [q.abs_repr, unbox_box_id, Function.comp]
-      abs_map f x := by 
+      abs_map f x := by
                       dsimp
                       rw [map_eq]
                       apply congrArg
                       simp [box_unbox_id, q.abs_map]
 
   /-- If `F` is isomorphic to a polynomial functor `P'`, then `F` is a QPF -/
-  def ofPolynomial  {F : TypeFun n} 
+  def ofPolynomial  {F : TypeFun n}
                     (P : MvPFunctor n)
-    := @ofIsomorphism _ F P.Obj 
-  
+    := @ofIsomorphism _ F P.Obj
+
 
 end MvQPF