diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean
index 8c79181..011c032 100644
--- a/LeroyCompilerVerificationCourse/Compil.lean
+++ b/LeroyCompilerVerificationCourse/Compil.lean
@@ -171,7 +171,6 @@ theorem code_at_head :
     rw [heq1] at H
     induction H
     case code_at_intro c1 c2 c3 oc a =>
-      unfold instr_at
       induction c1 generalizing oc with grind
 
 @[grind] theorem code_at_tail :
@@ -227,41 +226,23 @@ theorem code_at_head :
     induction C generalizing pc i
     case nil => grind
     case cons f t t_ih =>
-      unfold instr_at at h
-      by_cases pc = 0
-      rotate_left
-      next nz =>
-        grind
-      next z =>
-        have := code_at.code_at_intro [] [] (f :: t) pc
-        grind
+      have := code_at.code_at_intro [] [] (f :: t) pc
+      grind
 
 @[grind] theorem code_at_to_instr_at : code_at C pc (c1 ++ i :: c2) → instr_at C (pc + codelen c1) = .some i := by
-    intro h
-    cases h
-    next b e a =>
-      have := instr_at_app i (c2 ++ e) (b ++ c1) (pc + codelen c1) (by simp [codelen]; grind)
-      grind [List.append_eq]
+  grind
 
 theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int) (stk : stack) :
   code_at C pc (compile_aexp a) →
   transitions C (pc, stk, s) (pc + codelen (compile_aexp a), aeval s a :: stk, s) := by
     induction a generalizing C pc stk
     next =>
-      simp [aeval, compile_aexp]
-      intro a
       unfold transitions
-      apply star_one
-      apply transition.trans_const
-      cases a
-      next => grind
+      grind
     next =>
-      simp [aeval, compile_aexp]
       intro a
       apply star_one
-      apply transition.trans_var
-      cases a
-      next => grind
+      grind
     next a1 a2 a1_ih a2_ih =>
       simp [aeval, compile_aexp]
       intro a
@@ -269,14 +250,13 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int)
       · apply a1_ih
         grind
       · apply star_trans
-        · specialize a2_ih C (pc + codelen (compile_aexp a1)) (aeval s a1 :: stk)
-          apply a2_ih
+        · apply a2_ih
           grind
         · apply star_one
           cases a
           next c1 c3 a =>
-            have h1 := instr_a instr.Iadd c3 (c1 ++ compile_aexp a1 ++ compile_aexp a2) (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) (by grind)
-            have h2 := @transition.trans_add ((c1 ++ compile_aexp a1 ++ compile_aexp a2) ++ (instr.Iadd :: c3)) (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) stk s (aeval s a1) (aeval s a2) (by grind)
+            have h1 := instr_a
+            have h2 := @transition.trans_add
             grind
     next a1 a2 a1_ih a2_ih =>
       simp [aeval, compile_aexp]
@@ -285,17 +265,15 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int)
       · apply a1_ih
         grind
       · apply star_trans
-        · specialize a2_ih C (pc + codelen (compile_aexp a1)) (aeval s a1 :: stk)
-          apply a2_ih
+        · apply a2_ih
           grind
         · apply star_trans
           · apply star_one
-            · have := @transition.trans_opp C (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) ((aeval s a1) :: stk) s (aeval s a2)
-              apply this
+            · apply transition.trans_opp
               grind
           · apply star_one
-            · have := @code_at_to_instr_at C pc (compile_aexp a1 ++ compile_aexp a2 ++ [instr.Iopp])  instr.Iadd [] (by grind)
-              have := @transition.trans_add C (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2) + 1) stk s (aeval s a1) (-aeval s a2) (by simp [codelen] at *; grind)
+            · have := @code_at_to_instr_at C pc (compile_aexp a1 ++ compile_aexp a2 ++ [instr.Iopp])
+              have := @transition.trans_add
               grind
 -- Miss 5
 theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : Int) (pc : Int) (stk : stack) (h : code_at C pc (compile_bexp b d1 d0))  :
@@ -311,12 +289,7 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
         apply star.star_refl
       case neg is_not_zero =>
         apply star_one
-        simp [is_not_zero, codelen]
-        apply transition.trans_branch _ _ _ d1
-        · simp [compile_bexp, is_not_zero] at h
-          have := @code_at_to_instr_at C pc [] (instr.Ibranch d1) [] (by grind)
-          grind
-        · grind
+        grind
     next =>
       simp [compile_bexp, beval]
       by_cases d0 = 0
@@ -326,51 +299,27 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
       case neg is_not_zero =>
         apply star_one
         simp [is_not_zero, codelen]
