chore: tidy various files (#12121)

Author: Ruben-VandeVelde

Mathlib/Algebra/Function/Indicator.lean

@@ -322,18 +322,8 @@ theorem mulIndicator_preimage_of_not_mem (s : Set α) (f : α → M) {t : Set M}
 @[to_additive]
 theorem mem_range_mulIndicator {r : M} {s : Set α} {f : α → M} :
     r ∈ range (mulIndicator s f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s := by
--- Porting note: This proof used to be:
-  -- simp [mulIndicator, ite_eq_iff, exists_or, eq_univ_iff_forall, and_comm, or_comm,
-  -- @eq_comm _ r 1]
-  simp only [mem_range, mulIndicator, ne_eq, mem_image]
-  rw [eq_univ_iff_forall, not_forall]
-  refine ⟨?_, ?_⟩
-  · rintro ⟨y, hy⟩
-    split_ifs at hy with hys
-    · tauto
-    · left
-      tauto
-  · rintro (⟨hr, ⟨x, hx⟩⟩ | ⟨x, ⟨hx, hxs⟩⟩) <;> use x <;> split_ifs <;> tauto
+  simp [mulIndicator, ite_eq_iff, exists_or, eq_univ_iff_forall, and_comm, or_comm,
+    @eq_comm _ r 1]
 #align set.mem_range_mul_indicator Set.mem_range_mulIndicator
 #align set.mem_range_indicator Set.mem_range_indicator
 

Mathlib/Data/Nat/ChineseRemainder.lean

@@ -32,7 +32,8 @@ lemma modEq_list_prod_iff {a b} {l : List ℕ} (co : l.Pairwise Coprime) :
   induction' l with m l ih
   · simp [modEq_one]
   · have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
-    simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]
+    simp only [List.prod_cons, ← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co),
+      List.length_cons]
     constructor
     · rintro ⟨h0, hs⟩ i
       cases i using Fin.cases <;> simp [h0, hs]
@@ -42,8 +43,11 @@ lemma modEq_list_prod_iff' {a b} {s : ι → ℕ} {l : List ι} (co : l.Pairwise
     a ≡ b [MOD (l.map s).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i] := by
   induction' l with i l ih
   · simp [modEq_one]
-  · have : Coprime (s i) (l.map s).prod := coprime_list_prod_right_iff.mpr
-      (by simp; intro j hj; exact (List.pairwise_cons.mp co).1 j hj)
+  · have : Coprime (s i) (l.map s).prod := by
+      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
+        forall_apply_eq_imp_iff₂]
+      intro j hj
+      exact (List.pairwise_cons.mp co).1 j hj
     simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]
 
 variable (a s : ι → ℕ)
@@ -54,38 +58,52 @@ def chineseRemainderOfList : (l : List ι) → l.Pairwise (Coprime on s) →
     { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
   | [],     _  => ⟨0, by simp⟩
   | i :: l, co => by
-    have : Coprime (s i) (l.map s).prod := coprime_list_prod_right_iff.mpr
-      (by simp; intro j hj; exact (List.pairwise_cons.mp co).1 j hj)
+    have : Coprime (s i) (l.map s).prod := by
+      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
+        forall_apply_eq_imp_iff₂]
+      intro j hj
+      exact (List.pairwise_cons.mp co).1 j hj
     have ih := chineseRemainderOfList l co.of_cons
     have k := chineseRemainder this (a i) ih
