merge #312

Std/Data/Array/Init/Lemmas.lean

@@ -131,7 +131,7 @@ theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
 
 @[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
   simp only [push, getElem_eq_data_get, List.concat_eq_append]
-  rw [List.get_append_right] <;> simp [getElem_eq_data_get]
+  rw [List.get_append_right] <;> simp [getElem_eq_data_get, Nat.zero_lt_one]
 
 theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
     (a.push x)[i] = if h : i < a.size then a[i] else x := by

Std/Data/Char.lean

@@ -12,12 +12,12 @@ private theorem csize_eq (c) :
     csize c = 1 ∨ csize c = 2 ∨ csize c = 3 ∨
     csize c = 4 := by
   simp only [csize, Char.utf8Size]
-  repeat (first | split | (solve | simp))
+  repeat (first | split | (solve | simp (config := {decide := true})))
 
 theorem csize_pos (c) : 0 < csize c := by
-  rcases csize_eq c with _|_|_|_ <;> simp_all
+  rcases csize_eq c with _|_|_|_ <;> simp_all (config := {decide := true})
 
 theorem csize_le_4 (c) : csize c ≤ 4 := by
-  rcases csize_eq c with _|_|_|_ <;> simp_all
+  rcases csize_eq c with _|_|_|_ <;> simp_all (config := {decide := true})
 
 end String

Std/Data/Fin/Lemmas.lean

@@ -645,7 +645,7 @@ theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
   exists_fin_succ.trans <| or_congr_right exists_fin_one
 
 theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by
-  simp [forall_fin_two]
+  simp only [forall_fin_two]; decide
 
 /--
 Define `motive i` by reverse induction on `i : Fin (n + 1)` via induction on the underlying `Nat`

Std/Data/Int/DivMod.lean

@@ -30,11 +30,11 @@ theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(div m b +
 
 @[simp] protected theorem zero_div : ∀ b : Int, div 0 b = 0
   | ofNat _ => show ofNat _ = _ by simp
-  | -[_+1] => show -ofNat _ = _ by simp
+  | -[_+1] => show -ofNat _ = _ by simp; rfl
 
 @[local simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
   | ofNat _ => show ofNat _ = _ by simp
-  | -[_+1] => show -ofNat _ = _ by simp
+  | -[_+1] => show -ofNat _ = _ by simp; rfl
 
 @[simp] theorem zero_fdiv (b : Int) : fdiv 0 b = 0 := by cases b <;> rfl
 
@@ -174,7 +174,7 @@ theorem add_mul_ediv_left (a : Int) {b : Int}
   Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H
 
 theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
-  if h : c = 0 then by simp [h] else by
+  if h : c = 0 then by simp [h]; rfl else by
     let ⟨k, hk⟩ := H
     rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
       ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]
@@ -736,7 +736,7 @@ protected theorem mul_ediv_assoc' (b : Int) {a c : Int}
   rw [Int.mul_comm, Int.mul_ediv_assoc _ h, Int.mul_comm]
 
 theorem div_dvd_div : ∀ {a b c : Int}, a ∣ b → b ∣ c → b.div a ∣ c.div a
-  | a, _, _, ⟨b, rfl⟩, ⟨c, rfl⟩ => if az : a = 0 then by simp [az] else by
+  | a, _, _, ⟨b, rfl⟩, ⟨c, rfl⟩ => if az : a = 0 then by simp_arith [az] else by
     rw [Int.mul_div_cancel_left _ az, Int.mul_assoc, Int.mul_div_cancel_left _ az]
     apply Int.dvd_mul_right
 
@@ -807,7 +807,7 @@ theorem fdiv_eq_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → a.fdiv b = a / b
     rw [mul_fdiv_cancel_left _ bz, mul_ediv_cancel_left _ bz]
 
 theorem neg_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → (-a) / b = -(a / b)
-  | _, b, ⟨c, rfl⟩ => by if bz : b = 0 then simp [bz] else
+  | _, b, ⟨c, rfl⟩ => by if bz : b = 0 then simp [bz]; rfl else
     rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]
 
 theorem sub_ediv_of_dvd (a : Int) {b c : Int}

Std/Data/List/Count.lean

@@ -51,11 +51,11 @@ theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a
     if h : p x then
       rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
       · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
-      · simp only [h]
+      · simp only [h, not_true_eq_false, decide_False, not_false_eq_true]
     else
       rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
       · rfl
-      · simp only [h]
+      · simp only [h, not_false_eq_true, decide_True]
 
 theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
   induction l with

Std/Data/List/Lemmas.lean

@@ -1968,8 +1968,8 @@ theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l := drop
 theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)
   | [], _, _ => by simp
   | x :: xs, hl, h => by
