chore(*): remove some local attribute [semireducible]s (#17874)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

counterexamples/char_p_zero_ne_char_zero.lean

@@ -18,11 +18,8 @@ This file shows that there are semiring `R` for which `char_p R 0` holds and `ch
 The example is `{0, 1}` with saturating addition.
 -/
 
-local attribute [semireducible] with_zero
-
-@[simp] lemma add_one_eq_one : ∀ (x : with_zero unit), x + 1 = 1
-| 0 := rfl
-| 1 := rfl
+@[simp] lemma add_one_eq_one (x : with_zero unit) : x + 1 = 1 :=
+with_zero.cases_on x (by refl) (λ h, by refl)
 
 lemma with_zero_unit_char_p_zero : char_p (with_zero unit) 0 :=
 ⟨λ x, by cases x; simp⟩

src/data/int/range.lean

@@ -19,15 +19,13 @@ This could be unified with `data.list.intervals`. See the TODOs there.
 
 namespace int
 
-local attribute [semireducible] int.nonneg
-
 /-- List enumerating `[m, n)`. This is the ℤ variant of `list.Ico`. -/
 def range (m n : ℤ) : list ℤ :=
 (list.range (to_nat (n-m))).map $ λ r, m+r
 
 theorem mem_range_iff {m n r : ℤ} : r ∈ range m n ↔ m ≤ r ∧ r < n :=
 ⟨λ H, let ⟨s, h1, h2⟩ := list.mem_map.1 H in h2 ▸
-  ⟨le_add_of_nonneg_right trivial,
+  ⟨le_add_of_nonneg_right (coe_zero_le s),
   add_lt_of_lt_sub_left $ match n-m, h1 with
     | (k:ℕ), h1 := by rwa [list.mem_range, to_nat_coe_nat, ← coe_nat_lt] at h1
     end⟩,

src/data/nat/modeq.lean

@@ -247,8 +247,6 @@ by { apply modeq_cancel_left_of_coprime hmc, simpa [mul_comm] using h }
 
 end modeq
 
-local attribute [semireducible] int.nonneg
-
 /-- The natural number less than `lcm n m` congruent to `a` mod `n` and `b` mod `m` -/
 def chinese_remainder' (h : a ≡ b [MOD gcd n m]) : {k // k ≡ a [MOD n] ∧ k ≡ b [MOD m]} :=
 if hn : n = 0 then ⟨a, begin rw [hn, gcd_zero_left] at h, split, refl, exact h end⟩ else

src/ring_theory/localization/fraction_ring.lean

@@ -116,10 +116,14 @@ local attribute [semireducible] is_fraction_ring.inv
 
 protected lemma mul_inv_cancel (x : K) (hx : x ≠ 0) :
   x * is_fraction_ring.inv A x = 1 :=
-show x * dite _ _ _ = 1, by rw [dif_neg hx,
-  ←is_unit.mul_left_inj (map_units K ⟨(sec _ x).1, mem_non_zero_divisors_iff_ne_zero.2 $
-    λ h0, hx $ eq_zero_of_fst_eq_zero (sec_spec (non_zero_divisors A) x) h0⟩),
-  one_mul, mul_assoc, mk'_spec, ←eq_mk'_iff_mul_eq]; exact (mk'_sec _ x).symm
+show x * dite _ _ _ = 1, begin
+  rw [dif_neg hx, ←is_unit.mul_left_inj
+    (map_units K ⟨(sec _ x).1, mem_non_zero_divisors_iff_ne_zero.2 $
+      λ h0, hx $ eq_zero_of_fst_eq_zero (sec_spec (non_zero_divisors A) x) h0⟩),
+    one_mul, mul_assoc],
+  rw [mk'_spec, ←eq_mk'_iff_mul_eq],
+  exact (mk'_sec _ x).symm
+end
 
 /-- A `comm_ring` `K` which is the localization of an integral domain `R` at `R - {0}` is a field.
 See note [reducible non-instances]. -/

src/topology/constructions.lean

@@ -97,12 +97,11 @@ lemma is_closed_map_to_mul : is_closed_map (to_mul : additive α → α) := is_c
 lemma is_closed_map_of_add : is_closed_map (of_add : α → multiplicative α) := is_closed_map.id
 lemma is_closed_map_to_add : is_closed_map (to_add : multiplicative α → α) := is_closed_map.id
 
-local attribute [semireducible] nhds
-
-lemma nhds_of_mul (a : α) : 𝓝 (of_mul a) = map of_mul (𝓝 a) := rfl
-lemma nhds_of_add (a : α) : 𝓝 (of_add a) = map of_add (𝓝 a) := rfl
-lemma nhds_to_mul (a : additive α) : 𝓝 (to_mul a) = map to_mul (𝓝 a) := rfl
-lemma nhds_to_add (a : multiplicative α) : 𝓝 (to_add a) = map to_add (𝓝 a) := rfl
+lemma nhds_of_mul (a : α) : 𝓝 (of_mul a) = map of_mul (𝓝 a) := by { unfold nhds, refl, }
+lemma nhds_of_add (a : α) : 𝓝 (of_add a) = map of_add (𝓝 a) := by { unfold nhds, refl, }
+lemma nhds_to_mul (a : additive α) : 𝓝 (to_mul a) = map to_mul (𝓝 a) := by { unfold nhds, refl, }
+lemma nhds_to_add (a : multiplicative α) : 𝓝 (to_add a) = map to_add (𝓝 a) :=
+by { unfold nhds, refl, }
 
 end
 
@@ -129,10 +128,8 @@ lemma is_open_map_of_dual : is_open_map (of_dual : αᵒᵈ → α) := is_open_m
 lemma is_closed_map_to_dual : is_closed_map (to_dual : α → αᵒᵈ) := is_closed_map.id
 lemma is_closed_map_of_dual : is_closed_map (of_dual : αᵒᵈ → α) := is_closed_map.id
 
-local attribute [semireducible] nhds
-
-lemma nhds_to_dual (a : α) : 𝓝 (to_dual a) = map to_dual (𝓝 a) := rfl
-lemma nhds_of_dual (a : α) : 𝓝 (of_dual a) = map of_dual (𝓝 a) := rfl
+lemma nhds_to_dual (a : α) : 𝓝 (to_dual a) = map to_dual (𝓝 a) := by { unfold nhds, refl, }
+lemma nhds_of_dual (a : α) : 𝓝 (of_dual a) = map of_dual (𝓝 a) := by { unfold nhds, refl, }
 
 end