feat(algebra/ordered_field): rewrite and cleanup (#3751)

Group similar lemmas in a more intuitive way
Add docstrings, module doc and section headers
Simplify some proofs
Remove some implications if they had a corresponding `iff` lemma.
Add some more variants of some lemmas
Rename some lemmas for consistency
List of name changes (the lemma on the right might be a bi-implication, if the original version was an implication):
`add_midpoint` -> `add_sub_div_two_lt`
`le_div_of_mul_le`, `mul_le_of_le_div` -> `le_div_iff`
`lt_div_of_mul_lt`, `mul_lt_of_lt_div` -> `lt_div_iff`
`div_le_of_le_mul` -> `div_le_iff'`
`le_mul_of_div_le` -> `div_le_iff`
`div_lt_of_pos_of_lt_mul` -> `div_lt_iff'`
`mul_le_of_neg_of_div_le`, `div_le_of_neg_of_mul_le` -> `div_le_iff_of_neg`
`mul_lt_of_neg_of_div_lt`, `div_lt_of_neg_of_mul_lt` -> `div_lt_iff_of_neg`
`div_le_div_of_pos_of_le` -> `div_le_div_of_le`
`div_le_div_of_neg_of_le` -> `div_le_div_of_nonpos_of_le`
`div_lt_div_of_pos_of_lt` -> `div_lt_div_of_lt`
`div_mul_le_div_mul_of_div_le_div_nonneg` -> `div_mul_le_div_mul_of_div_le_div`
`one_le_div_of_le`, `le_of_one_le_div`, `one_le_div_iff_le` -> `one_le_div`
`one_lt_div_of_lt`, `lt_of_one_lt_div`, `one_lt_div_iff_lt` -> `one_lt_div`
`div_le_one_iff_le` -> `div_le_one`
`div_lt_one_iff_lt` -> `div_lt_one`
`one_div_le_of_pos_of_one_div_le` -> `one_div_le`
`one_div_le_of_neg_of_one_div_le` -> `one_div_le_of_neg`
`div_lt_div_of_pos_of_lt_of_pos` -> `div_lt_div_of_lt_left`

One regression I noticed in some other files: when using `div_le_iff`, and the argument is proven by some lemma about `linear_ordered_semiring` then Lean gives a type mismatch. Presumably this happens because the instance chain `ordered_field -> has_le` doesn't go via `ordered_semiring`. The fix is to give the type explicitly, for example using `div_le_iff (t : (0 : ℝ) < _)`

src/algebra/continued_fractions/computation/approximations.lean

@@ -77,12 +77,11 @@ begin
     ∧ int_fract_pair.of ifp_n.fr⁻¹ = ifp_succ_n, from
       succ_nth_stream_eq_some_iff.elim_left succ_nth_stream_eq,
   change 1 ≤ ⌊ifp_n.fr⁻¹⌋,
-  suffices : 1 ≤ ifp_n.fr⁻¹, by { rw_mod_cast [le_floor], assumption },
-  suffices : 1 * ifp_n.fr ≤ 1, by
-  { rw inv_eq_one_div,
-    have : 0 < ifp_n.fr, from
+  suffices : 1 ≤ ifp_n.fr⁻¹, { rw_mod_cast [le_floor], assumption },
+  suffices : ifp_n.fr ≤ 1,
+  { have h : 0 < ifp_n.fr :=
       lt_of_le_of_ne (nth_stream_fr_nonneg nth_stream_eq) stream_nth_fr_ne_zero.symm,
-    solve_by_elim [le_div_of_mul_le], },
+    apply one_le_inv h this },
   simp [(le_of_lt (nth_stream_fr_lt_one nth_stream_eq))]
 end
 

src/analysis/normed_space/basic.lean

@@ -287,7 +287,7 @@ lemma antilipschitz_with.add_lipschitz_with {α : Type*} [metric_space α] {Kf :
 begin
   refine antilipschitz_with.of_le_mul_dist (λ x y, _),
   rw [nnreal.coe_inv, ← div_eq_inv_mul],
-  apply le_div_of_mul_le (nnreal.coe_pos.2 $ nnreal.sub_pos.2 hK),
+  rw le_div_iff (nnreal.coe_pos.2 $ nnreal.sub_pos.2 hK),
   rw [mul_comm, nnreal.coe_sub (le_of_lt hK), sub_mul],
   calc ↑Kf⁻¹ * dist x y - Kg * dist x y ≤ dist (f x) (f y) - dist (g x) (g y) :
     sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)

src/analysis/normed_space/multilinear.lean

@@ -328,8 +328,9 @@ begin
     rw [this, norm_zero],
     exact mul_nonneg (op_norm_nonneg f) A },
   { have hlt : 0 < ∏ i, ∥m i∥ := lt_of_le_of_ne A (ne.symm h),
-    exact le_mul_of_div_le hlt ((le_Inf _ bounds_nonempty bounds_bdd_below).2
-      (λ c ⟨_, hc⟩, div_le_of_le_mul hlt (begin rw mul_comm, apply hc, end))) }
+    rw [← div_le_iff hlt],
+    apply (le_Inf _ bounds_nonempty bounds_bdd_below).2,
+    rintro c ⟨_, hc⟩, rw [div_le_iff hlt], apply hc }
 end
 
 lemma ratio_le_op_norm : ∥f m∥ / ∏ i, ∥m i∥ ≤ ∥f∥ :=

