feat(algebra/order/monoid): zero_le_one' lemma with explicit type argument (#14594)

Author: vihdzp

src/algebra/geom_sum.lean

@@ -373,7 +373,7 @@ lemma nat.geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
   ∑ i in Ico 1 n, a/b^i ≤ a/(b - 1) :=
 begin
   cases n,
-  { rw [Ico_eq_empty_of_le (@zero_le_one ℕ _ _ _ _), sum_empty],
+  { rw [Ico_eq_empty_of_le (zero_le_one' ℕ), sum_empty],
     exact nat.zero_le _ },
   rw ←add_le_add_iff_left a,
   calc

src/algebra/order/monoid.lean

@@ -114,9 +114,13 @@ class linear_ordered_comm_monoid (α : Type*)
 class zero_le_one_class (α : Type*) [has_zero α] [has_one α] [has_le α] :=
 (zero_le_one : (0 : α) ≤ 1)
 
-@[simp] lemma zero_le_one [has_le α] [has_zero α] [has_one α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
+@[simp] lemma zero_le_one [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
 zero_le_one_class.zero_le_one
 
+/- `zero_le_one` with an explicit type argument. -/
+lemma zero_le_one' (α) [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] : (0 : α) ≤ 1 :=
+zero_le_one
+
 lemma zero_le_two [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
   [covariant_class α α (+) (≤)] : (0 : α) ≤ 2 :=
 add_nonneg zero_le_one zero_le_one

src/analysis/specific_limits/basic.lean

@@ -539,7 +539,7 @@ end
 
 lemma tendsto_nat_floor_div_at_top :
   tendsto (λ x, (⌊x⌋₊ : R) / x) at_top (𝓝 1) :=
-by simpa using tendsto_nat_floor_mul_div_at_top (@zero_le_one R _ _ _ _)
+by simpa using tendsto_nat_floor_mul_div_at_top (zero_le_one' R)
 
 lemma tendsto_nat_ceil_mul_div_at_top {a : R} (ha : 0 ≤ a) :
   tendsto (λ x, (⌈a * x⌉₊ : R) / x) at_top (𝓝 a) :=
@@ -558,6 +558,6 @@ end
 
 lemma tendsto_nat_ceil_div_at_top :
   tendsto (λ x, (⌈x⌉₊ : R) / x) at_top (𝓝 1) :=
-by simpa using tendsto_nat_ceil_mul_div_at_top (@zero_le_one R _ _ _ _)
+by simpa using tendsto_nat_ceil_mul_div_at_top (zero_le_one' R)
 
 end

src/data/int/basic.lean

@@ -221,7 +221,7 @@ le_sub_iff_add_le
   λ a0, (abs_eq_zero.mpr a0).le.trans_lt zero_lt_one⟩
 
 lemma abs_le_one_iff {a : ℤ} : |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1 :=
-by rw [le_iff_lt_or_eq, abs_lt_one_iff, abs_eq (@zero_le_one ℤ _ _ _ _)]
+by rw [le_iff_lt_or_eq, abs_lt_one_iff, abs_eq (zero_le_one' ℤ)]
 
 lemma one_le_abs {z : ℤ} (h₀: z ≠ 0) : 1 ≤ |z| :=
 add_one_le_iff.mpr (abs_pos.mpr h₀)
@@ -1624,7 +1624,7 @@ begin
 end
 
 lemma sq_eq_one_of_sq_lt_four {x : ℤ} (h1 : x ^ 2 < 4) (h2 : x ≠ 0) : x ^ 2 = 1 :=
-sq_eq_one_iff.mpr ((abs_eq (@zero_le_one ℤ _ _ _ _)).mp (le_antisymm (lt_add_one_iff.mp
+sq_eq_one_iff.mpr ((abs_eq (zero_le_one' ℤ)).mp (le_antisymm (lt_add_one_iff.mp
   (abs_lt_of_sq_lt_sq h1 zero_le_two)) (sub_one_lt_iff.mp (abs_pos.mpr h2))))
 
 lemma sq_eq_one_of_sq_le_three {x : ℤ} (h1 : x ^ 2 ≤ 3) (h2 : x ≠ 0) : x ^ 2 = 1 :=

src/topology/algebra/order/floor.lean

@@ -178,14 +178,14 @@ begin
       have : (uncurry f) (s, 0) = (uncurry f) (s, (1 : α)),
         by simp [uncurry, hf],
       rw this,
-      refine (h _ ⟨⟨⟩, by exact_mod_cast right_mem_Icc.2 (@zero_le_one α _ _ _ _)⟩).tendsto.comp _,
+      refine (h _ ⟨⟨⟩, by exact_mod_cast right_mem_Icc.2 (zero_le_one' α)⟩).tendsto.comp _,
       rw [nhds_within_prod_eq, nhds_within_univ],
       rw nhds_within_Icc_eq_nhds_within_Iic (@zero_lt_one α _ _),
       exact tendsto_id.prod_map
         (tendsto_nhds_within_mono_right Iio_subset_Iic_self $ tendsto_fract_left _) },
     { simp only [continuous_within_at, fract_coe, nhds_within_prod_eq,
                   nhds_within_univ, id.def, comp_app, prod.map_mk],
-      refine (h _ ⟨⟨⟩, by exact_mod_cast left_mem_Icc.2 (@zero_le_one α _ _ _ _)⟩).tendsto.comp _,
+      refine (h _ ⟨⟨⟩, by exact_mod_cast left_mem_Icc.2 (zero_le_one' α)⟩).tendsto.comp _,
       rw [nhds_within_prod_eq, nhds_within_univ,
         nhds_within_Icc_eq_nhds_within_Ici (@zero_lt_one α _ _)],
       exact tendsto_id.prod_map (tendsto_fract_right _) } },

src/topology/homotopy/basic.lean

@@ -141,24 +141,24 @@ lemma extend_apply_of_le_zero (F : homotopy f₀ f₁) {t : ℝ} (ht : t ≤ 0)
   F.extend t x = f₀ x :=
 begin
   rw [←F.apply_zero],
-  exact continuous_map.congr_fun (set.Icc_extend_of_le_left (@zero_le_one ℝ _ _ _ _) F.curry ht) x,
+  exact continuous_map.congr_fun (set.Icc_extend_of_le_left (zero_le_one' ℝ) F.curry ht) x,
 end
 
 lemma extend_apply_of_one_le (F : homotopy f₀ f₁) {t : ℝ} (ht : 1 ≤ t) (x : X) :
   F.extend t x = f₁ x :=
 begin
   rw [←F.apply_one],
-  exact continuous_map.congr_fun (set.Icc_extend_of_right_le (@zero_le_one ℝ _ _ _ _) F.curry ht) x,
+  exact continuous_map.congr_fun (set.Icc_extend_of_right_le (zero_le_one' ℝ) F.curry ht) x,
 end
 
 @[simp]
 lemma extend_apply_coe (F : homotopy f₀ f₁) (t : I) (x : X) : F.extend t x = F (t, x) :=
-continuous_map.congr_fun (set.Icc_extend_coe (@zero_le_one ℝ _ _ _ _) F.curry t) x
+continuous_map.congr_fun (set.Icc_extend_coe (zero_le_one' ℝ) F.curry t) x
 
 @[simp]
 lemma extend_apply_of_mem_I (F : homotopy f₀ f₁) {t : ℝ} (ht : t ∈ I) (x : X) :
   F.extend t x = F (⟨t, ht⟩, x) :=
-continuous_map.congr_fun (set.Icc_extend_of_mem (@zero_le_one ℝ _ _ _ _) F.curry ht) x
+continuous_map.congr_fun (set.Icc_extend_of_mem (zero_le_one' ℝ) F.curry ht) x
 
 lemma congr_fun {F G : homotopy f₀ f₁} (h : F = G) (x : I × X) : F x = G x :=
 continuous_map.congr_fun (congr_arg _ h) x

src/topology/path_connected.lean

@@ -555,9 +555,9 @@ begin
   have : range f = univ,
   { rw range_iff_surjective,
     intro t,
-    have h₁ : continuous (Icc_extend (@zero_le_one ℝ _ _ _ _) f),
+    have h₁ : continuous (Icc_extend (zero_le_one' ℝ) f),
     { continuity },
-    have := intermediate_value_Icc (@zero_le_one ℝ _ _ _ _) h₁.continuous_on,
+    have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuous_on,
     { rw [Icc_extend_left, Icc_extend_right] at this,
       change Icc (f 0) (f 1) ⊆ _ at this,
       rw [hf₀, hf₁] at this,