-    cases m <;> cases n <;> simp only [disjoint_cons_left, mem_cons, disjoint_cons_right,
-      drop, true_or, eq_self_iff_true, not_true, false_and, not_mem_nil, disjoint_nil_left, take]
+    cases m <;> cases n <;> simp only [disjoint_cons_left, drop, not_mem_nil, disjoint_nil_left,
+      take, not_false_eq_true, and_self]
     · case succ.zero => cases h
     · cases hl with | cons h₀ h₁ =>
       refine ⟨fun h => h₀ _ (mem_of_mem_drop h) rfl, ?_⟩
@@ -2122,7 +2122,7 @@ theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by
   simp only [range_eq_range', range'_sublist_right]
 
 theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by
-  simp only [range_eq_range', range'_subset_right]
+  simp only [range_eq_range', range'_subset_right, lt_succ_self]
 
 @[simp]
 theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n := by

Std/Data/Nat/Lemmas.lean

@@ -827,7 +827,7 @@ theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
   | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
 
 theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
-  match n % 2, @Nat.mod_lt n 2 (by simp) with
+  match n % 2, @Nat.mod_lt n 2 (by decide) with
   | 0, _ => .inl rfl
   | 1, _ => .inr rfl
 
@@ -972,7 +972,9 @@ theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   | k+1 =>
     rw [log2]; split
     · have n0 : 0 < n / 2 := (Nat.le_div_iff_mul_le (by decide)).2 ‹_›
-      simp [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0), le_div_iff_mul_le, Nat.pow_succ]
+      simp only [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0), le_div_iff_mul_le,
+        Nat.pow_succ]
+      exact Nat.le_div_iff_mul_le (by decide)
     · simp only [le_zero_eq, succ_ne_zero, false_iff]
       refine mt (Nat.le_trans ?_) ‹_›
       exact Nat.pow_le_pow_of_le_right (Nat.succ_pos 1) (Nat.le_add_left 1 k)

Std/Data/Rat/Lemmas.lean

@@ -126,7 +126,7 @@ theorem mk_eq_divInt (num den nz c) : ⟨num, den, nz, c⟩ = num /. (den : Nat)
 
 theorem divInt_self (a : Rat) : a.num /. a.den = a := by rw [divInt_ofNat, mkRat_self]
 
-@[simp] theorem zero_divInt (n) : 0 /. n = 0 := by cases n <;> simp [divInt]
+@[simp] theorem zero_divInt (n) : 0 /. n = 0 := by cases n <;> simp [divInt]; rfl
 
 @[simp] theorem divInt_zero (n) : n /. 0 = 0 := mkRat_zero n
 
@@ -215,7 +215,7 @@ theorem neg_normalize (n d z) : -normalize n d z = normalize (-n) d z := by
   simp [normalize, maybeNormalize_eq]; ext <;> simp [Int.neg_div]
 
 theorem neg_mkRat (n d) : -mkRat n d = mkRat (-n) d := by
-  if z : d = 0 then simp [z] else simp [← normalize_eq_mkRat z, neg_normalize]
+  if z : d = 0 then simp [z]; rfl else simp [← normalize_eq_mkRat z, neg_normalize]
 
 theorem neg_divInt (n d) : -(n /. d) = -n /. d := by
   rcases Int.eq_nat_or_neg d with ⟨_, rfl | rfl⟩ <;> simp [divInt_neg', neg_mkRat]
@@ -300,7 +300,7 @@ theorem inv_def (a : Rat) : a.inv = a.den /. a.num := by
 
 @[simp] protected theorem inv_zero : (0 : Rat).inv = 0 := by
   unfold Rat.inv
-  simp
+  rfl
 
 @[simp] theorem inv_divInt (n d : Int) : (n /. d).inv = d /. n := by
   if z : d = 0 then simp [z] else

Std/Logic.lean

@@ -77,7 +77,7 @@ theorem not_iff_false_intro (h : a) : ¬a ↔ False := iff_false_intro (not_not_
 theorem iff_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ↔ b) ↔ (c ↔ d) :=
   ⟨fun h => h₁.symm.trans <| h.trans h₂, fun h => h₁.trans <| h.trans h₂.symm⟩
 
-@[simp] theorem not_true : (¬True) ↔ False := iff_false_intro (not_not_intro ⟨⟩)
+theorem not_true : (¬True) ↔ False := iff_false_intro (not_not_intro ⟨⟩)
 
 theorem not_false_iff : (¬False) ↔ True := iff_true_intro not_false