From a98cb15cee91657e76fd8b7775ca9d0b833d2ab2 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Sat, 7 Sep 2024 22:24:25 +0200
Subject: [PATCH] induction ... using ... new principle works?!

---
 Pdl/Soundness.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Pdl/Soundness.lean b/Pdl/Soundness.lean
index 43e9265..89184ef 100644
--- a/Pdl/Soundness.lean
+++ b/Pdl/Soundness.lean
@@ -459,11 +459,10 @@ theorem PathIn.init_inductionOn t {motive : PathIn tab → Prop}
     exact root
 
 theorem PathIn.nil_le_anything : PathIn.nil ≤ t := by
-  apply PathIn.init_inductionOn t
+  induction t using PathIn.init_inductionOn
   case root =>
     exact Relation.ReflTransGen.refl
-  case step Hist two three =>
-    intro s nil_le_s u s_edge_u
+  case step nil_le_s u s_edge_u =>
     apply Relation.ReflTransGen.tail nil_le_s s_edge_u
 
 theorem PathIn.loc_le_loc_of_le {t1 t2} (h : t1 ≤ t2) :
@@ -600,7 +599,7 @@ def PathIn.rewind : (t : PathIn tab) → (k : Fin (t.toHistory.length + 1)) →
 | .pdl r tail, k => Fin.lastCases (.nil)
     (PathIn.pdl r ∘ tail.rewind ∘ Fin.cast (pdl_length_eq r tail)) k
 
-/-- Rewinding with 0 steps does nothing. -/
+/-- Rewinding 0 steps does nothing. -/
 theorem PathIn.rewind_zero {p : PathIn tab} : p.rewind 0 = p := by
   induction p -- Not sure about the strategy here.
   · simp [rewind]