src/analysis/normed_space/operator_norm.lean

@@ -252,8 +252,8 @@ theorem le_op_norm : ∥f x∥ ≤ ∥f∥ * ∥x∥ :=
 classical.by_cases
   (λ heq : x = 0, by { rw heq, simp })
   (λ hne, have hlt : 0 < ∥x∥, from norm_pos_iff.2 hne,
-    le_mul_of_div_le hlt ((le_Inf _ bounds_nonempty bounds_bdd_below).2
-    (λ c ⟨_, hc⟩, div_le_of_le_mul hlt (by { rw mul_comm, apply hc }))))
+    (div_le_iff hlt).mp ((le_Inf _ bounds_nonempty bounds_bdd_below).2
+    (λ c ⟨_, hc⟩, (div_le_iff hlt).mpr $ by { apply hc })))
 
 theorem le_op_norm_of_le {c : ℝ} {x} (h : ∥x∥ ≤ c) : ∥f x∥ ≤ ∥f∥ * c :=
 le_trans (f.le_op_norm x) (mul_le_mul_of_nonneg_left h f.op_norm_nonneg)
@@ -264,9 +264,7 @@ lipschitz_with.of_dist_le_mul $ λ x y,
   by { rw [dist_eq_norm, dist_eq_norm, ←map_sub], apply le_op_norm }
 
 lemma ratio_le_op_norm : ∥f x∥ / ∥x∥ ≤ ∥f∥ :=
-(or.elim (lt_or_eq_of_le (norm_nonneg _))
-  (λ hlt, div_le_of_le_mul hlt (by { rw mul_comm, apply le_op_norm }))
-  (λ heq, by { rw [←heq, div_zero], apply op_norm_nonneg }))
+div_le_iff_of_nonneg_of_le (norm_nonneg _) f.op_norm_nonneg (le_op_norm _ _)
 
 /-- The image of the unit ball under a continuous linear map is bounded. -/
 lemma unit_le_op_norm : ∥x∥ ≤ 1 → ∥f x∥ ≤ ∥f∥ :=

src/analysis/normed_space/real_inner_product.lean

@@ -449,7 +449,7 @@ begin
   by_cases h : 0 = abs (∥x∥ * ∥y∥),
   { rw [←h, div_zero],
     norm_num },
