diff --git a/Analysis/Appendix_B_2.lean b/Analysis/Appendix_B_2.lean
index 2910da9e..bf888736 100644
--- a/Analysis/Appendix_B_2.lean
+++ b/Analysis/Appendix_B_2.lean
@@ -1,5 +1,9 @@
 import Mathlib.Tactic
 import Analysis.Appendix_B_1
+import Mathlib.Tactic.Push
+
+-- Tag rpow lemmas for push/pull
+attribute [push] NNReal.rpow_add NNReal.rpow_neg NNReal.rpow_mul NNReal.rpow_sub NNReal.rpow_add_one NNReal.rpow_natCast
 
 /-!
 # Analysis I, Appendix B.2: The decimal representation of real numbers
@@ -61,7 +65,7 @@ theorem NNRealDecimal.surj (x:NNReal) : ∃ d:NNRealDecimal, x = d := by
     rw [ha n]; calc
       _ = s n * (10:NNReal)^(-n:ℝ) + a n * 10^(-n-1:ℝ) := by
         simp [add_mul]; ring_nf; congr 1
-        rw [mul_assoc, ←rpow_add_one]; ring_nf; norm_num
+        rw [mul_assoc]; pull (disch := norm_num) _ ^ _; congr 1; ring
       _ = s 0 + (∑ i ∈ .range n, a i * (10:NNReal)^(-i-1:ℝ) + a n * 10^(-n-1:ℝ)) := by grind
       _ = _ := by congr; symm; apply Finset.sum_range_succ
   have := (d.toNNReal_conv.tendsto_sum_tsum_nat).const_add (s 0:NNReal)