-    exact ⟨k, by
-      simp [k.prop.1]; intro j hj
-      exact ((modEq_list_prod_iff' co.of_cons).mp k.prop.2 j hj).trans (ih.prop j hj)⟩
+    use k
+    simp only [List.mem_cons, forall_eq_or_imp, k.prop.1, true_and]
+    intro j hj
+    exact ((modEq_list_prod_iff' co.of_cons).mp k.prop.2 j hj).trans (ih.prop j hj)
 
 @[simp] theorem chineseRemainderOfList_nil :
     (chineseRemainderOfList a s [] List.Pairwise.nil : ℕ) = 0 := rfl
 
 theorem chineseRemainderOfList_lt_prod (l : List ι)
     (co : l.Pairwise (Coprime on s)) (hs : ∀ i ∈ l, s i ≠ 0) :
     chineseRemainderOfList a s l co < (l.map s).prod := by
-  cases' l with i l <;> simp
-  · simp [chineseRemainderOfList]
-    have : Coprime (s i) (l.map s).prod := coprime_list_prod_right_iff.mpr
-      (by simp; intro j hj; exact (List.pairwise_cons.mp co).1 j hj)
-    exact chineseRemainder_lt_mul this (a i)
-      (chineseRemainderOfList a s l co.of_cons)
-        (hs i (by simp)) (by simp; intro j hj; exact hs j (by simp [hj]))
+  cases l with
+  | nil => simp
+  | cons i l =>
+    simp only [chineseRemainderOfList, List.map_cons, List.prod_cons]
+    have : Coprime (s i) (l.map s).prod := by
+      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
+        forall_apply_eq_imp_iff₂]
+      intro j hj
+      exact (List.pairwise_cons.mp co).1 j hj
+    refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
+      (hs i (List.mem_cons_self _ l)) ?_
+    simp only [ne_eq, List.prod_eq_zero_iff, List.mem_map, not_exists, not_and]
+    intro j hj
+    exact hs j (List.mem_cons_of_mem _ hj)
 
 theorem chineseRemainderOfList_modEq_unique (l : List ι)
     (co : l.Pairwise (Coprime on s)) {z} (hz : ∀ i ∈ l, z ≡ a i [MOD s i]) :
     z ≡ chineseRemainderOfList a s l co [MOD (l.map s).prod] := by
   induction' l with i l ih
   · simp [modEq_one]
-  · simp [chineseRemainderOfList]
-    have : Coprime (s i) (l.map s).prod := coprime_list_prod_right_iff.mpr
-      (by simp; intro j hj; exact (List.pairwise_cons.mp co).1 j hj)
+  · simp only [List.map_cons, List.prod_cons, chineseRemainderOfList]
+    have : Coprime (s i) (l.map s).prod := by
+      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
+        forall_apply_eq_imp_iff₂]
+      intro j hj
+      exact (List.pairwise_cons.mp co).1 j hj
     exact chineseRemainder_modEq_unique this
-      (hz i (by simp)) (ih co.of_cons (fun j hj => hz j (by simp [hj])))
+      (hz i (List.mem_cons_self _ _)) (ih co.of_cons (fun j hj => hz j (List.mem_cons_of_mem _ hj)))
 
 theorem chineseRemainderOfList_perm {l l' : List ι} (hl : l.Perm l')
     (hs : ∀ i ∈ l, s i ≠ 0) (co : l.Pairwise (Coprime on s)) :
@@ -137,8 +155,8 @@ theorem chineseRemainderOfMultiset_lt_prod {m : Multiset ι}
 `a i` mod `s i` for all  `i ∈ t`. -/
 def chineseRemainderOfFinset (t : Finset ι)
     (hs : ∀ i ∈ t, s i ≠ 0) (pp : Set.Pairwise t (Coprime on s)) :
-    { k // ∀ i ∈ t, k ≡ a i [MOD s i] } :=
-  by simpa using chineseRemainderOfMultiset a s t.nodup (by simpa using hs) (by simpa using pp)
+    { k // ∀ i ∈ t, k ≡ a i [MOD s i] } := by
+  simpa using chineseRemainderOfMultiset a s t.nodup (by simpa using hs) (by simpa using pp)
 
 theorem chineseRemainderOfFinset_lt_prod {t : Finset ι}
     (hs : ∀ i ∈ t, s i ≠ 0) (pp : Set.Pairwise t (Coprime on s)) :