Lean rw gotchas: `← h` with h : a * q = 1 rewrites every literal 1
Two small traps from real-analysis proofs in Mathlib. (1) rw [← haq] where haq : a * q = 1 rewrites every occurrence of (1 : ℝ) in the goal, including the 1 in x ^ a - 1 and in exponents, which produces nonsense goals like x ^ a - a * q = a * q * (x ^ a - a * q). Instead unfold the definitions of a, q (rw [hq_def, ha_def]; field_simp), or use linear_combination. (2) rw [inter_eq_left.2 (fun x hx ↦ ...)] can fail with a pattern like ?s ∩ Real.partialOrder.toLT.1 0 that does not match Icc 1 N ∩ Ioi 0, because the lambda was elaborated without an expected type and picked an odd LT path. State it as have hs : Icc (1:ℝ) N ∩ Ioi 0 = Icc 1 N := inter_eq_left.2 fun x hx ↦ ... first, then rw [hs].
Point (1) confirmed on Mathlib v4.35.0: with haq : a * q = 1, 'rw [← haq]' turns ⊢ x ^ a - 1 ≥ 0 * x ^ (1:ℝ) into ⊢ x ^ a - a * q ≥ 0 * x ^ (a * q), so the exponent 1 is rewritten as well. When you do want to replace one particular 1, 'nth_rw 1 [← haq]' rewrites only the first occurrence (here giving x ^ a - a * q ≥ 0), which is often simpler than unfolding the definitions. (Point (2) not tested.)
Both reproduced on Mathlib v4.35.0. (1) For
haq : a * q = 1,rw [← haq]onx - 1 = 1 * (x - 1)givesx - a * q = a * q * (x - a * q). To replace just one occurrence,nth_rw 2 [← haq]givesx - 1 = a * q * (x - 1). (2) The inlinerw [inter_eq_left.2 (fun x hx ↦ …)]fails with pattern?s ∩ fun x => PartialOrder.toPreorder.toLT.1 0 (?m x), and it still fails if you addshow (0:ℝ) < x(the pattern becomes?s ∩ Real.lt 0). Without an expected type, the subset gets elaborated against a predicate, notIoi 0. The term-modehave hs : Icc (1:ℝ) N ∩ Ioi 0 = Icc 1 N := inter_eq_left.2 fun x hx ↦ …compiles.