-        apply transition.trans_branch _ _ _ d0
-        · simp [compile_bexp, is_not_zero] at h
-          have := @code_at_to_instr_at C pc [] (instr.Ibranch d0) [] (by grind)
-          grind
-        · grind
+        grind
     next a1 a2 =>
       simp [compile_bexp, beval]
       apply star_trans
-      · apply compile_aexp_correct
-        rotate_left
-        · exact a1
-        · grind
+      · apply compile_aexp_correct (a := a1)
+        grind
       · apply star_trans
-        · apply compile_aexp_correct
-          rotate_right
-          · exact a2
-          · grind
+        · apply compile_aexp_correct (a := a2)
+          grind
         · apply star_one
-          · apply transition.trans_beq
-            rotate_left; rotate_left
-            · exact d1
-            · exact d0
-            · simp [compile_bexp] at h
-              grind
-            · grind
+          · apply transition.trans_beq (d1 := d1) (d0 := d0) <;> grind
     next a1 a2 =>
       simp [compile_bexp, beval]
       apply star_trans
-      · apply compile_aexp_correct
-        rotate_left
-        · exact a1
-        · grind
+      · apply compile_aexp_correct (a := a1)
+        grind
       · apply star_trans
-        · apply compile_aexp_correct
-          rotate_right
-          · exact a2
-          · grind
+        · apply compile_aexp_correct (a := a2)
+          grind
         · apply star_one
-          · apply transition.trans_ble
-            rotate_left; rotate_left
-            · exact d1
-            · exact d0
-            · simp [compile_bexp] at h
-              grind
-            · grind
+          · apply transition.trans_ble (d1 := d1) (d0 := d0) <;> grind
     next b1 ih =>
       grind
     next b1 b2 b1_ih b2_ih =>
@@ -379,11 +328,8 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
       unfold compile_bexp
       simp [heq1, heq2]
       apply star_trans
-      · apply b1_ih
-        rotate_left
-        · exact 0
-        · exact (codelen code2 + d0)
-        · grind
+      · apply b1_ih (d1 := 0) (d0 := codelen code2 + d0)
+        grind
       · by_cases beval s b1 = true
         case pos isTrue =>
           simp [isTrue]
@@ -397,9 +343,6 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
           simp [Int.add_assoc] at *
           exact b2_ih
         case neg isFalse =>
-          simp [beval, isFalse]
-          rw [heq2]
-          simp [codelen_app]
           grind
 
 theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s c s') :
@@ -418,24 +361,16 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s
     intro C pc stk h
     unfold compile_com
     apply star_trans
-    · apply compile_aexp_correct
-      rotate_left
-      · exact a
-      · unfold compile_com at h
-        grind
+    · apply compile_aexp_correct (a := a)
+      grind
     · apply star_one
-      · have := @transition.trans_setvar C (pc + codelen (compile_aexp a)) stk s x (aeval s a)
-        rw [codelen_app, codelen_singleton]
-        suffices transition C (pc + codelen (compile_aexp a), aeval s a :: stk, s) (pc + codelen (compile_aexp a) + 1, stk, update x (aeval s a) s) from by grind
-        apply this
+      · have := @transition.trans_setvar C
         grind
   case cexec_seq s'2 c1 s1 c2 s2 cexec1 cexec2 c1_ih c2_ih =>
     intro C pc stk h
     apply star_trans
     · apply c1_ih
-      unfold compile_com at h
-      apply code_at_app_left
-      exact h
+      grind
     · specialize c2_ih C (pc + codelen (compile_com c1)) stk
       simp [compile_com, codelen_app]
       simp [Int.add_assoc] at c2_ih
@@ -459,11 +394,7 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s
         · apply ih
           grind
         · apply star_one
-          · apply transition.trans_branch
-            rotate_right
-            · exact codelen code2
-            · grind
-            · grind
+          · apply transition.trans_branch (d := codelen code2) <;> grind
       case neg isFalse =>
         simp [isFalse]
         rw [heq3]
@@ -499,17 +430,13 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s
     apply star_trans
     · apply compile_bexp_correct C s b 0 (codelen code_body + 1) pc stk (by grind)
     · apply star_trans
-      · simp [isTrue]
-        rw [heq2]
-        specialize ih1 C (pc + codelen code_branch) stk
-        apply ih1
+      · apply ih1
         grind
       · apply star_trans
         · apply star_one
-          apply transition.trans_branch
+          apply transition.trans_branch (d := d)
           rotate_left
           rotate_left
