feat(order/basic): add simp attribute on le_refl, zero_le_one and zero_lt_one (#7733)

These ones show up so often that they would have deserved a simp attribute long ago.

Author: sgouezel

src/algebra/ordered_ring.lean

@@ -23,7 +23,7 @@ class ordered_semiring (α : Type u) extends semiring α, ordered_cancel_add_com
 section ordered_semiring
 variables [ordered_semiring α] {a b c d : α}
 
-lemma zero_le_one : 0 ≤ (1:α) :=
+@[simp] lemma zero_le_one : 0 ≤ (1:α) :=
 ordered_semiring.zero_le_one
 
 lemma zero_le_two : 0 ≤ (2:α) :=
@@ -37,7 +37,7 @@ section nontrivial
 
 variables [nontrivial α]
 
-lemma zero_lt_one : 0 < (1 : α) :=
+@[simp] lemma zero_lt_one : 0 < (1 : α) :=
 lt_of_le_of_ne zero_le_one zero_ne_one
 
 lemma zero_lt_two : 0 < (2:α) := add_pos zero_lt_one zero_lt_one

src/analysis/complex/isometry.lean

@@ -137,16 +137,14 @@ begin
       rw norm_sq_eq_abs,
       change 0 < ∥a∥ ^ 2,
       rw linear_isometry.norm_map,
-      simp,
-      simp [zero_lt_one] },
+      simp },
     have h : (∀ z, g z = z) ∨ (∀ z, g z = conj z) := linear_isometry_complex_aux g hg1,
     change (∀ z, a⁻¹ * f z = z) ∨ (∀ z, a⁻¹ * f z = conj z) at h,
     have ha : a ≠ 0 := by {
       rw ← norm_sq_pos,
       rw norm_sq_eq_abs,
       change 0 < ∥a∥ ^ 2,
       rw linear_isometry.norm_map,
-      simp,
-      simp [zero_lt_one] },
+      simp },
     simpa only [← inv_mul_eq_iff_eq_mul' ha] }
 end

src/data/complex/basic.lean

@@ -536,7 +536,7 @@ begin
   fsplit,
   { rintro ⟨⟨x, l, rfl⟩, h⟩,
     by_cases hx : x = 0,
-    { simp [hx] at h, exfalso, exact h (le_refl _), },
+    { simpa [hx] using h },
     { replace l : 0 < x := l.lt_of_ne (ne.symm hx),
       exact ⟨x, l, rfl⟩, } },
   { rintro ⟨x, l, rfl⟩,

src/data/real/golden_ratio.lean

@@ -155,7 +155,6 @@ begin
   simp only,
   rw [nat.fib_succ_succ, add_comm],
   simp [finset.sum_fin_eq_sum_range, finset.sum_range_succ'],
-  refl,
 end
 
 /-- The geometric sequence `λ n, φ^n` is a solution of `fib_rec`. -/

src/geometry/euclidean/basic.lean

@@ -499,7 +499,7 @@ by rw [dist_left_midpoint p1 p2, dist_right_midpoint p1 p2]
 /-- If M is the midpoint of the segment AB, then ∠AMB = π. -/
 lemma angle_midpoint_eq_pi (p1 p2 : P) (hp1p2 : p1 ≠ p2) : ∠ p1 (midpoint ℝ p1 p2) p2 = π :=
 have p2 -ᵥ midpoint ℝ p1 p2 = -(p1 -ᵥ midpoint ℝ p1 p2), by { rw neg_vsub_eq_vsub_rev, simp },
-by simp [angle, this, hp1p2]
+by simp [angle, this, hp1p2, -zero_lt_one]
 
 /-- If M is the midpoint of the segment AB and C is the same distance from A as it is from B
 then ∠CMA = π / 2. -/

src/order/basic.lean

@@ -56,6 +56,8 @@ open function
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w} {r : α → α → Prop}
 
+attribute [simp] le_refl
+
 @[simp] lemma lt_self_iff_false [preorder α] (a : α) : a < a ↔ false :=
 by simp [lt_irrefl a]
 

src/testing/slim_check/sampleable.lean

@@ -442,7 +442,7 @@ begin
 end
 
 lemma list.one_le_sizeof (xs : list α) : 1 ≤ sizeof xs :=
-by cases xs; unfold_wf; [refl, linarith]
+by cases xs; unfold_wf; linarith
 
 /--
 `list.shrink_removes` shrinks a list by removing chunks of size `k` in

src/topology/path_connected.lean

@@ -138,16 +138,16 @@ def extend : ℝ → X := Icc_extend zero_le_one γ
 lemma continuous_extend : continuous γ.extend :=
 γ.continuous.Icc_extend
 
-@[simp] lemma extend_zero : γ.extend 0 = x :=
-(Icc_extend_left _ _).trans γ.source
-
-@[simp] lemma extend_one : γ.extend 1 = y :=
-(Icc_extend_right _ _).trans γ.target
-
 @[simp] lemma extend_extends {X : Type*} [topological_space X] {a b : X}
   (γ : path a b) {t : ℝ} (ht : t ∈ (Icc 0 1 : set ℝ)) : γ.extend t = γ ⟨t, ht⟩ :=
 Icc_extend_of_mem _ γ ht
 
+lemma extend_zero : γ.extend 0 = x :=
+by simp
+
+lemma extend_one : γ.extend 1 = y :=
+by simp
+
 @[simp] lemma extend_extends' {X : Type*} [topological_space X] {a b : X}
   (γ : path a b) (t : (Icc 0 1 : set ℝ)) : γ.extend t = γ t :=
 Icc_extend_coe _ γ t

src/topology/unit_interval.lean

@@ -39,10 +39,14 @@ instance has_zero : has_zero I := ⟨⟨0, by split ; norm_num⟩⟩
 
 @[simp, norm_cast] lemma coe_zero : ((0 : I) : ℝ) = 0 := rfl
 
+@[simp] lemma mk_zero (h : (0 : ℝ) ∈ Icc (0 : ℝ) 1) : (⟨0, h⟩ : I) = 0 := rfl
+
 instance has_one : has_one I := ⟨⟨1, by split ; norm_num⟩⟩
 
 @[simp, norm_cast] lemma coe_one : ((1 : I) : ℝ) = 1 := rfl
 
+@[simp] lemma mk_one (h : (1 : ℝ) ∈ Icc (0 : ℝ) 1) : (⟨1, h⟩ : I) = 1 := rfl
+
 instance : nonempty I := ⟨0⟩
 
 /-- Unit interval central symmetry. -/

test/nontriviality.lean

@@ -36,10 +36,10 @@ begin
   exact zero_le_one,
 end
 
-example {R : Type} [ordered_ring R] : 0 ≤ (1 : R) :=
+example {R : Type} [ordered_ring R] : 0 ≤ (2 : R) :=
 begin
   success_if_fail { nontriviality punit },
-  exact zero_le_one,
+  exact zero_le_two,
 end
 
 example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 2 ∣ 4 :=