-  { apply div_le_of_le_mul (lt_of_le_of_ne (ge_iff_le.mp (abs_nonneg (∥x∥ * ∥y∥))) h),
+  { rw div_le_iff' (lt_of_le_of_ne (ge_iff_le.mp (abs_nonneg (∥x∥ * ∥y∥))) h),
     convert abs_inner_le_norm x y using 1,
     rw [abs_mul, abs_of_nonneg (norm_nonneg x), abs_of_nonneg (norm_nonneg y), mul_one] }
 end

src/analysis/normed_space/riesz_lemma.lean

@@ -35,7 +35,7 @@ begin
   let r' := max r 2⁻¹,
   have hr' : r' < 1, by { simp [r', hr], norm_num },
   have hlt : 0 < r' := lt_of_lt_of_le (by norm_num) (le_max_right r 2⁻¹),
-  have hdlt : d < d / r', from lt_div_of_mul_lt hlt ((mul_lt_iff_lt_one_right hdp).2 hr'),
+  have hdlt : d < d / r', from (lt_div_iff hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr'),
   obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' :=
     metric.exists_dist_lt_of_inf_dist_lt hdlt hFn,
   have x_ne_y₀ : x - y₀ ∉ F,

src/analysis/special_functions/exp_log.lean

@@ -434,7 +434,7 @@ begin
       exp y = exp y * 1 : by simp
       ... ≤ exp y * (exp y / y)^n : begin
           apply mul_le_mul_of_nonneg_left (one_le_pow_of_one_le _ n) (le_of_lt (exp_pos _)),
-          apply one_le_div_of_le _ y_pos,
+          rw one_le_div y_pos,
           apply le_trans _ (add_one_le_exp_of_nonneg (le_of_lt y_pos)),
           exact le_add_of_le_of_nonneg (le_refl _) (zero_le_one)
         end

src/analysis/special_functions/pow.lean

@@ -91,16 +91,16 @@ have (log x * (↑n)⁻¹).im = (log x).im / n,
 have h : -π < (log x * (↑n)⁻¹).im ∧ (log x * (↑n)⁻¹).im ≤ π,
   from (le_total (log x).im 0).elim
     (λ h, ⟨calc -π < (log x).im : by simp [log, neg_pi_lt_arg]
-            ... ≤ ((log x).im * 1) / n : le_div_of_mul_le (nat.cast_pos.2 hn)
+            ... ≤ ((log x).im * 1) / n : (le_div_iff (nat.cast_pos.2 hn : (0 : ℝ) < _)).mpr
               (mul_le_mul_of_nonpos_left (by rw ← nat.cast_one; exact nat.cast_le.2 hn) h)
             ... = (log x * (↑n)⁻¹).im : by simp [this],
           this.symm ▸ le_trans (div_nonpos_of_nonpos_of_nonneg h n.cast_nonneg)
             (le_of_lt real.pi_pos)⟩)
     (λ h, ⟨this.symm ▸ lt_of_lt_of_le (neg_neg_of_pos real.pi_pos)
             (div_nonneg h n.cast_nonneg),
           calc (log x * (↑n)⁻¹).im = (1 * (log x).im) / n : by simp [this]
-            ... ≤ (log x).im : (div_le_of_le_mul (nat.cast_pos.2 hn)
-              (mul_le_mul_of_nonneg_right (by rw ← nat.cast_one; exact nat.cast_le.2 hn) h))
+            ... ≤ (log x).im : (div_le_iff' (nat.cast_pos.2 hn : (0 : ℝ) < _)).mpr
+              (mul_le_mul_of_nonneg_right (by rw ← nat.cast_one; exact nat.cast_le.2 hn) h)
             ... ≤ _ : by simp [log, arg_le_pi]⟩),
 by rw [← cpow_nat_cast, ← cpow_mul _ h.1 h.2,
     inv_mul_cancel (show (n : ℂ) ≠ 0, from nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 hn)),

src/data/complex/basic.lean

@@ -434,13 +434,11 @@ by simpa [re_add_im] using abs_add z.re (z.im * I)
 
 lemma abs_re_div_abs_le_one (z : ℂ) : abs' (z.re / z.abs) ≤ 1 :=
 if hz : z = 0 then by simp [hz, zero_le_one]
-else by rw [_root_.abs_div, abs_abs]; exact
-  div_le_of_le_mul (abs_pos.2 hz) (by rw mul_one; exact abs_re_le_abs _)
+else by { simp_rw [_root_.abs_div, abs_abs, div_le_iff (abs_pos.2 hz), one_mul, abs_re_le_abs] }
 
 lemma abs_im_div_abs_le_one (z : ℂ) : abs' (z.im / z.abs) ≤ 1 :=
 if hz : z = 0 then by simp [hz, zero_le_one]
-else by rw [_root_.abs_div, abs_abs]; exact
-  div_le_of_le_mul (abs_pos.2 hz) (by rw mul_one; exact abs_im_le_abs _)
+else by { simp_rw [_root_.abs_div, abs_abs, div_le_iff (abs_pos.2 hz), one_mul, abs_im_le_abs] }
 
 @[simp, norm_cast] lemma abs_cast_nat (n : ℕ) : abs (n : ℂ) = n :=
 by rw [← of_real_nat_cast, abs_of_nonneg (nat.cast_nonneg n)]

src/data/complex/exponential.lean

@@ -137,7 +137,7 @@ begin
   refine @is_cau_of_mono_bounded _ _ _ _ ((1 : α) / (1 - abv x)) 0 _ _,
   { assume n hn,
     rw abs_of_nonneg,
-    refine div_le_div_of_pos_of_le (sub_pos.2 hx1)
+    refine div_le_div_of_le (le_of_lt $ sub_pos.2 hx1)
       (sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)),
     refine div_nonneg (sub_nonneg.2 _) (sub_nonneg.2 $ le_of_lt hx1),
     clear hn,
@@ -146,7 +146,7 @@ begin
     { 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_pos_of_le (sub_pos.2 hx1) (sub_le_sub_left _ _),
+    refine div_le_div_of_le (le_of_lt $ sub_pos.2 hx1) (sub_le_sub_left _ _),
     rw [← one_mul (_ ^ n), pow_succ],
     exact mul_le_mul_of_nonneg_right (le_of_lt hx1) (pow_nonneg (abv_nonneg _ _) _) }
 end
@@ -1129,7 +1129,7 @@ calc 0 < x - x ^ 3 / 6 - abs' x ^ 4 * (5 / 96) :
     (by rwa [_root_.abs_of_nonneg (le_of_lt hx0)]))).2
 
 lemma sin_pos_of_pos_of_le_two {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 2) : 0 < sin x :=