-          · exact d
           · exact (pc + codelen code_branch + codelen code_body + 1 + d)
           · grind
           · grind
@@ -520,7 +447,6 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s
             rw [heq1, heq2, heq3] at ih2
             simp [codelen_app]
             simp [codelen_app] at ih2
-
             have : (pc + codelen code_branch + codelen code_body + 1 + d +
       (codelen code_branch + (codelen code_body + codelen [instr.Ibranch d])) ) = (pc + (codelen code_branch + (codelen code_body + codelen [instr.Ibranch d]))) := by grind
             rw [←this]
diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean
index df39445..757d9b8 100644
--- a/LeroyCompilerVerificationCourse/Constprop.lean
+++ b/LeroyCompilerVerificationCourse/Constprop.lean
@@ -444,8 +444,7 @@ theorem cp_bexp_sound :
   ∀ s S, matches' s S ->
   ∀ b, beval s (cp_bexp S b) = beval s b := by
     intro s S AG b
-    induction b
-    any_goals grind [mk_EQUAL_sound, mk_LESSEQUAL_sound, mk_AND_sound, mk_NOT_sound]
+    induction b with grind [mk_EQUAL_sound, mk_LESSEQUAL_sound, mk_AND_sound, mk_NOT_sound]
 
 @[grind] noncomputable def cp_com (S : Store) (c : com) : com :=
   match c with
@@ -469,7 +468,6 @@ theorem cp_com_correct_terminating :
     case ASSIGN x a =>
       cases EXEC
       next =>
-        simp [cp_com]
         have := @cexec.cexec_assign s1 x (cp_aexp S1 a)
         grind
     case IFTHENELSE b c1 c2 c1_ih c2_ih =>
diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean
index 5ce1922..070f98d 100644
--- a/LeroyCompilerVerificationCourse/Deadcode.lean
+++ b/LeroyCompilerVerificationCourse/Deadcode.lean
@@ -7,30 +7,26 @@ Authors: Wojciech Różowski
 import LeroyCompilerVerificationCourse.Imp
 import Std.Data.HashSet
 
-open Classical in
-@[grind] def IdentSet := Std.HashSet ident
-  deriving Membership, Union, EmptyCollection
+abbrev IdentSet := Std.HashSet ident
 
-@[grind] instance : HasSubset IdentSet where
+instance : HasSubset IdentSet where
   Subset (a b : IdentSet) := ∀ x ∈ a, x ∈ b
 
-@[grind] noncomputable instance (a b : IdentSet) : Decidable (a ⊆ b) := Classical.propDecidable (a ⊆ b)
+noncomputable instance (a b : IdentSet) : Decidable (a ⊆ b) := Classical.propDecidable (a ⊆ b)
 
-@[grind] instance (x : ident) (a : IdentSet) : Decidable (x ∈ a) := Std.HashSet.instDecidableMem
-
-@[grind] instance : EmptyCollection IdentSet where
+instance : EmptyCollection IdentSet where
   emptyCollection := Std.HashSet.emptyWithCapacity
 
-@[grind] axiom union_characterisation (a b : IdentSet) (x : ident) : x ∈ (a ∪ b) ↔ x ∈ a ∨ x ∈ b
+@[grind =] theorem subset_def (a b : IdentSet) : a ⊆ b ↔ ∀ x ∈ a, x ∈ b := Iff.rfl
+
+@[grind] axiom union_characterisation (a b : IdentSet) (x : ident) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b
 
 @[grind] theorem union_characterisation2 (a b c : IdentSet) : a ⊆ b ∧ a ⊆ c → a ⊆ (b ∪ c) := by
-  intro ⟨ m1 , m2 ⟩
-  intro y mem
-  specialize m1 y mem
-  specialize m2 y mem
+  intro ⟨m1, m2⟩
+  intro y
+  specialize m1 y
   grind
 
-
 @[grind] theorem insert_characterisation (a : IdentSet) (x : ident) : x ∈ a.insert x := by
   grind
 
@@ -70,26 +66,16 @@ open Classical in
 
 @[grind] theorem  fixpoint_charact' (n : Nat) (x : IdentSet)  (F : IdentSet → IdentSet) (default : IdentSet) :
   ((F (deadcode_fixpoint_rec F default n x)) ⊆ (deadcode_fixpoint_rec F default n x)) ∨ (deadcode_fixpoint_rec F default n x = default) := by
-    induction n generalizing x <;> grind
+    induction n generalizing x with grind
 
 theorem fixpoint_charact (F : IdentSet → IdentSet) (default : IdentSet) :
     ((F (deadcode_fixpoint F default)) ⊆ (deadcode_fixpoint F default)) ∨ (deadcode_fixpoint F default = default) := by grind
 