@@ -96,14 +100,14 @@ theorem NNRealDecimal.not_inj : (1:NNReal) = (mk 1 fun _ ↦ 0) ∧ (1:NNReal) =
     . simp
     rw [Finset.sum_range_succ, hn, Nat.cast_add, Nat.cast_one, neg_add']
     have : (10:NNReal)^(-n:ℝ) = 10^(-n-1:ℝ) * 10 := by
-      rw [←rpow_add_one]; simp; norm_num
+      pull (disch := norm_num) _ ^ _; congr 1; ring
     simp [this, ←coe_inj]
     rw [NNReal.coe_sub, NNReal.coe_sub]
     . suffices h : ∀ c a : ℝ, c = 9 → 1 - a * 10 + c * a = 1 - a by apply h; norm_cast
       grind
     . apply rpow_le_one_of_one_le_of_nonpos; norm_num; linarith
-    rw [←rpow_add_one]
-    apply rpow_le_one_of_one_le_of_nonpos; norm_num; linarith; norm_num
+    pull (disch := norm_num) _ ^ _
+    apply rpow_le_one_of_one_le_of_nonpos; norm_num; linarith
   convert Filter.Tendsto.const_sub (f := fun n:ℕ ↦ (10:NNReal)^(-n:ℝ)) (c := 0) 1 _; simp
   convert tendsto_pow_atTop_nhds_zero_of_lt_one (show (1/10:NNReal) < 1 by bound) with n
   rw [←rpow_natCast, one_div, inv_rpow, rpow_neg]
diff --git a/Analysis/MeasureTheory/Section_1_2_1.lean b/Analysis/MeasureTheory/Section_1_2_1.lean
index 5a0bb7bc..d03f685c 100644
--- a/Analysis/MeasureTheory/Section_1_2_1.lean
+++ b/Analysis/MeasureTheory/Section_1_2_1.lean
@@ -1,6 +1,10 @@
 import Analysis.MeasureTheory.Section_1_2_0
 import Analysis.Misc.«Real-EReal-ENNReal»
 import Analysis.Misc.Combinatorics
+import Mathlib.Tactic.Push
+
+-- Tag zpow lemmas for push/pull
+attribute [push] zpow_add₀ zpow_sub₀ zpow_neg
 
 /-!
 # Introduction to Measure Theory, Section 1.2.1: Properties of Lebesgue outer measure
@@ -4499,9 +4503,7 @@ lemma nesting {d:ℕ} {n m : ℤ} {a : Fin d → ℤ} {b : Fin d → ℤ} :
       have h2m_pos : (0:ℝ) < 2^m := zpow_pos (by norm_num : (0:ℝ) < 2) m
       have h_mn_pos : 0 < m - n := Int.sub_pos_of_lt hn
       have h_zpow_eq : (2:ℝ)^(m-n) * 2^n = 2^m := by
-        rw [← zpow_add₀ (by norm_num : (2:ℝ) ≠ 0)]
-        congr 1
-        omega
+        pull (disch := norm_num) _ ^ _; congr 1; omega
       -- hi says: if a_i/2^n ≤ b_i/2^m then (a_i+1)/2^n < (b_i+1)/2^m
       -- Case 1: a_i/2^n > b_i/2^m (the hypothesis of hi fails)
       -- Case 2: a_i/2^n ≤ b_i/2^m but (a_i+1)/2^n < (b_i+1)/2^m (hi applies)
@@ -4519,12 +4521,12 @@ lemma nesting {d:ℕ} {n m : ℤ} {a : Fin d → ℤ} {b : Fin d → ℤ} :
             simp only [div_mul_cancel₀ _ (ne_of_gt h2m_pos)] at h1
             calc (b i : ℝ) < (a i : ℝ) / 2^n * 2^m := h1
               _ = (a i : ℝ) * (2^m / 2^n) := by ring
-              _ = (a i : ℝ) * 2^(m-n) := by rw [← zpow_sub₀ (by norm_num : (2:ℝ) ≠ 0)]
+              _ = (a i : ℝ) * 2^(m-n) := by pull (disch := norm_num) _ ^ _; rfl
           have hhi : (a i : ℝ) * 2^(m-n) < (b i : ℝ) + 1 := by
             have h1 : (a i : ℝ) / 2^n * 2^m < ((b i : ℝ) + 1) / 2^m * 2^m := by nlinarith
             simp only [div_mul_cancel₀ _ (ne_of_gt h2m_pos)] at h1
             calc (a i : ℝ) * 2^(m-n) = (a i : ℝ) * (2^m / 2^n) := by
-                    rw [← zpow_sub₀ (by norm_num : (2:ℝ) ≠ 0)]
+                    pull (disch := norm_num) _ ^ _; rfl
               _ = (a i : ℝ) / 2^n * 2^m := by ring
               _ < (b i : ℝ) + 1 := h1
           -- a_i * 2^(m-n) is an integer in (b_i, b_i+1), contradiction
@@ -4554,12 +4556,12 @@ lemma nesting {d:ℕ} {n m : ℤ} {a : Fin d → ℤ} {b : Fin d → ℤ} :
             simp only [div_mul_cancel₀ _ (ne_of_gt h2m_pos)] at h1
             calc (b i : ℝ) < ((a i : ℝ) + 1) / 2^n * 2^m := h1
               _ = ((a i : ℝ) + 1) * (2^m / 2^n) := by ring
-              _ = ((a i : ℝ) + 1) * 2^(m-n) := by rw [← zpow_sub₀ (by norm_num : (2:ℝ) ≠ 0)]
+              _ = ((a i : ℝ) + 1) * 2^(m-n) := by pull (disch := norm_num) _ ^ _; rfl
           have hhi : ((a i : ℝ) + 1) * 2^(m-n) < (b i : ℝ) + 1 := by
             have h1 : ((a i : ℝ) + 1) / 2^n * 2^m < ((b i : ℝ) + 1) / 2^m * 2^m := by nlinarith
             simp only [div_mul_cancel₀ _ (ne_of_gt h2m_pos)] at h1
             calc ((a i : ℝ) + 1) * 2^(m-n) = ((a i : ℝ) + 1) * (2^m / 2^n) := by
-                    rw [← zpow_sub₀ (by norm_num : (2:ℝ) ≠ 0)]
+                    pull (disch := norm_num) _ ^ _; rfl
               _ = ((a i : ℝ) + 1) / 2^n * 2^m := by ring
               _ < (b i : ℝ) + 1 := h1
           -- (a_i+1) * 2^(m-n) is an integer in (b_i, b_i+1), contradiction
@@ -4617,12 +4619,12 @@ lemma nesting {d:ℕ} {n m : ℤ} {a : Fin d → ℤ} {b : Fin d → ℤ} :
             simp only [div_mul_cancel₀ _ (ne_of_gt h2n_pos)] at h1
             calc (a i : ℝ) < (b i : ℝ) / 2^m * 2^n := h1
               _ = (b i : ℝ) * (2^n / 2^m) := by ring
-              _ = (b i : ℝ) * 2^(n-m) := by rw [← zpow_sub₀ (by norm_num : (2:ℝ) ≠ 0)]
+              _ = (b i : ℝ) * 2^(n-m) := by pull (disch := norm_num) _ ^ _; rfl
           have hhi : (b i : ℝ) * 2^(n-m) < (a i : ℝ) + 1 := by
             have h1 : (b i : ℝ) / 2^m * 2^n < ((a i : ℝ) + 1) / 2^n * 2^n := by nlinarith
             simp only [div_mul_cancel₀ _ (ne_of_gt h2n_pos)] at h1
             calc (b i : ℝ) * 2^(n-m) = (b i : ℝ) * (2^n / 2^m) := by
-                    rw [← zpow_sub₀ (by norm_num : (2:ℝ) ≠ 0)]
+                    pull (disch := norm_num) _ ^ _; rfl
               _ = (b i : ℝ) / 2^m * 2^n := by ring
               _ < (a i : ℝ) + 1 := h1
           -- b_i * 2^(n-m) is an integer in (a_i, a_i+1), contradiction
@@ -4652,12 +4654,12 @@ lemma nesting {d:ℕ} {n m : ℤ} {a : Fin d → ℤ} {b : Fin d → ℤ} :
             simp only [div_mul_cancel₀ _ (ne_of_gt h2n_pos)] at h1
             calc (a i : ℝ) < ((b i : ℝ) + 1) / 2^m * 2^n := h1
               _ = ((b i : ℝ) + 1) * (2^n / 2^m) := by ring
-              _ = ((b i : ℝ) + 1) * 2^(n-m) := by rw [← zpow_sub₀ (by norm_num : (2:ℝ) ≠ 0)]
+              _ = ((b i : ℝ) + 1) * 2^(n-m) := by pull (disch := norm_num) _ ^ _; rfl
           have hhi : ((b i : ℝ) + 1) * 2^(n-m) < (a i : ℝ) + 1 := by
             have h1 : ((b i : ℝ) + 1) / 2^m * 2^n < ((a i : ℝ) + 1) / 2^n * 2^n := by nlinarith
             simp only [div_mul_cancel₀ _ (ne_of_gt h2n_pos)] at h1
             calc ((b i : ℝ) + 1) * 2^(n-m) = ((b i : ℝ) + 1) * (2^n / 2^m) := by
-                    rw [← zpow_sub₀ (by norm_num : (2:ℝ) ≠ 0)]
+                    pull (disch := norm_num) _ ^ _; rfl
               _ = ((b i : ℝ) + 1) / 2^m * 2^n := by ring
               _ < (a i : ℝ) + 1 := h1
           -- (b_i+1) * 2^(n-m) is an integer in (a_i, a_i+1), contradiction
diff --git a/Analysis/MeasureTheory/Section_1_3_5.lean b/Analysis/MeasureTheory/Section_1_3_5.lean
index db655d41..644f3c0a 100644
--- a/Analysis/MeasureTheory/Section_1_3_5.lean
+++ b/Analysis/MeasureTheory/Section_1_3_5.lean
@@ -334,12 +334,10 @@ theorem ComplexAbsolutelyIntegrable.approx_by_simple {d:ℕ} {f: EuclideanSpace'
   -- Re/Im of f - g
   have hfg_re : Complex.re_fun (f - g) = Complex.re_fun f - g_re := by
     ext x; simp only [Complex.re_fun, hg_def, Pi.sub_apply, Pi.add_apply, Pi.smul_apply,
-      smul_eq_mul, Real.complex_fun, Complex.sub_re, Complex.add_re, Complex.ofReal_re,
-      Complex.mul_re, Complex.I_re, Complex.I_im, Complex.ofReal_im]; ring
+      smul_eq_mul, Real.complex_fun]; push Complex.re; ring
   have hfg_im : Complex.im_fun (f - g) = Complex.im_fun f - g_im := by
     ext x; simp only [Complex.im_fun, hg_def, Pi.sub_apply, Pi.add_apply, Pi.smul_apply,
-      smul_eq_mul, Real.complex_fun, Complex.sub_im, Complex.add_im, Complex.ofReal_im,
-      Complex.mul_im, Complex.I_re, Complex.I_im, Complex.ofReal_re]; ring
+      smul_eq_mul, Real.complex_fun]; push Complex.im; ring
   -- Pointwise: |f-g| ≤ |Re(f-g)| + |Im(f-g)|
   have h_bound : ∀ x, EReal.abs_fun (f - g) x ≤
       (EReal.abs_fun (Complex.re_fun (f - g)) + EReal.abs_fun (Complex.im_fun (f - g))) x :=