-have x / 2 ≤ 1, from div_le_of_le_mul (by norm_num) (by simpa),
+have x / 2 ≤ 1, from (div_le_iff (by norm_num)).mpr (by simpa),
 calc 0 < 2 * sin (x / 2) * cos (x / 2) :
   mul_pos (mul_pos (by norm_num) (sin_pos_of_pos_of_le_one (half_pos hx0) this))
     (cos_pos_of_le_one (by rwa [_root_.abs_of_nonneg (le_of_lt (half_pos hx0))]))

src/data/padics/hensel.lean

@@ -111,7 +111,7 @@ calc T = ∥F.eval a∥ / ∥((F.derivative.eval a)^2 : ℚ_[p])∥ : normed_fie
    ... = ∥F.eval a∥ / ∥(F.derivative.eval a)∥^2 : by simp [pow, monoid.pow]
 
 private lemma T_lt_one : T < 1 :=
-let h := (div_lt_one_iff_lt deriv_sq_norm_pos).2 hnorm in
+let h := (div_lt_one deriv_sq_norm_pos).2 hnorm in
 by rw T_def; apply h
 
 private lemma T_pow {n : ℕ} (hn : n > 0) : T ^ n < 1 :=
@@ -367,10 +367,9 @@ tendsto_nhds_unique newton_seq_dist_tendsto' newton_seq_dist_tendsto
 
 private lemma soln_dist_to_a_lt_deriv : ∥soln - a∥ < ∥F.derivative.eval a∥ :=
 begin
-  rw soln_dist_to_a,
-  apply div_lt_of_pos_of_lt_mul,
-  { apply deriv_norm_pos; assumption },
-  { rwa _root_.pow_two at hnorm }
+  rw [soln_dist_to_a, div_lt_iff],
+  { rwa _root_.pow_two at hnorm },
+  { apply deriv_norm_pos, assumption }
 end
 
 private lemma eval_soln : F.eval soln = 0 :=

src/data/padics/padic_numbers.lean

