chore(topology/algebra): make the divisor argument of div_const exp…

…licit (#18411)

This is using the rule "parameters which do not appear in the types of other parameters should be explicit".
In particular, this means that it is easier to use proofs of the form `convert hf.div_const c`, without having to omit `c` and hope that Lean can guess it.

This makes the argument explicit for:

* `cont_diff_within_at.div_const`
* `cont_diff_at.div_const`
* `cont_diff_on.div_const`
* `cont_diff.div_const`
* `filter.tendsto.div_const`
* `continuous_at.div_const`
* `continuous_within_at.div_const`
* `continuous_on.div_const`
* `continuous.div_const`
* `differentiable_within_at.div_const`
* `differentiable_at.div_const`
* `differentiable_on.div_const`
* `differentiable.div_const`
* `deriv_within_div_const`


It was already explicit for:
* `filter.tendsto.div_const'`
* `has_sum.div_const`
* `summable.div_const`
* `integrable.div_const`
* `has_deriv_at.div_const`
* `has_deriv_within_at.div_const`
* `has_strict_deriv_at.div_const`
* `periodic.div_const`
* `measurable.div_const`
* `ae_measurable.div_const`
* The `mul` variants of many of the above

src/analysis/calculus/bump_function_findim.lean

@@ -217,7 +217,7 @@ begin
     from A.exists_smooth_support_eq,
   have B : ∀ x, f x ∈ Icc (0 : ℝ) 1 := λ x, f_range (mem_range_self x),
   refine ⟨λ x, (f x + f (-x)) / 2, _, _, _, _⟩,
-  { exact (f_smooth.add (f_smooth.comp cont_diff_neg)).div_const },
+  { exact (f_smooth.add (f_smooth.comp cont_diff_neg)).div_const _ },
   { assume x,
     split,
     { linarith [(B x).1, (B (-x)).1] },
@@ -513,7 +513,7 @@ begin
           dsimp only,
           linarith, },
         { apply cont_diff_on.smul _ cont_diff_on_snd,
-          refine (cont_diff_on_fst.add cont_diff_on_const).div_const.inv _,
+          refine ((cont_diff_on_fst.add cont_diff_on_const).div_const _).inv _,
           rintros ⟨R, x⟩ ⟨(hR : 1 < R), hx⟩,
           apply ne_of_gt,
           dsimp only,

src/analysis/calculus/bump_function_inner.lean

@@ -505,10 +505,10 @@ lemma nonneg_normed (x : E) : 0 ≤ f.normed μ x :=
 div_nonneg f.nonneg $ integral_nonneg f.nonneg'
 
 lemma cont_diff_normed {n : ℕ∞} : cont_diff ℝ n (f.normed μ) :=
-f.cont_diff.div_const
+f.cont_diff.div_const _
 
 lemma continuous_normed : continuous (f.normed μ) :=
-f.continuous.div_const
+f.continuous.div_const _
 
 lemma normed_sub (x : E) : f.normed μ (c - x) = f.normed μ (c + x) :=
 by simp_rw [f.normed_def, f.sub]

src/analysis/calculus/cont_diff.lean

@@ -2861,20 +2861,20 @@ lemma cont_diff_on.pow {f : E → 𝔸} (hf : cont_diff_on 𝕜 n f s) (m : ℕ)
   cont_diff_on 𝕜 n (λ y, f y ^ m) s :=
 λ y hy, (hf y hy).pow m
 
-lemma cont_diff_within_at.div_const {f : E → 𝕜'} {n} {c : 𝕜'}
-  (hf : cont_diff_within_at 𝕜 n f s x) :
+lemma cont_diff_within_at.div_const {f : E → 𝕜'} {n}
+  (hf : cont_diff_within_at 𝕜 n f s x) (c : 𝕜') :
   cont_diff_within_at 𝕜 n (λ x, f x / c) s x :=
 by simpa only [div_eq_mul_inv] using hf.mul cont_diff_within_at_const
 
-lemma cont_diff_at.div_const {f : E → 𝕜'} {n} {c : 𝕜'} (hf : cont_diff_at 𝕜 n f x) :
+lemma cont_diff_at.div_const {f : E → 𝕜'} {n} (hf : cont_diff_at 𝕜 n f x) (c : 𝕜') :
   cont_diff_at 𝕜 n (λ x, f x / c) x :=
-hf.div_const
+hf.div_const c
 
-lemma cont_diff_on.div_const {f : E → 𝕜'} {n} {c : 𝕜'} (hf : cont_diff_on 𝕜 n f s) :
+lemma cont_diff_on.div_const {f : E → 𝕜'} {n} (hf : cont_diff_on 𝕜 n f s) (c : 𝕜') :
   cont_diff_on 𝕜 n (λ x, f x / c) s :=
-λ x hx, (hf x hx).div_const
+λ x hx, (hf x hx).div_const c
 
-lemma cont_diff.div_const {f : E → 𝕜'} {n} {c : 𝕜'} (hf : cont_diff 𝕜 n f) :
+lemma cont_diff.div_const {f : E → 𝕜'} {n} (hf : cont_diff 𝕜 n f) (c : 𝕜') :
   cont_diff 𝕜 n (λ x, f x / c) :=
 by simpa only [div_eq_mul_inv] using hf.mul cont_diff_const
 

src/analysis/calculus/deriv.lean

@@ -1639,23 +1639,23 @@ lemma has_strict_deriv_at.div_const (hc : has_strict_deriv_at c c' x) (d : 𝕜'
   has_strict_deriv_at (λ x, c x / d) (c' / d) x :=
 by simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹
 
-lemma differentiable_within_at.div_const (hc : differentiable_within_at 𝕜 c s x) {d : 𝕜'} :
+lemma differentiable_within_at.div_const (hc : differentiable_within_at 𝕜 c s x) (d : 𝕜') :
   differentiable_within_at 𝕜 (λx, c x / d) s x :=
 (hc.has_deriv_within_at.div_const _).differentiable_within_at
 
-@[simp] lemma differentiable_at.div_const (hc : differentiable_at 𝕜 c x) {d : 𝕜'} :
+@[simp] lemma differentiable_at.div_const (hc : differentiable_at 𝕜 c x) (d : 𝕜') :
   differentiable_at 𝕜 (λ x, c x / d) x :=
 (hc.has_deriv_at.div_const _).differentiable_at
 
-lemma differentiable_on.div_const (hc : differentiable_on 𝕜 c s) {d : 𝕜'} :
+lemma differentiable_on.div_const (hc : differentiable_on 𝕜 c s) (d : 𝕜') :
   differentiable_on 𝕜 (λx, c x / d) s :=
-λ x hx, (hc x hx).div_const
+λ x hx, (hc x hx).div_const d
 
-@[simp] lemma differentiable.div_const (hc : differentiable 𝕜 c) {d : 𝕜'} :
+@[simp] lemma differentiable.div_const (hc : differentiable 𝕜 c) (d : 𝕜') :
   differentiable 𝕜 (λx, c x / d) :=
-λ x, (hc x).div_const
+λ x, (hc x).div_const d
 
-lemma deriv_within_div_const (hc : differentiable_within_at 𝕜 c s x) {d : 𝕜'}
+lemma deriv_within_div_const (hc : differentiable_within_at 𝕜 c s x) (d : 𝕜')
   (hxs : unique_diff_within_at 𝕜 s x) :
   deriv_within (λx, c x / d) s x = (deriv_within c s x) / d :=
 by simp [div_eq_inv_mul, deriv_within_const_mul, hc, hxs]

src/analysis/normed/field/basic.lean

@@ -483,7 +483,7 @@ begin
     ... ≤ ‖r - e‖ / ‖r‖ / ε :
       div_le_div_of_le_left (div_nonneg (norm_nonneg _) (norm_nonneg _)) ε0 he.le },
   refine squeeze_zero' (eventually_of_forall $ λ _, norm_nonneg _) this _,
-  refine (continuous_const.sub continuous_id).norm.div_const.div_const.tendsto' _ _ _,
+  refine (((continuous_const.sub continuous_id).norm.div_const _).div_const _).tendsto' _ _ _,
   simp,
 end
 

src/analysis/special_functions/integrals.lean

@@ -69,7 +69,7 @@ begin
       field_simp [(by linarith : r + 1 ≠ 0)], ring, },
     apply integrable_on_deriv_of_nonneg hc _ hderiv,
     { intros x hx, apply rpow_nonneg_of_nonneg hx.1.le, },
-    { refine (continuous_on_id.rpow_const _).div_const, intros x hx, right, linarith } },
+    { refine (continuous_on_id.rpow_const _).div_const _, intros x hx, right, linarith } },
   intro c, rcases le_total 0 c with hc|hc,
   { exact this c hc },
   { rw [interval_integrable.iff_comp_neg, neg_zero],
@@ -296,7 +296,7 @@ begin
     ring },
   intro c,
   apply integral_eq_sub_of_has_deriv_right,
-  { refine (complex.continuous_of_real_cpow_const _).div_const.continuous_on,
+  { refine ((complex.continuous_of_real_cpow_const _).div_const _).continuous_on,
     rwa [complex.add_re, complex.one_re, ←neg_lt_iff_pos_add] },
   { refine λ x hx, (has_deriv_at_of_real_cpow _ _).has_deriv_within_at,
     { rcases le_total c 0 with hc | hc,

src/analysis/special_functions/log/deriv.lean

@@ -248,7 +248,7 @@ begin
     suffices : tendsto (λ (t : ℕ), |x| ^ (t + 1) / (1 - |x|)) at_top
       (𝓝 (|x| * 0 / (1 - |x|))), by simpa,
     simp only [pow_succ],
-    refine (tendsto_const_nhds.mul _).div_const,
+    refine (tendsto_const_nhds.mul _).div_const _,
     exact tendsto_pow_at_top_nhds_0_of_lt_1 (abs_nonneg _) h },
   show summable (λ (n : ℕ), x ^ (n + 1) / (n + 1)),
   { refine summable_of_norm_bounded _ (summable_geometric_of_lt_1 (abs_nonneg _) h) (λ i, _),

src/analysis/special_functions/trigonometric/deriv.lean

@@ -44,7 +44,7 @@ lemma has_deriv_at_sin (x : ℂ) : has_deriv_at sin (cos x) x :=
 
 lemma cont_diff_sin {n} : cont_diff ℂ n sin :=
 (((cont_diff_neg.mul cont_diff_const).cexp.sub
-  (cont_diff_id.mul cont_diff_const).cexp).mul cont_diff_const).div_const
+  (cont_diff_id.mul cont_diff_const).cexp).mul cont_diff_const).div_const _
 
 lemma differentiable_sin : differentiable ℂ sin :=
 λx, (has_deriv_at_sin x).differentiable_at
@@ -72,7 +72,7 @@ lemma has_deriv_at_cos (x : ℂ) : has_deriv_at cos (-sin x) x :=
 
 lemma cont_diff_cos {n} : cont_diff ℂ n cos :=
 ((cont_diff_id.mul cont_diff_const).cexp.add
-  (cont_diff_neg.mul cont_diff_const).cexp).div_const
+  (cont_diff_neg.mul cont_diff_const).cexp).div_const _
 
 lemma differentiable_cos : differentiable ℂ cos :=
 λx, (has_deriv_at_cos x).differentiable_at
@@ -101,7 +101,7 @@ lemma has_deriv_at_sinh (x : ℂ) : has_deriv_at sinh (cosh x) x :=
 (has_strict_deriv_at_sinh x).has_deriv_at
 
 lemma cont_diff_sinh {n} : cont_diff ℂ n sinh :=
-(cont_diff_exp.sub cont_diff_neg.cexp).div_const
+(cont_diff_exp.sub cont_diff_neg.cexp).div_const _
 
 lemma differentiable_sinh : differentiable ℂ sinh :=
 λx, (has_deriv_at_sinh x).differentiable_at
@@ -127,7 +127,7 @@ lemma has_deriv_at_cosh (x : ℂ) : has_deriv_at cosh (sinh x) x :=
 (has_strict_deriv_at_cosh x).has_deriv_at
 
 lemma cont_diff_cosh {n} : cont_diff ℂ n cosh :=
-(cont_diff_exp.add cont_diff_neg.cexp).div_const
+(cont_diff_exp.add cont_diff_neg.cexp).div_const _
 
 lemma differentiable_cosh : differentiable ℂ cosh :=
 λx, (has_deriv_at_cosh x).differentiable_at

src/topology/algebra/group/basic.lean

@@ -832,8 +832,8 @@ lemma filter.tendsto.const_div' (b : G) {c : G} {f : α → G} {l : filter α}
 tendsto_const_nhds.div' h
 
 @[to_additive sub_const]
-lemma filter.tendsto.div_const' (b : G) {c : G} {f : α → G} {l : filter α}
-  (h : tendsto f l (𝓝 c)) : tendsto (λ k : α, f k / b) l (𝓝 (c / b)) :=
+lemma filter.tendsto.div_const' {c : G} {f : α → G} {l : filter α}
+  (h : tendsto f l (𝓝 c)) (b : G) : tendsto (λ k : α, f k / b) l (𝓝 (c / b)) :=
 h.div' tendsto_const_nhds
 
 variables [topological_space α] {f g : α → G} {s : set α} {x : α}

src/topology/algebra/group_with_zero.lean

@@ -48,24 +48,24 @@ section div_const
 variables [group_with_zero G₀] [topological_space G₀] [has_continuous_mul G₀]
   {f : α → G₀} {s : set α} {l : filter α}
 
-lemma filter.tendsto.div_const {x y : G₀} (hf : tendsto f l (𝓝 x)) :
+lemma filter.tendsto.div_const {x : G₀} (hf : tendsto f l (𝓝 x)) (y : G₀) :
   tendsto (λa, f a / y) l (𝓝 (x / y)) :=
 by simpa only [div_eq_mul_inv] using hf.mul tendsto_const_nhds
 
 variables [topological_space α]
 
-lemma continuous_at.div_const {a : α} (hf : continuous_at f a) {y : G₀} :
+lemma continuous_at.div_const {a : α} (hf : continuous_at f a) (y : G₀) :
   continuous_at (λ x, f x / y) a :=
 by simpa only [div_eq_mul_inv] using hf.mul continuous_at_const
 
-lemma continuous_within_at.div_const {a} (hf : continuous_within_at f s a) {y : G₀} :
+lemma continuous_within_at.div_const {a} (hf : continuous_within_at f s a) (y : G₀) :
   continuous_within_at (λ x, f x / y) s a :=
-hf.div_const
+hf.div_const _
 
-lemma continuous_on.div_const (hf : continuous_on f s) {y : G₀} : continuous_on (λ x, f x / y) s :=
+lemma continuous_on.div_const (hf : continuous_on f s) (y : G₀) : continuous_on (λ x, f x / y) s :=
 by simpa only [div_eq_mul_inv] using hf.mul continuous_on_const
 
-@[continuity] lemma continuous.div_const (hf : continuous f) {y : G₀} :
+@[continuity] lemma continuous.div_const (hf : continuous f) (y : G₀) :
   continuous (λ x, f x / y) :=
 by simpa only [div_eq_mul_inv] using hf.mul continuous_const