fixes in Archive

Archive/MiuLanguage/DecisionNec.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gihan Marasingha
 -/
 import Archive.MiuLanguage.Basic
+import Mathlib.Data.List.Basic
 import Mathlib.Data.List.Count
 import Mathlib.Data.Nat.ModEq
 import Mathlib.Tactic.Ring
@@ -71,9 +72,10 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) :
   any_goals apply mod3_eq_1_or_mod3_eq_2 h_ih
   -- Porting note: `simp_rw [count_append]` usually doesn't work
   · left; rw [count_append, count_append]; rfl
-  · right; simp_rw [count_append, count_cons, if_false, two_mul]; simp
+  · right; simp_rw [count_append, count_cons, beq_iff_eq, ite_false, add_zero, two_mul]
   · left; rw [count_append, count_append, count_append]
-    simp_rw [count_cons_self, count_nil, count_cons, ite_false, add_right_comm, add_mod_right]
+    simp_rw [count_cons_self, count_nil, count_cons, beq_iff_eq, ite_false, add_right_comm,
+      add_mod_right]
     simp
   · left; rw [count_append, count_append, count_append]
     simp only [ne_eq, not_false_eq_true, count_cons_of_ne, count_nil, add_zero]

Archive/MiuLanguage/DecisionSuf.lean

@@ -251,7 +251,7 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count
     · -- case `x = M` gives a contradiction.
       exfalso; exact hm (mem_cons_self M xs)
     · -- case `x = I`
-      rw [count_cons, if_pos rfl, length, succ_inj']
+      rw [count_cons, beq_self_eq_true, if_pos rfl, length, succ_inj']
       apply hxs
       · simpa only [count]
       · rw [mem_cons, not_or] at hm; exact hm.2
@@ -307,7 +307,9 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D
   use as, bs
   refine ⟨rfl, ?_, ?_, ?_⟩
   · -- Porting note: `simp_rw [count_append]` didn't work
-    rw [count_append] at hu; simp_rw [count_cons, if_true, add_succ, succ_inj'] at hu
+    rw [count_append] at hu
+    simp_rw [count_cons, beq_self_eq_true, if_true, add_succ, beq_iff_eq, reduceIte, add_zero,
+      succ_inj'] at hu
     rwa [count_append, count_append]
   · apply And.intro rfl
     rw [cons_append, cons_append]

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -115,26 +115,27 @@ theorem counted_succ_succ (p q : ℕ) :
     obtain ⟨hl₀, hl₁, hl₂⟩ := hl
     obtain hlast | hlast := hl₂ (l.head hlnil) (List.head_mem hlnil)
     · refine Or.inl ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
-      · rw [List.count_tail l 1 hlnil, hl₀, hlast, if_pos rfl, Nat.add_sub_cancel]
+      · rw [List.count_tail l 1 hlnil, hl₀, hlast, beq_self_eq_true, if_pos rfl, Nat.add_sub_cancel]
       · rw [List.count_tail l (-1) hlnil, hl₁, hlast, if_neg (by decide), Nat.sub_zero]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
       · rw [← hlast, List.head_cons_tail]
     · refine Or.inr ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
       · rw [List.count_tail l 1 hlnil, hl₀, hlast, if_neg (by decide), Nat.sub_zero]
-      · rw [List.count_tail l (-1) hlnil, hl₁, hlast, if_pos rfl, Nat.add_sub_cancel]
+      · rw [List.count_tail l (-1) hlnil, hl₁, hlast, beq_self_eq_true, if_pos rfl,
+          Nat.add_sub_cancel]
       · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
       · rw [← hlast, List.head_cons_tail]
   · rintro (⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩ | ⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩)
     · refine ⟨?_, ?_, ?_⟩
-      · rw [List.count_cons, if_pos rfl, ht₀]
+      · rw [List.count_cons, beq_self_eq_true, if_pos rfl, ht₀]
       · rw [List.count_cons, if_neg, ht₁]
         norm_num
       · rintro x (_ | _)
         exacts [Or.inl rfl, ht₂ x (by tauto)]
     · refine ⟨?_, ?_, ?_⟩
       · rw [List.count_cons, if_neg, ht₀]
         norm_num
-      · rw [List.count_cons, if_pos rfl, ht₁]
+      · rw [List.count_cons, beq_self_eq_true, if_pos rfl, ht₁]
       · rintro x (_ | _)
         exacts [Or.inr rfl, ht₂ x (by tauto)]