@@ -629,10 +629,10 @@ lemma exi_rat_seq_conv {ε : ℚ} (hε : 0 < ε) :
 begin
   refine (exists_nat_gt (1/ε)).imp (λ N hN i hi, _),
   have h := classical.some_spec (rat_dense' (f i) (div_nat_pos i)),
-  refine lt_of_lt_of_le h (div_le_of_le_mul (by exact_mod_cast succ_pos _) _),
+  refine lt_of_lt_of_le h ((div_le_iff' $ by exact_mod_cast succ_pos _).mpr _),
   rw right_distrib,
   apply le_add_of_le_of_nonneg,
-  { exact le_mul_of_div_le hε (le_trans (le_of_lt hN) (by exact_mod_cast hi)) },
+  { exact (div_le_iff hε).mp (le_trans (le_of_lt hN) (by exact_mod_cast hi)) },
   { apply le_of_lt, simpa }
 end
 

src/data/real/basic.lean

@@ -447,7 +447,7 @@ end,
       ← le_div_iff (div_pos h _30), div_div_cancel' (ne_of_gt h)],
     apply add_le_add,
     { simpa using (mul_le_mul_left (@two_pos ℝ _)).2 (Sup_le_ub _ ⟨_, lb⟩ ub) },
-    { rw [div_le_one_iff_le _30],
+    { rw [div_le_one _30],
       refine le_trans (sub_le_self _ (mul_self_nonneg _)) (le_trans x1 _),
       exact (le_add_iff_nonneg_left _).2 (le_of_lt two_pos) } }
 end

src/data/real/cardinality.lean

@@ -74,7 +74,7 @@ begin
     apply lt_of_le_of_lt (cantor_function_le (le_of_lt h1) h3 hf_max),
     apply lt_of_lt_of_le _ (cantor_function_le (le_of_lt h1) h3 hg_min),
     have : c / (1 - c) < 1,
-    { rw [div_lt_one_iff_lt, lt_sub_iff_add_lt],
+    { rw [div_lt_one, lt_sub_iff_add_lt],
       { convert add_lt_add h2 h2, norm_num },
       rwa sub_pos },
     convert this,

src/data/real/conjugate_exponents.lean

@@ -78,7 +78,7 @@ lemma mul_eq_add : p * q = p + q :=
 by simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj
 
 @[symm] protected lemma symm : q.is_conjugate_exponent p :=
-{ one_lt := by { rw [h.conj_eq], exact one_lt_div_of_lt _ h.sub_one_pos (sub_one_lt p) },
+{ one_lt := by { rw [h.conj_eq], exact (one_lt_div h.sub_one_pos).mpr (sub_one_lt p) },
   inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj }
 
 end is_conjugate_exponent

src/data/real/hyperreal.lean

@@ -511,7 +511,7 @@ is_st_iff_abs_sub_lt_delta.mpr $ λ d hd,
         field_simp [this, @two_ne_zero ℝ* _, add_mul, mul_add, mul_assoc, mul_comm, mul_left_comm] }
   ... < (d / 2 * 1 + d / 2 : ℝ*) :
         add_lt_add_right (mul_lt_mul_of_pos_left
-        ((div_lt_one_iff_lt $ lt_of_le_of_lt (abs_nonneg x) ht).mpr ht) $
+        ((div_lt_one $ lt_of_le_of_lt (abs_nonneg x) ht).mpr ht) $
         half_pos $ coe_pos.2 hd) _
   ... = (d : ℝ*) : by rw [mul_one, add_halves]
 

src/data/real/pi.lean

@@ -10,8 +10,8 @@ namespace real
 lemma pi_gt_sqrt_two_add_series (n : ℕ) : 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) < pi :=
 begin
   have : sqrt (2 - sqrt_two_add_series 0 n) / 2 * 2 ^ (n+2) < pi,
-  { apply mul_lt_of_lt_div, apply pow_pos, norm_num,
-    rw [←sin_pi_over_two_pow_succ], apply sin_lt, apply div_pos pi_pos, apply pow_pos, norm_num },
+  { rw [← lt_div_iff, ←sin_pi_over_two_pow_succ], apply sin_lt, apply div_pos pi_pos,
+    all_goals { apply pow_pos, norm_num } },
   apply lt_of_le_of_lt (le_of_eq _) this,
   rw [pow_succ _ (n+1), ←mul_assoc, div_mul_cancel, mul_comm], norm_num
 end
@@ -20,23 +20,24 @@ lemma pi_lt_sqrt_two_add_series (n : ℕ) :
   pi < 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) + 1 / 4 ^ n :=
 begin
   have : pi < (sqrt (2 - sqrt_two_add_series 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n+2),
-  { rw [←div_lt_iff, ←sin_pi_over_two_pow_succ],
+  { rw [← div_lt_iff, ← sin_pi_over_two_pow_succ],
     refine lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _,
     { apply div_pos pi_pos, apply pow_pos, norm_num },
-    { apply div_le_of_le_mul, apply pow_pos, norm_num, refine le_trans pi_le_four _,
-      simp only [show ((4 : ℝ) = 2 ^ 2), by norm_num, mul_one],
-      apply pow_le_pow, norm_num, apply le_add_of_nonneg_left, apply nat.zero_le },
+    { rw div_le_iff',
+      { refine le_trans pi_le_four _,
+        simp only [show ((4 : ℝ) = 2 ^ 2), by norm_num, mul_one],
+        apply pow_le_pow, norm_num, apply le_add_of_nonneg_left, apply nat.zero_le },
+        { apply pow_pos, norm_num }},
     apply add_le_add_left, rw div_le_div_right,
-    apply le_div_of_mul_le, apply pow_pos, apply pow_pos, norm_num,
-    rw [←mul_pow],
+    rw [le_div_iff, ←mul_pow],
     refine le_trans _ (le_of_eq (one_pow 3)), apply pow_le_pow_of_le_left,
     { apply le_of_lt, apply mul_pos, apply div_pos pi_pos, apply pow_pos, norm_num, apply pow_pos,
       norm_num },
-    apply mul_le_of_le_div, apply pow_pos, norm_num,
+    rw ← le_div_iff,
     refine le_trans ((div_le_div_right _).mpr pi_le_four) _, apply pow_pos, norm_num,
     rw [pow_succ, pow_succ, ←mul_assoc, ←div_div_eq_div_mul],
-    convert le_refl _, norm_num, norm_num,
-    apply pow_pos, norm_num },
+    convert le_refl _,
+    all_goals { repeat {apply pow_pos}, norm_num }},
   apply lt_of_lt_of_le this (le_of_eq _), rw [add_mul], congr' 1,
   { rw [pow_succ _ (n+1), ←mul_assoc, div_mul_cancel, mul_comm], norm_num },
   rw [pow_succ, ←pow_mul, mul_comm n 2, pow_mul, show (2 : ℝ) ^ 2 = 4, by norm_num, pow_succ,
@@ -52,7 +53,7 @@ theorem pi_lower_bound_start (n : ℕ) {a}
   (h : sqrt_two_add_series ((0:ℕ) / (1:ℕ)) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2) : a < pi :=
 begin
   refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series n), rw [mul_comm],
-  refine le_mul_of_div_le (pow_pos (by norm_num) _) (le_sqrt_of_sqr_le _),
+  refine (div_le_iff (pow_pos (by norm_num) _ : (0 : ℝ) < _)).mp (le_sqrt_of_sqr_le _),
   rwa [le_sub, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
 end
 

src/dynamics/circle/rotation_number/translation_number.lean

@@ -535,15 +535,15 @@ translation_number_translate z ▸ translation_number_mono
 
 lemma translation_number_le_of_le_add_int {x : ℝ} {m : ℤ} (h : f x ≤ x + m) : τ f ≤ m :=
 le_of_tendsto' (f.tendsto_translation_number' x) $ λ n,
-div_le_of_le_mul n.cast_add_one_pos $ sub_le_iff_le_add'.2 $
+(div_le_iff' (n.cast_add_one_pos : (0 : ℝ) < _)).mpr $ sub_le_iff_le_add'.2 $
 (coe_pow f (n + 1)).symm ▸ f.iterate_le_of_map_le_add_int h (n + 1)
 
 lemma translation_number_le_of_le_add_nat {x : ℝ} {m : ℕ} (h : f x ≤ x + m) : τ f ≤ m :=
 @translation_number_le_of_le_add_int f x m h
 
 lemma le_translation_number_of_add_int_le {x : ℝ} {m : ℤ} (h : x + m ≤ f x) : ↑m ≤ τ f :=
 ge_of_tendsto' (f.tendsto_translation_number' x) $ λ n,
-le_div_of_mul_le n.cast_add_one_pos $ le_sub_iff_add_le'.2 $
+(le_div_iff (n.cast_add_one_pos : (0 : ℝ) < _)).mpr $ le_sub_iff_add_le'.2 $
 by simp only [coe_pow, mul_comm (m:ℝ), ← nat.cast_add_one, f.le_iterate_of_add_int_le_map h]
 
 lemma le_translation_number_of_add_nat_le {x : ℝ} {m : ℕ} (h : x + m ≤ f x) : ↑m ≤ τ f :=

src/topology/metric_space/antilipschitz.lean

@@ -42,7 +42,7 @@ lemma antilipschitz_with.mul_le_dist [metric_space α] [metric_space β] {K : 
 begin
   by_cases hK : K = 0, by simp [hK, dist_nonneg],
   rw [nnreal.coe_inv, ← div_eq_inv_mul],
-  apply div_le_of_le_mul (nnreal.coe_pos.2 $ zero_lt_iff_ne_zero.2 hK),
+  rw div_le_iff' (nnreal.coe_pos.2 $ zero_lt_iff_ne_zero.2 hK),
   exact hf.le_mul_dist x y
 end