chore(*): protect some definitions to get rid of _root_ (#2846)

These were amongst the worst offenders.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/algebra/associated.lean

@@ -171,8 +171,8 @@ have h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z),
 have hp0: p ^ (k + l) ≠ 0, from pow_ne_zero _ hp.ne_zero,
 have hpd : p ∣ x * y, from ⟨z, by rwa [domain.mul_right_inj hp0] at h⟩,
 (hp.div_or_div hpd).elim
-  (λ ⟨d, hd⟩, or.inl ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
-  (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
+  (λ ⟨d, hd⟩, or.inl ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
+  (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
 
 /-- Two elements of a `monoid` are `associated` if one of them is another one
 multiplied by a unit on the right. -/

src/computability/primrec.lean

@@ -102,7 +102,7 @@ theorem mul : primrec (unpaired (*)) :=
 
 theorem pow : primrec (unpaired (^)) :=
 (prec (const 1) (mul.comp (pair (right.comp right) left))).of_eq $
-λ p, by simp; induction p.unpair.2; simp [*, pow_succ]
+λ p, by simp; induction p.unpair.2; simp [*, nat.pow_succ]
 
 end primrec
 

src/data/complex/exponential.lean

@@ -120,11 +120,11 @@ begin
     clear hn,
     induction n with n ih,
     { simp },
-    { rw [_root_.pow_succ, ← one_mul (1 : α)],
+    { rw [pow_succ, ← one_mul (1 : α)],
       refine mul_le_mul (le_of_lt hx1) ih (abv_pow abv x n ▸ abv_nonneg _ _) (by norm_num) } },
   { assume n hn,
     refine div_le_div_of_le_of_pos (sub_le_sub_left _ _) (sub_pos.2 hx1),
-    rw [← one_mul (_ ^ n), _root_.pow_succ],
+    rw [← one_mul (_ ^ n), pow_succ],
     exact mul_le_mul_of_nonneg_right (le_of_lt hx1) (pow_nonneg (abv_nonneg _ _) _) }
 end
 

src/data/list/basic.lean

@@ -2839,7 +2839,7 @@ end
 @[simp] theorem length_sublists' : ∀ l : list α, length (sublists' l) = 2 ^ length l
 | []     := rfl
 | (a::l) := by simp only [sublists'_cons, length_append, length_sublists' l, length_map,
-    length, pow_succ, mul_succ, mul_zero, zero_add]
+    length, nat.pow_succ, mul_succ, mul_zero, zero_add]
 
 @[simp] theorem sublists_nil : sublists (@nil α) = [[]] := rfl
 

src/data/monoid_algebra.lean

@@ -119,40 +119,40 @@ lemma one_def : (1 : monoid_algebra k G) = single 1 1 :=
 rfl
 
 -- TODO: the simplifier unfolds 0 in the instance proof!
-private lemma zero_mul (f : monoid_algebra k G) : 0 * f = 0 :=
+protected lemma zero_mul (f : monoid_algebra k G) : 0 * f = 0 :=
 by simp only [mul_def, sum_zero_index]
 
-private lemma mul_zero (f : monoid_algebra k G) : f * 0 = 0 :=
+protected lemma mul_zero (f : monoid_algebra k G) : f * 0 = 0 :=
 by simp only [mul_def, sum_zero_index, sum_zero]
 
 private lemma left_distrib (a b c : monoid_algebra k G) : a * (b + c) = a * b + a * c :=
-by simp only [mul_def, sum_add_index, mul_add, _root_.mul_zero, single_zero, single_add,
+by simp only [mul_def, sum_add_index, mul_add, mul_zero, single_zero, single_add,
   eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add]
 
 private lemma right_distrib (a b c : monoid_algebra k G) : (a + b) * c = a * c + b * c :=
-by simp only [mul_def, sum_add_index, add_mul, _root_.mul_zero, _root_.zero_mul, single_zero,
+by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul, single_zero,
   single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero, sum_add]
 
 instance : semiring (monoid_algebra k G) :=
 { one       := 1,
   mul       := (*),
-  one_mul   := assume f, by simp only [mul_def, one_def, sum_single_index, _root_.zero_mul,
+  one_mul   := assume f, by simp only [mul_def, one_def, sum_single_index, zero_mul,
     single_zero, sum_zero, zero_add, one_mul, sum_single],
-  mul_one   := assume f, by simp only [mul_def, one_def, sum_single_index, _root_.mul_zero,
+  mul_one   := assume f, by simp only [mul_def, one_def, sum_single_index, mul_zero,
     single_zero, sum_zero, add_zero, mul_one, sum_single],
-  zero_mul  := zero_mul,
-  mul_zero  := mul_zero,
+  zero_mul  := monoid_algebra.zero_mul,
+  mul_zero  := monoid_algebra.mul_zero,
   mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index,
     sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
-    add_mul, mul_add, add_assoc, mul_assoc, _root_.zero_mul, _root_.mul_zero, sum_zero, sum_add],
+    add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add],
   left_distrib  := left_distrib,
   right_distrib := right_distrib,
   .. finsupp.add_comm_monoid }
 
 @[simp] lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} :
   (single a₁ b₁ : monoid_algebra k G) * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂) :=
-(sum_single_index (by simp only [_root_.zero_mul, single_zero, sum_zero])).trans
-  (sum_single_index (by rw [_root_.mul_zero, single_zero]))
+(sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans
+  (sum_single_index (by rw [mul_zero, single_zero]))
 
 @[simp] lemma single_pow {a : G} {b : k} :
   ∀ n : ℕ, (single a b : monoid_algebra k G)^n = single (a^n) (b ^ n)
@@ -473,40 +473,40 @@ lemma one_def : (1 : add_monoid_algebra k G) = single 0 1 :=
 rfl
 
 -- TODO: the simplifier unfolds 0 in the instance proof!
-private lemma zero_mul (f : add_monoid_algebra k G) : 0 * f = 0 :=
+protected lemma zero_mul (f : add_monoid_algebra k G) : 0 * f = 0 :=
 by simp only [mul_def, sum_zero_index]
 
-private lemma mul_zero (f : add_monoid_algebra k G) : f * 0 = 0 :=
+protected lemma mul_zero (f : add_monoid_algebra k G) : f * 0 = 0 :=
 by simp only [mul_def, sum_zero_index, sum_zero]
 
 private lemma left_distrib (a b c : add_monoid_algebra k G) : a * (b + c) = a * b + a * c :=
-by simp only [mul_def, sum_add_index, mul_add, _root_.mul_zero, single_zero, single_add,
+by simp only [mul_def, sum_add_index, mul_add, mul_zero, single_zero, single_add,
   eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add]
 
 private lemma right_distrib (a b c : add_monoid_algebra k G) : (a + b) * c = a * c + b * c :=
-by simp only [mul_def, sum_add_index, add_mul, _root_.mul_zero, _root_.zero_mul, single_zero,
+by simp only [mul_def, sum_add_index, add_mul, mul_zero, zero_mul, single_zero,
   single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero, sum_add]
 
 instance : semiring (add_monoid_algebra k G) :=
 { one       := 1,
   mul       := (*),
-  one_mul   := assume f, by simp only [mul_def, one_def, sum_single_index, _root_.zero_mul,
+  one_mul   := assume f, by simp only [mul_def, one_def, sum_single_index, zero_mul,
     single_zero, sum_zero, zero_add, one_mul, sum_single],
-  mul_one   := assume f, by simp only [mul_def, one_def, sum_single_index, _root_.mul_zero,
+  mul_one   := assume f, by simp only [mul_def, one_def, sum_single_index, mul_zero,
     single_zero, sum_zero, add_zero, mul_one, sum_single],
-  zero_mul  := zero_mul,
-  mul_zero  := mul_zero,
+  zero_mul  := add_monoid_algebra.zero_mul,
+  mul_zero  := add_monoid_algebra.mul_zero,
   mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index,
     sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
-    add_mul, mul_add, add_assoc, mul_assoc, _root_.zero_mul, _root_.mul_zero, sum_zero, sum_add],
+    add_mul, mul_add, add_assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add],
   left_distrib  := left_distrib,
   right_distrib := right_distrib,
   .. finsupp.add_comm_monoid }
 
 lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} :
   (single a₁ b₁ : add_monoid_algebra k G) * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂) :=
-(sum_single_index (by simp only [_root_.zero_mul, single_zero, sum_zero])).trans
-  (sum_single_index (by rw [_root_.mul_zero, single_zero]))
+(sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans
+  (sum_single_index (by rw [mul_zero, single_zero]))
 
 section
 

src/data/nat/basic.lean

@@ -20,6 +20,11 @@ and extra recursors:
 
 universes u v
 
+run_cmd do env ← tactic.get_env,
+  tactic.set_env $
+  [``nat.pow_zero,
+   ``nat.pow_succ].foldl environment.mk_protected env
+
 instance : canonically_ordered_comm_semiring ℕ :=
 { le_iff_exists_add := assume a b,
   ⟨assume h, let ⟨c, hc⟩ := nat.le.dest h in ⟨c, hc.symm⟩,
@@ -894,7 +899,7 @@ attribute [simp] nat.pow_zero nat.pow_one
 | (k+1) := show 1^k * 1 = 1, by rw [mul_one, one_pow]
 
 theorem pow_add (a m n : ℕ) : a^(m + n) = a^m * a^n :=
-by induction n; simp [*, pow_succ, mul_assoc]
+by induction n; simp [*, nat.pow_succ, mul_assoc]
 
 theorem pow_two (a : ℕ) : a ^ 2 = a * a := show (1 * a) * a = _, by rw one_mul
 

src/data/nat/choose.lean

@@ -98,14 +98,14 @@ begin
         rw[pow_succ y, mul_assoc, mul_assoc, mul_assoc, mul_assoc] } }
   end,
   induction n with n ih,
-  { rw [_root_.pow_zero, sum_range_succ, range_zero, sum_empty, add_zero],
+  { rw [pow_zero, sum_range_succ, range_zero, sum_empty, add_zero],
     dsimp [t], rw [choose_self, nat.cast_one, mul_one, mul_one] },
   { rw[sum_range_succ', h_first],
     rw[finset.sum_congr rfl (h_middle n), finset.sum_add_distrib, add_assoc],
     rw[pow_succ (x + y), ih, add_mul, finset.mul_sum, finset.mul_sum],
     congr' 1,
     rw[finset.sum_range_succ', finset.sum_range_succ, h_first, h_last,
-       mul_zero, zero_add, _root_.pow_succ] }
+       mul_zero, zero_add, pow_succ] }
 end
 
 /-- The binomial theorem-/

src/data/nat/parity.lean

@@ -87,7 +87,7 @@ begin
 end
 
 @[parity_simps] theorem even_pow {m n : nat} : even (m^n) ↔ even m ∧ n ≠ 0 :=
-by { induction n with n ih; simp [*, pow_succ, even_mul], tauto }
+by { induction n with n ih; simp [*, nat.pow_succ, even_mul], tauto }
 
 lemma even_div {a b : ℕ} : even (a / b) ↔ a % (2 * b) / b = 0 :=
 by rw [even, dvd_iff_mod_eq_zero, nat.div_mod_eq_mod_mul_div, mul_comm]

src/data/nat/prime.lean

@@ -445,14 +445,14 @@ begin
   induction m with m IH generalizing i, {simp [pow_succ, le_zero_iff] at *},
   by_cases p ∣ i,
   { cases h with a e, subst e,
-    rw [pow_succ, mul_comm (p^m) p, nat.mul_dvd_mul_iff_left pp.pos, IH],
+    rw [nat.pow_succ, mul_comm (p^m) p, nat.mul_dvd_mul_iff_left pp.pos, IH],
     split; intro h; rcases h with ⟨k, h, e⟩,
     { exact ⟨succ k, succ_le_succ h, by rw [mul_comm, e]; refl⟩ },
     cases k with k,
     { apply pp.not_dvd_one.elim,
       simp at e, rw ← e, apply dvd_mul_right },
     { refine ⟨k, le_of_succ_le_succ h, _⟩,
-      rwa [mul_comm, pow_succ, nat.mul_left_inj pp.pos] at e } },
+      rwa [mul_comm, nat.pow_succ, nat.mul_left_inj pp.pos] at e } },
   { split; intro d,
     { rw (pp.coprime_pow_of_not_dvd h).eq_one_of_dvd d,
       exact ⟨0, zero_le _, rfl⟩ },

src/data/nat/sqrt.lean

@@ -98,15 +98,15 @@ private lemma sqrt_aux_is_sqrt (n) : ∀ m r,
 | (m+1) r h₁ h₂ := begin
     apply sqrt_aux_is_sqrt_lemma
       (m+1) r n h₁ (2^m * 2^m)
-      (by simp [shiftr, pow_succ, div2_val, mul_comm, mul_left_comm];
+      (by simp [shiftr, nat.pow_succ, div2_val, mul_comm, mul_left_comm];
           repeat {rw @nat.mul_div_cancel_left _ 2 dec_trivial});
       intros,
     { have := sqrt_aux_is_sqrt m r h₁ a,
-      simpa [pow_succ, mul_comm, mul_assoc] },
-    { rw [pow_succ, mul_two, ← add_assoc] at h₂,
+      simpa [nat.pow_succ, mul_comm, mul_assoc] },
+    { rw [nat.pow_succ, mul_two, ← add_assoc] at h₂,
       have := sqrt_aux_is_sqrt m (r + 2^(m+1)) a h₂,
       rwa show (r + 2^(m + 1)) * 2^(m+1) = 2 * (r + 2^(m + 1)) * 2^m,
-          by simp [pow_succ, mul_comm, mul_left_comm] }
+          by simp [nat.pow_succ, mul_comm, mul_left_comm] }
   end
 
 private lemma sqrt_is_sqrt (n : ℕ) : is_sqrt n (sqrt n) :=

src/data/padics/padic_norm.lean

@@ -209,7 +209,7 @@ A rewrite lemma for `padic_val_rat p (q^k) with condition `q ≠ 0`.
 protected lemma pow {q : ℚ} (hq : q ≠ 0) {k : ℕ} :
     padic_val_rat p (q ^ k) = k * padic_val_rat p q :=
 by induction k; simp [*, padic_val_rat.mul _ hq (pow_ne_zero _ hq),
-  _root_.pow_succ, add_mul, add_comm]
+  pow_succ, add_mul, add_comm]
 
 /--
 A rewrite lemma for `padic_val_rat p (q⁻¹)` with condition `q ≠ 0`.

src/data/pnat/basic.lean

@@ -166,7 +166,7 @@ instance coe_mul_hom : is_monoid_hom (coe : ℕ+ → ℕ) :=
 
 @[simp] theorem pow_coe (m : ℕ+) (n : ℕ) : ((m ^ n : ℕ+) : ℕ) = (m : ℕ) ^ n :=
 by induction n with n ih;
- [refl, rw [nat.pow_succ, _root_.pow_succ, mul_coe, mul_comm, ih]]
+ [refl, rw [nat.pow_succ, pow_succ, mul_coe, mul_comm, ih]]
 
 instance : left_cancel_semigroup ℕ+ :=
 { mul_left_cancel := λ a b c h, by {

src/data/real/cardinality.lean

@@ -32,7 +32,7 @@ by simp [cantor_function_aux, h]
 
 lemma cantor_function_aux_succ (f : ℕ → bool) :
   (λ n, cantor_function_aux c f (n + 1)) = λ n, c * cantor_function_aux c (λ n, f (n + 1)) n :=
-by { ext n, cases h : f (n + 1); simp [h, _root_.pow_succ] }
+by { ext n, cases h : f (n + 1); simp [h, pow_succ] }
 
 lemma summable_cantor_function (f : ℕ → bool) (h1 : 0 ≤ c) (h2 : c < 1) :
   summable (cantor_function_aux c f) :=

src/data/real/cau_seq.lean

@@ -83,7 +83,7 @@ abs_sub_le_iff.2 ⟨sub_abv_le_abv_sub abv _ _,
 
 lemma abv_pow {β : Type*} [domain β] (abv : β → α) [is_absolute_value abv]
   (a : β) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
-by induction n; simp [abv_mul abv, _root_.pow_succ, abv_one abv, *]
+by induction n; simp [abv_mul abv, pow_succ, abv_one abv, *]
 
 end is_absolute_value
 

src/number_theory/sum_four_squares.lean

@@ -32,7 +32,7 @@ calc 2 * 2 * m = (x - y)^2 + (x + y)^2 : by rw [mul_assoc, h]; ring
 ... = (2 * ((x - y) / 2))^2 + (2 * ((x + y) / 2))^2 :
   by rw [int.mul_div_cancel' hxsuby, int.mul_div_cancel' hxaddy]
 ... = 2 * 2 * (((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2) :
-  by simp [mul_add, _root_.pow_succ, mul_comm, mul_assoc, mul_left_comm]
+  by simp [mul_add, pow_succ, mul_comm, mul_assoc, mul_left_comm]
 
 lemma exists_sum_two_squares_add_one_eq_k (p : ℕ) [hp : fact p.prime] :
   ∃ (a b : ℤ) (k : ℕ), a^2 + b^2 + 1 = k * p ∧ k < p :=

src/ring_theory/multiplicity.lean

@@ -283,15 +283,15 @@ lemma finite_mul_iff {p a b : α} (hp : prime p) : finite p (a * b) ↔ finite p
 
 lemma finite_pow {p a : α} (hp : prime p) : Π {k : ℕ} (ha : finite p a), finite p (a ^ k)
 | 0     ha := ⟨0, by simp [mt is_unit_iff_dvd_one.2 hp.2.1]⟩
-| (k+1) ha := by rw [_root_.pow_succ]; exact finite_mul hp ha (finite_pow ha)
+| (k+1) ha := by rw [pow_succ]; exact finite_mul hp ha (finite_pow ha)
 
 variable [decidable_rel ((∣) : α → α → Prop)]
 
 @[simp] lemma multiplicity_self {a : α} (ha : ¬is_unit a) (ha0 : a ≠ 0) :
   multiplicity a a = 1 :=
 eq_some_iff.2 ⟨by simp, λ ⟨b, hb⟩, ha (is_unit_iff_dvd_one.2
   ⟨b, (domain.mul_right_inj ha0).1 $ by clear _fun_match;
-    simpa [_root_.pow_succ, mul_assoc] using hb⟩)⟩
+    simpa [pow_succ, mul_assoc] using hb⟩)⟩
 
 @[simp] lemma get_multiplicity_self {a : α} (ha : finite a a) :
   get (multiplicity a a) ha = 1 :=
@@ -353,13 +353,13 @@ end
 protected lemma pow' {p a : α} (hp : prime p) (ha : finite p a) : ∀ {k : ℕ},
   get (multiplicity p (a ^ k)) (finite_pow hp ha) = k * get (multiplicity p a) ha
 | 0     := by dsimp [_root_.pow_zero]; simp [one_right hp.not_unit]; refl
-| (k+1) := by dsimp only [_root_.pow_succ];
+| (k+1) := by dsimp only [pow_succ];
   erw [multiplicity.mul' hp, pow', add_mul, one_mul, add_comm]
 
 lemma pow {p a : α} (hp : prime p) : ∀ {k : ℕ},
   multiplicity p (a ^ k) = k •ℕ (multiplicity p a)
 | 0        := by simp [one_right hp.not_unit]
-| (succ k) := by simp [_root_.pow_succ, succ_nsmul, pow, multiplicity.mul hp]
+| (succ k) := by simp [pow_succ, succ_nsmul, pow, multiplicity.mul hp]
 
 lemma multiplicity_pow_self {p : α} (h0 : p ≠ 0) (hu : ¬ is_unit p) (n : ℕ) :
   multiplicity p (p ^ n) = n :=

src/topology/basic.lean

@@ -49,6 +49,13 @@ universes u v w
 
 attribute [class] topological_space
 
+run_cmd do env ← tactic.get_env,
+  tactic.set_env $
+  [``topological_space.is_open,
+   ``topological_space.is_open_univ,
+   ``topological_space.is_open_inter,
+   ``topological_space.is_open_sUnion].foldl environment.mk_protected env
+
 /-- A constructor for topologies by specifying the closed sets,
 and showing that they satisfy the appropriate conditions. -/
 def topological_space.of_closed {α : Type u} (T : set (set α))

test/ring_exp.lean

@@ -177,7 +177,7 @@ def pow_sub_pow_factor (x y : α) : Π {i : ℕ},{z // x^i - y^i = z*(x - y)}
 begin
   cases @pow_sub_pow_factor (k+1) with z hz,
   existsi z*x + y^(k+1),
-  rw [_root_.pow_succ x, _root_.pow_succ y, ←sub_add_sub_cancel (x*x^(k+1)) (x*y^(k+1)),
+  rw [pow_succ x, pow_succ y, ←sub_add_sub_cancel (x*x^(k+1)) (x*y^(k+1)),
   ←mul_sub x, hz],
   ring_exp_eq
 end