diff --git a/Analysis/Section_6_7.lean b/Analysis/Section_6_7.lean
index ff2b8d96..fcf3d918 100644
--- a/Analysis/Section_6_7.lean
+++ b/Analysis/Section_6_7.lean
@@ -1,6 +1,10 @@
 import Mathlib.Tactic
 import Analysis.Section_5_epilogue
 import Analysis.Section_6_6
+import Mathlib.Tactic.Push
+
+-- Tag rpow lemmas for push/pull
+attribute [push] Real.rpow_add Real.rpow_neg Real.rpow_mul Real.rpow_sub Real.rpow_natCast
 
 /-!
 # Analysis I, Section 6.7: Real exponentiation, part II
@@ -56,25 +60,25 @@ lemma ratPow_continuous {x α:ℝ} (hx: x > 0) {q: ℕ → ℚ}
   . replace : x^(q m:ℝ) ≤ x^(q n:ℝ) := by rw [rpow_le_rpow_left_iff h]; norm_cast
     rw [abs_of_nonneg (by linarith)]
     calc
-      _ = x^(q m:ℝ) * (x^(q n - q m:ℝ) - 1) := by ring_nf; rw [←rpow_add (by linarith)]; ring_nf
+      _ = x^(q m:ℝ) * (x^(q n - q m:ℝ) - 1) := by ring_nf; pull (disch := positivity) _ ^ _; ring_nf
       _ ≤ x^M * (x^(1/(K+1:ℝ)) - 1) := by
         gcongr <;> try exact h'
         . rw [sub_nonneg]; apply one_le_rpow h'; norm_cast; linarith
         . specialize hbound m; simp_all [abs_le']
         grind [abs_le']
       _ ≤ x^M * (ε * x^(-M)) := by gcongr; grind [abs_le']
-      _ = ε := by rw [mul_comm, mul_assoc, ←rpow_add]; simp; linarith
+      _ = ε := by rw [mul_comm, mul_assoc]; pull (disch := positivity) _ ^ _; simp
   replace : x^(q n:ℝ) ≤ x^(q m:ℝ) := by rw [rpow_le_rpow_left_iff h]; norm_cast; linarith
   rw [abs_of_nonpos (by linarith)]
   calc
-    _ = x^(q n:ℝ) * (x^(q m - q n:ℝ) - 1) := by ring_nf; rw [←rpow_add]; ring_nf; positivity
+    _ = x^(q n:ℝ) * (x^(q m - q n:ℝ) - 1) := by ring_nf; pull (disch := positivity) _ ^ _; ring_nf
     _ ≤ x^M * (x^(1/(K+1:ℝ)) - 1) := by
       gcongr <;> try exact h'
       . rw [sub_nonneg]; apply one_le_rpow h'; norm_cast; linarith
       . specialize hbound n; simp_all [abs_le']
       grind [abs_le']
     _ ≤ x^M * (ε * x^(-M)) := by gcongr; simp_all [abs_le']
-    _ = ε := by rw [mul_comm, mul_assoc, ←rpow_add]; simp; positivity
+    _ = ε := by rw [mul_comm, mul_assoc]; pull (disch := positivity) _ ^ _; simp
 
 
 lemma ratPow_lim_uniq {x α:ℝ} (hx: x > 0) {q q': ℕ → ℚ}
@@ -89,7 +93,7 @@ lemma ratPow_lim_uniq {x α:ℝ} (hx: x > 0) {q q': ℕ → ℚ}
     convert (lim_mul (b := (fun n ↦ x^(r n:ℝ):Sequence)) (ratPow_continuous hx hq') this.1).2
     . rw [mul_coe]
       rcongr _ n
-      rw [←rpow_add (by linarith)]
+      pull (disch := positivity) _ ^ _
       simp [r]
     exact this.2.symm
   intro ε hε
@@ -115,7 +119,7 @@ lemma ratPow_lim_uniq {x α:ℝ} (hx: x > 0) {q q': ℕ → ℚ}
   . simp; linarith
   have h5 : x ^ (r n.toNat:ℝ) ≤ x^(K + 1:ℝ)⁻¹ := by gcongr; linarith; simp_all [r]
   have h6 : (x^(K + 1:ℝ)⁻¹)⁻¹ ≤ x ^ (r n.toNat:ℝ) := by
-    rw [←rpow_neg (by linarith)]
+    pull (disch := positivity) _ ^ _
     gcongr; linarith
     simp [r]; linarith
   split_ands <;> linarith
@@ -160,7 +164,7 @@ theorem Real.ratPow_add {x:ℝ} (hx: x > 0) (q r:ℝ) : rpow x (q+r) = rpow x q
   have h1 := ratPow_continuous hx hq'
   have h2 := ratPow_continuous hx hr'
   rw [rpow_eq_lim_ratPow hx hq', rpow_eq_lim_ratPow hx hr', rpow_eq_lim_ratPow hx hq'r', ←(lim_mul h1 h2).2, mul_coe]
-  rcongr n; rw [←rpow_add]; simp; linarith
+  rcongr n; pull (disch := positivity) _ ^ _; norm_cast
 
 
 /-- Proposition 6.7.3(b) / Exercise 6.7.1 -/