+@[grind]
 theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F_stable : ∀ x , x ⊆ default -> (F x) ⊆ default) : deadcode_fixpoint F default ⊆ default := by
   have : ∀ n : Nat, ∀ x : IdentSet, x ⊆ default → (deadcode_fixpoint_rec F default n x) ⊆ default := by
     intro n
-    induction n
-    case zero =>
-      intro x contained
-      simp [deadcode_fixpoint_rec]
-      unfold Subset
-      unfold instHasSubsetIdentSet
-      grind
-    case succ n ih =>
-      grind
-  apply this
-  unfold Subset
-  unfold instHasSubsetIdentSet
+    induction n with grind
   grind
 
 @[grind] noncomputable def live (c : com) (L : IdentSet) : IdentSet :=
@@ -108,106 +94,16 @@ theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F
       let default := (fv_com (.WHILE b c)) ∪ L
       deadcode_fixpoint (fun x => L' ∪ (live c x)) default
 
+@[grind]
 theorem live_upper_bound :
   ∀ c L,
-   (live c L) ⊆ ((fv_com c) ∪  L) := by
+   (live c L) ⊆ ((fv_com c) ∪ L) := by
     intro c
-    induction c
-    case SKIP =>
-      intro L
-      simp [fv_com, live]
-      unfold Subset
-      unfold instHasSubsetIdentSet
-      grind
-    case ASSIGN x a =>
-      intro L
-      simp [fv_com, live]
-      split
-      case isTrue h =>
-        unfold Subset
-        unfold instHasSubsetIdentSet
-        grind
-      case isFalse h =>
-        unfold Subset
-        unfold instHasSubsetIdentSet
-        grind
-    case SEQ c1 c2 c1_ih c2_ih =>
-      intro L
-      simp [live, fv_com]
-      unfold Subset at *
-      unfold instHasSubsetIdentSet at *
-      simp at *
-      intro x contained
-      specialize c1_ih (live c2 L) x contained
-      grind
-    case IFTHENELSE b c1 c2 c1_ih c2_ih =>
-      unfold Subset at *
-      unfold instHasSubsetIdentSet at *
-      simp at *
-      grind
-    case WHILE b c1 c1_ih =>
-      simp [live, fv_com]
-      intro L
-      apply fixpoint_upper_bound
-      intro x hyp
-      intro y hyp2
-      have : y ∈ fv_bexp b ∨ y ∈ L ∨ y ∈ live c1 x := by grind
-      apply Or.elim this
-      next =>
-        grind
-      next =>
-        intro hyp3
-        apply Or.elim hyp3
-        next => grind
-        next =>
-          clear hyp3
-          intro hyp3
-          specialize c1_ih x y hyp3
-          have : y ∈ fv_com c1 ∨ y ∈ x := by grind
-          apply Or.elim this
-          next => grind
-          next =>
-            intro hyp4
-            specialize hyp y hyp4
-            grind
+    induction c with grind
 
 theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet)
   (eq : L' = live (.WHILE b c) L) :
-  (fv_bexp b) ⊆ L' ∧ L ⊆ L' ∧ (live c L') ⊆ L' := by
-    have hyp := fixpoint_charact (fun x : IdentSet => (fv_bexp b) ∪ L ∪ (live c x)) ((fv_bexp b) ∪ (fv_com c) ∪ L)
-    apply Or.elim hyp
-    case left =>
-      intro included
-      constructor
-      case left =>
-        intro y contained
-        specialize included y
-        grind
-      case right =>
-        constructor
-        case left =>
-          intro y mem
-          specialize included y
-          grind
-        case right =>
-          intro y mem
-          specialize included y
-          grind
-    case right =>
-      intro equal
-      constructor
-      case left =>
-        intro y mem
-        grind
-      case right =>
-        constructor
-        case left =>
-          intro y mem
-          grind
-        case right =>
-          intro y mem
-          have := live_upper_bound c L' y mem
-          grind
+  (fv_bexp b) ⊆ L' ∧ L ⊆ L' ∧ (live c L') ⊆ L' := by grind
 
 @[grind] noncomputable def dce (c : com) (L : IdentSet) : com :=
   match c with
@@ -222,13 +118,7 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet)
 
 @[grind] theorem agree_mon :
   ∀ L L' s1 s2,
-  agree L' s1 s2 -> L ⊆ L' -> agree L s1 s2 := by
-    intro L L' s1 s2 AG sub
-    unfold agree at *
-    intro x inL
-    specialize sub x inL
-    specialize AG x sub
-    exact AG
+  agree L' s1 s2 -> L ⊆ L' -> agree L s1 s2 := by grind
 
 @[grind] theorem aeval_agree :
   ∀ L s1 s2, agree L s1 s2 ->
@@ -238,129 +128,23 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet)
     any_goals grind
     case VAR x =>
       simp [fv_aexp]
-      intro mem
-      have : x ∈ L := by
-        have := insert_characterisation ∅ x
-        specialize mem x this
-        exact mem
-      simp [aeval]
-      unfold agree at AG
-      specialize AG x this
-      exact AG
-    case PLUS a1 a2 a1_ih a2_ih =>
-      intro contained
-      simp [aeval]
-      congr 1
-      next =>
-        apply a1_ih
-        simp [fv_aexp] at contained
-        intro y mem
-        specialize contained y (by grind)
-        exact contained
-      next =>
-        apply a2_ih
-        simp [fv_aexp] at contained
-        intro y mem
-        specialize contained y (by grind)
-        exact contained
-    case MINUS a1 a2 a1_ih a2_ih =>
-      intro contained
-      simp [aeval]
-      congr 1
-      next =>
-        apply a1_ih
-        simp [fv_aexp] at contained
-        intro y mem
-        specialize contained y (by grind)
-        exact contained
-      next =>
-        apply a2_ih
-        simp [fv_aexp] at contained
-        intro y mem
-        specialize contained y (by grind)
-        exact contained
+      grind
 
 theorem beval_agree :
   ∀ L s1 s2, agree L s1 s2 ->
   ∀ b, (fv_bexp b) ⊆ L -> beval s1 b = beval s2 b := by
     intro L s1 s2 AG b
-    induction b
-    any_goals grind
-    case EQUAL a1 a2 =>
-      intro cont
-      unfold agree at AG
-      simp [fv_bexp] at cont
-      have aeval_lemma := aeval_agree L s1 s2 AG
-      have subgoal1 : fv_aexp a1 ⊆ L := by
-        intro y mem
-        specialize cont y (by grind)
-        exact cont
-      have subgoal2 : fv_aexp a2 ⊆ L := by
-        intro y mem
-        specialize cont y (by grind)
-        exact cont
-      have eq1 := aeval_lemma a1 subgoal1
-      have eq2 := aeval_lemma a2 subgoal2
-      grind
-    case LESSEQUAL a1 a2 =>
-      intro cont
-      unfold agree at AG
-      simp [fv_bexp] at cont
-      have aeval_lemma := aeval_agree L s1 s2 AG
-      have subgoal1 : fv_aexp a1 ⊆ L := by
-        intro y mem
-        specialize cont y (by grind)
-        exact cont
-      have subgoal2 : fv_aexp a2 ⊆ L := by
-        intro y mem
-        specialize cont y (by grind)
-        exact cont
-      have eq1 := aeval_lemma a1 subgoal1
-      have eq2 := aeval_lemma a2 subgoal2
-      grind
-    case AND b1 b2 b1_ih b2_ih =>
-      intro cont
-      simp [fv_bexp] at cont
-      have : fv_bexp b1 ⊆ L ∧ fv_bexp b2 ⊆ L := by
-        constructor
-        case left =>
-          intro y mem
-          specialize cont y (by grind)
-          exact cont
-        case right =>
-          intro y mem
-          specialize cont y (by grind)
-          exact cont
-      specialize b1_ih (by grind)
-      specialize b2_ih (by grind)
-      grind
+    induction b with grind
 
 theorem agree_update_live :
   ∀ s1 s2 L x v,
   agree (L.erase x) s1 s2 ->
-  agree L (update x v s1) (update x v s2) := by
-    intro s1 s2 L x v AG
-    unfold agree at *
-    intro y
-    specialize AG y
-    intro inL
-    by_cases x = y
-    case neg notEq =>
-      specialize AG (by grind)
-      grind
-    case pos isEq =>
-      grind
+  agree L (update x v s1) (update x v s2) := by grind
 
 theorem agree_update_dead :
   ∀ s1 s2 L x v,
   agree L s1 s2 -> ¬x ∈ L ->
-  agree L (update x v s1) s2 := by
-    intro s1 s2 L x v AG not
-    unfold agree at *
-    intro y mem
-    specialize AG y mem
-    simp [update]
-    by_cases x=y <;> grind
+  agree L (update x v s1) s2 := by grind
 
 theorem dce_correct_terminating :
   ∀ s c s', cexec s c s' ->
@@ -371,19 +155,14 @@ theorem dce_correct_terminating :
     any_goals grind
     case cexec_while_loop s1 b c1 s2 s3 isTrue EX1 EX2 a_ih a_ih2 =>
       intro L s4 hyp
-      have := live_while_charact b c1 L  (live (com.WHILE b c1) L) (by grind)
-      have : agree (live c1 (live (com.WHILE b c1) L)) s1 s4 := by
-        apply agree_mon
-        · exact hyp
-        · grind
-      have ⟨ t1, ht1, ht2⟩ :=  a_ih (live (.WHILE b c1) L) s4 this
-      have ⟨u1, hu1, hu2 ⟩ :=  a_ih2 L t1 ht2
+      have ⟨t1, ht1, ht2⟩ :=  a_ih (live (.WHILE b c1) L) s4 (by grind)
+      have ⟨u1, hu1, hu2⟩ :=  a_ih2 L t1 ht2
       exists u1
       constructor
       rotate_right
       · exact hu2
       · apply cexec.cexec_while_loop
-        · have := beval_agree (live (com.WHILE b c1) L) s1 s4 hyp b (by grind)
+        · have := beval_agree (live (com.WHILE b c1) L) s1 s4
           grind
         · exact ht1
         · grind
@@ -393,64 +172,31 @@ theorem dce_correct_terminating :
       by_cases x ∈ L
       case neg notIn =>
         exists s3
-        constructor
-        · grind [dce]
-        · simp [notIn] at AG
-          exact @agree_update_dead s2 s3 L x (aeval s2 a) (by grind) notIn
+        grind
       case pos isIn =>
-        simp [isIn] at AG
         exists (update x (aeval s3 a) s3)
-        constructor
-        · simp [dce, isIn]
-          grind
-        · have subgoal : aeval s2 a = aeval s3 a := by
-            apply aeval_agree
-            · exact AG
-            · intro y mem
-              grind
-          rw [subgoal]
-          apply @agree_update_live
-          grind
+        grind
     case cexec_ifthenelse s2 b c1 c2 s3 EXEC ih =>
       intro L s4 AG
       simp [dce]
       have EQ : beval s2 b = beval s4 b := by
         apply beval_agree
         · apply AG
-        · simp [live]
-          intro y mem
-          grind
+        · grind
       by_cases beval s2 b = true
       case pos isTrue =>
-        simp [isTrue] at EXEC
         specialize ih L s4
-        simp [live] at AG
-        simp [isTrue] at ih
-        have ⟨s5 , EX', AG' ⟩ := ih (by grind)
-        exists s5
-        constructor
-        · apply cexec.cexec_ifthenelse
-          grind
-        · exact AG'
+        grind
       case neg isFalse =>
-        simp [isFalse] at EXEC
         specialize ih L s4
-        simp [live] at AG
-        simp [isFalse] at ih
-        have ⟨s5 , EX', AG' ⟩ := ih (by grind)
-        exists s5
-        constructor
-        · apply cexec.cexec_ifthenelse
-          grind
-        · exact AG'
+        grind
     case cexec_while_done s2 b c isFalse =>
       intro L s1 AG
-      have ⟨ h1 , h2 , h3 ⟩ := live_while_charact b c L (live (com.WHILE b c) L) (by grind)
+      have ⟨h1, h2, h3⟩ := live_while_charact b c L (live (com.WHILE b c) L) (by grind)
       have EQ : beval s2 b = beval s1 b := by
         apply beval_agree
         · apply AG
-        · intro y mem
-          specialize h1 y mem
-          exact h1
+        · grind
       exists s1
       grind
+    case cexec_seq => grind [-subset_def] -- TODO: what does wrong?
diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean
index 1b5dca9..6f98c47 100644
--- a/LeroyCompilerVerificationCourse/Fixpoints.lean
+++ b/LeroyCompilerVerificationCourse/Fixpoints.lean
@@ -15,8 +15,8 @@ universe u
   le : α → α → Prop
   beq : α → α → Bool
   le_trans : ∀ x y z, le x y -> le y z -> le x z
-  beq_true' : ∀ x y : α, beq x y = true → eq x y
-  beq_false' : ∀ x y : α, beq x y = false → ¬ eq x y
+  beq_true' : ∀ x y : α, beq x y = true → eq x y := by grind
+  beq_false' : ∀ x y : α, beq x y = false → ¬ eq x y := by grind
   gt_wf : WellFounded (fun x y : α => le y x ∧ ¬eq y x)
 open OrderStruct
 
@@ -171,14 +171,8 @@ theorem hash_set_incl_size_leq (S1 S2 : Store) : Le S2 S1 → List.Subperm (S1.t
   ∀ S S', Gt S S' -> S.size < S'.size := by
     intro S S' hyp
     unfold Gt at hyp
-    have ⟨ t₁, t₂ ⟩ := @Le_cardinal S S' (hyp.1)
-    apply Nat.lt_of_le_of_ne
-    case h₁ => exact t₁
-    case h₂ =>
-      apply Classical.byContradiction
-      intro h
-      simp at h
-      grind
+    have ⟨t₁, t₂⟩ := @Le_cardinal S S' (hyp.1)
+    grind
 
 theorem Gt_wf : WellFounded Gt := by
   have := @InvImage Store Nat Nat.lt fun x => x.size
@@ -200,8 +194,6 @@ noncomputable instance : OrderStruct Store where
   le := Le
   beq (S1 S2 : Store) :=  Decidable.decide (Equal S1 S2)
   le_trans := Le_trans
-  beq_true' := by grind
-  beq_false' := by grind
   gt_wf := Gt_wf
 end Constprop
 
@@ -225,15 +217,9 @@ instance : Monotone Store (fun x => Join Init (F x)) where
       exact h2
 
 noncomputable def fixpoint_join : Store := by
-  have := iterate Store (fun x => Join Init (F x)) Init (by apply Le_Join_l)
-  apply this
-  dsimp
-  intro z hyp
-  unfold le instOrderStructStore
-  dsimp
-  unfold Le
-  intro x n hyp2
-  specialize hyp x n hyp2
+  apply iterate Store (fun x => Join Init (F x)) Init (by apply Le_Join_l)
+  intro z hyp x
+  specialize hyp x
   grind
 
 theorem fixpoint_join_eq : Eq' (Join Init (F (fixpoint_join Init F) )) (fixpoint_join Init F) := by
@@ -244,14 +230,9 @@ theorem fixpoint_join_eq : Eq' (Join Init (F (fixpoint_join Init F) )) (fixpoint
   unfold Eq'
   · exact this
   · exact Init
-  · dsimp
-    apply Le_Join_l
-  · intro z hyp
-    unfold le instOrderStructStore
-    dsimp
-    unfold Le
-    intro x n hyp2
-    specialize hyp x n hyp2
+  · apply Le_Join_l
+  · intro z hyp x
+    specialize hyp x
     grind
   · rw [heq1]
 
@@ -273,31 +254,23 @@ theorem fixpoint_join_smallest :
   ∀ S, Le (Join Init (F S)) S -> Le (fixpoint_join Init F) S := by
     intro S LE
     unfold fixpoint_join
-    dsimp
     have := (@iterate_correct Store _ (fun x => Join Init (F x)) _ (fixpoint_join Init F) Init (?_) ?_ ?_).2 S LE
     exact this
-    · dsimp
-      apply Le_Join_l
-    · intro z hyp
-      unfold le instOrderStructStore
-      dsimp
-      unfold Le
-      intro x n hyp2
-      specialize hyp x n hyp2
+    · apply Le_Join_l
+    · intro z hyp x
+      specialize hyp x
       grind
     · unfold fixpoint_join
       dsimp
 
 @[grind] theorem Join_increasing :
   ∀ S1 S2 S3 S4,
-  Le S1 S2 -> Le S3 S4 -> Le (Join S1 S3) (Join S2 S4) := by
-    intros
-    grind
+  Le S1 S2 -> Le S3 S4 -> Le (Join S1 S3) (Join S2 S4) := by grind
 
 @[grind] theorem Aeval_increasing : ∀ S1 S2, Le S1 S2 ->
   ∀ a n, Aeval S2 a = .some n -> Aeval S1 a =.some n := by
     intro S1 S2 LE a
-    induction a <;> grind
+    induction a with grind
 
 @[grind] theorem Beval_increasing : ∀ S1 S2, Le S1 S2 ->
   ∀ b n, Beval S2 b = .some n -> Beval S1 b = .some n := by
@@ -312,8 +285,7 @@ theorem fixpoint_join_smallest :
 theorem Update_increasing :
   ∀ S1 S2 x a,
   Le S1 S2 ->
-  Le (Update x (Aeval S1 a) S1) (Update x (Aeval S2 a) S2) := by
-    intros; grind
+  Le (Update x (Aeval S1 a) S1) (Update x (Aeval S2 a) S2) := by grind
 
 end FixpointJoin
 
@@ -375,9 +347,8 @@ noncomputable def Cexec' : (c : com) →  {F : Store → Store // ∀ x y, le x
             · exact hyp
           · apply mon₂
             · exact hyp
-        intro id val hyp2
-        have := (Join_characterization (f₁ x) (f₂ x) id val).1 hyp2
-        split <;> grind
+        intro id
+        grind
       case some val =>
         have := Beval_increasing x y hyp b val heq
         split <;> grind ⟩
diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean
index 816bb94..58f3512 100644
--- a/LeroyCompilerVerificationCourse/Imp.lean
+++ b/LeroyCompilerVerificationCourse/Imp.lean
@@ -252,18 +252,11 @@ theorem cexec_bounded_complete (s s' : store) (c : com) :
       intro fuel2 a_ih2
       exists (fuel1 + fuel2)
       intro fuel' fgt
-      have t : fuel' ≥ fuel1 ∧ fuel' ≥ fuel2 := by grind
       have t1 : fuel1 > 0 := by
-        false_or_by_contra
-        rename_i hyp
-        simp at hyp
-        specialize a_ih1 0 (by grind)
+        specialize a_ih1 0
         grind
       have t2 : fuel2 > 0 := by
-        false_or_by_contra
-        rename_i hyp
-        simp at hyp
-        specialize a_ih2 0 (by grind)
+        specialize a_ih2 0
         grind
       induction fuel' with grind
     case cexec_ifthenelse s b c1 c2 s' a a_ih =>
@@ -282,17 +275,15 @@ theorem cexec_bounded_complete (s s' : store) (c : com) :
       intro fuel1 a_ih1
       apply Exists.elim a_ih2
       intro fuel2 a_ih2
-      exists (fuel1 + fuel2)
-      intro fuel' fgt
       have t1 : fuel1 > 0 := by
-        false_or_by_contra
-        specialize a_ih1 0 (by grind)
+        specialize a_ih1 0
         grind
       have t2 : fuel2 > 0 := by
-        false_or_by_contra
-        specialize a_ih2 0 (by grind)
+        specialize a_ih2 0
         grind
+      exists (fuel1 + fuel2)
       unfold cexec_bounded
+      intro fuel' fgt
       induction fgt with grind
 
 /-
@@ -332,11 +323,7 @@ theorem red_progress :
       intro s
       apply Or.intro_right
       apply Or.elim (c1_ih s)
-      case h.left =>
-        intro c1_eq
-        exists c2
-        exists s
-        grind
+      case h.left => grind
       case h.right =>
         intro h
         apply Exists.elim h
@@ -362,11 +349,8 @@ def goes_wrong (c : com) (s : store) : Prop := ∃ c', ∃ s', star red (c, s) (
     grind
   case star_step x y _ a₁ a₂ a_ih =>
     apply star.star_step
-    · apply red.red_seq_step
-      rotate_left
-      · exact y.1
-      · exact y.2
-      · grind
+    · apply red.red_seq_step (c2 := y.1)  (s2 := y.2)
+      grind
     · grind
 
 /-
@@ -386,7 +370,7 @@ theorem cexec_to_reds (s s' : store) (c : com) : cexec s c s' → star red (c, s
       exact ih1
     · apply star.star_step
       apply red.red_seq_done
-      exact ih2
+      grind
   case cexec_while_loop ih1 ih2 =>
     apply star_trans
     · apply star_one
diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean
index 38eac21..ad428ac 100644
--- a/LeroyCompilerVerificationCourse/Sequences.lean
+++ b/LeroyCompilerVerificationCourse/Sequences.lean
@@ -108,8 +108,7 @@ theorem infseq_from_function : ∀ a, infseq_with_function R a → infseq R a :=
   intro x hyp
   unfold infseq_with_function at hyp
   have ⟨f , ⟨h0, hsucc⟩⟩ := hyp
-  refine ⟨f 1, ?_⟩
-  refine ⟨by grind, ?_⟩
+  refine ⟨f 1, by grind, ?_⟩
   unfold infseq_with_function
   refine ⟨fun n => f (n + 1), by grind⟩
 
@@ -117,7 +116,7 @@ theorem infseq_from_function : ∀ a, infseq_with_function R a → infseq R a :=
 
 theorem star_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) (sab : star R a b) :
     ∀ c, star R a c → star R b c ∨ star R c b := by
-  induction sab <;> grind
+  induction sab with grind
 
 theorem finseq_unique (R_functional : ∀ a b c, R a b -> R a c -> b = c) :
   ∀ a b b', star R a b → irred R b → star R a b' → irred R b' → b = b' := by