chore: exact by decide -> decide (#12067)

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/Algebra/Polynomial/Div.lean

@@ -701,7 +701,7 @@ theorem eval_divByMonic_pow_rootMultiplicity_ne_zero {p : R[X]} (a : R) (hp : p
   exact
     multiplicity.is_greatest'
       (multiplicity_finite_of_degree_pos_of_monic
-        (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; exact by decide)
+        (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
         (monic_X_sub_C _) hp)
       (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)
 #align polynomial.eval_div_by_monic_pow_root_multiplicity_ne_zero Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero

Mathlib/Data/Nat/Bits.lean

@@ -258,7 +258,7 @@ lemma bodd_bit (b n) : bodd (bit b n) = b := by
 lemma div2_bit (b n) : div2 (bit b n) = n := by
   rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
   <;> cases b
-  <;> exact by decide
+  <;> decide
 #align nat.div2_bit Nat.div2_bit
 
 lemma shiftLeft'_add (b m n) : ∀ k, shiftLeft' b m (n + k) = shiftLeft' b (shiftLeft' b m n) k

Mathlib/Data/Nat/Prime.lean

@@ -389,7 +389,7 @@ theorem not_prime_iff_minFac_lt {n : ℕ} (n2 : 2 ≤ n) : ¬Prime n ↔ minFac
 
 theorem minFac_le_div {n : ℕ} (pos : 0 < n) (np : ¬Prime n) : minFac n ≤ n / minFac n :=
   match minFac_dvd n with
-  | ⟨0, h0⟩ => absurd pos <| by rw [h0, mul_zero]; exact by decide
+  | ⟨0, h0⟩ => absurd pos <| by rw [h0, mul_zero]; decide
   | ⟨1, h1⟩ => by
     rw [mul_one] at h1
     rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, or_false_iff,

Mathlib/Data/Num/Lemmas.lean

@@ -810,7 +810,7 @@ theorem lt_iff_cmp {m n} : m < n ↔ cmp m n = Ordering.lt :=
 #align pos_num.lt_iff_cmp PosNum.lt_iff_cmp
 
 theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ Ordering.gt :=
-  not_congr <| lt_iff_cmp.trans <| by rw [← cmp_swap]; cases cmp m n <;> exact by decide
+  not_congr <| lt_iff_cmp.trans <| by rw [← cmp_swap]; cases cmp m n <;> decide
 #align pos_num.le_iff_cmp PosNum.le_iff_cmp
 
 end PosNum
@@ -865,7 +865,7 @@ theorem lt_iff_cmp {m n} : m < n ↔ cmp m n = Ordering.lt :=
 #align num.lt_iff_cmp Num.lt_iff_cmp
 
 theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ Ordering.gt :=
-  not_congr <| lt_iff_cmp.trans <| by rw [← cmp_swap]; cases cmp m n <;> exact by decide
+  not_congr <| lt_iff_cmp.trans <| by rw [← cmp_swap]; cases cmp m n <;> decide
 #align num.le_iff_cmp Num.le_iff_cmp
 
 theorem castNum_eq_bitwise {f : Num → Num → Num} {g : Bool → Bool → Bool}

Mathlib/FieldTheory/Finite/Basic.lean

@@ -90,9 +90,9 @@ theorem exists_root_sum_quadratic [Fintype R] {f g : R[X]} (hf2 : degree f = 2)
       _ < natDegree f * (univ.image fun x : R => eval x f).card +
             natDegree (-g) * (univ.image fun x : R => eval x (-g)).card :=
         (add_lt_add_of_lt_of_le
-          (lt_of_le_of_ne (card_image_polynomial_eval (by rw [hf2]; exact by decide))
+          (lt_of_le_of_ne (card_image_polynomial_eval (by rw [hf2]; decide))
             (mt (congr_arg (· % 2)) (by simp [natDegree_eq_of_degree_eq_some hf2, hR])))
-          (card_image_polynomial_eval (by rw [degree_neg, hg2]; exact by decide)))
+          (card_image_polynomial_eval (by rw [degree_neg, hg2]; decide)))
       _ = 2 * ((univ.image fun x : R => eval x f) ∪ univ.image fun x : R => eval x (-g)).card := by
         rw [card_union_of_disjoint hd];
           simp [natDegree_eq_of_degree_eq_some hf2, natDegree_eq_of_degree_eq_some hg2, mul_add]

Mathlib/Init/Data/Bool/Lemmas.lean

@@ -124,7 +124,7 @@ theorem of_decide_true {p : Prop} [Decidable p] : decide p → p :=
   (decide_iff p).1
 #align of_to_bool_true Bool.of_decide_true
 
-theorem bool_iff_false {b : Bool} : ¬b ↔ b = false := by cases b <;> exact by decide
+theorem bool_iff_false {b : Bool} : ¬b ↔ b = false := by cases b <;> decide
 #align bool_iff_false Bool.bool_iff_false
 
 theorem bool_eq_false {b : Bool} : ¬b → b = false :=
@@ -157,7 +157,7 @@ theorem coe_and_iff (a b : Bool) : a && b ↔ a ∧ b := by simp
 #align band_coe_iff Bool.coe_and_iff
 
 theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by
-  cases a <;> cases b <;> exact by decide
+  cases a <;> cases b <;> decide
 #align bxor_coe_iff Bool.coe_xor_iff
 
 @[simp]

Mathlib/NumberTheory/PythagoreanTriples.lean

@@ -420,7 +420,7 @@ private theorem coprime_sq_sub_sq_sum_of_odd_odd {m n : ℤ} (h : Int.gcd m n =
   have h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)) := by ring
   have h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0 := by
     rw [h2, Int.mul_ediv_cancel_left, Int.mul_emod_right]
-    exact by decide
+    decide
   refine' ⟨⟨_, h1⟩, ⟨_, h2⟩, h3, _⟩
   have h20 : (2 : ℤ) ≠ 0 := by decide
   rw [h1, h2, Int.mul_ediv_cancel_left _ h20, Int.mul_ediv_cancel_left _ h20]

Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean

@@ -89,7 +89,7 @@ theorem prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [hp : Fact p.Prime] (h
     by_contradiction fun hpi =>
       let ⟨a, b, hab⟩ := sq_add_sq_of_nat_prime_of_not_irreducible p hpi
       have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ ↑p := by
-        erw [← ZMod.nat_cast_mod p 4, hp3]; exact by decide
+        erw [← ZMod.nat_cast_mod p 4, hp3]; decide
       this a b (hab ▸ by simp)
 #align gaussian_int.prime_of_nat_prime_of_mod_four_eq_three GaussianInt.prime_of_nat_prime_of_mod_four_eq_three
 

Mathlib/Order/Compare.lean

@@ -143,7 +143,7 @@ theorem swap_orElse (o₁ o₂) : (orElse o₁ o₂).swap = orElse o₁.swap o
 #align ordering.swap_or_else Ordering.swap_orElse
 
 theorem orElse_eq_lt (o₁ o₂) : orElse o₁ o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by
-  cases o₁ <;> cases o₂ <;> exact by decide
+  cases o₁ <;> cases o₂ <;> decide
 #align ordering.or_else_eq_lt Ordering.orElse_eq_lt
 
 end Ordering

Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

@@ -179,7 +179,7 @@ theorem unique_irreducible ⦃p q : R⦄ (hp : Irreducible p) (hq : Irreducible
   · obtain rfl : n = 0 := by
       clear hn this
       revert H n
-      exact by decide
+      decide
     simp [not_irreducible_one, pow_zero] at this
   · simpa only [pow_one] using hn.symm
   · obtain ⟨n, rfl⟩ : ∃ k, n = 1 + k + 1 := Nat.exists_eq_add_of_lt H