chore(*): use le_rfl instead of le_refl _ (#11797)

src/algebra/algebra/operations.lean

@@ -255,7 +255,7 @@ begin
   induction n with n ih,
   { erw [pow_zero, pow_zero, set.singleton_subset_iff],
     rw [set_like.mem_coe, ← one_le],
-    exact le_refl _ },
+    exact le_rfl },
   { rw [pow_succ, pow_succ],
     refine set.subset.trans (set.mul_subset_mul (subset.refl _) ih) _,
     apply mul_subset_mul }

src/algebra/algebra/subalgebra.lean

@@ -544,7 +544,7 @@ protected lemma gc : galois_connection (adjoin R : set A → subalgebra R A) coe
 protected def gi : galois_insertion (adjoin R : set A → subalgebra R A) coe :=
 { choice := λ s hs, (adjoin R s).copy s $ le_antisymm (algebra.gc.le_u_l s) hs,
   gc := algebra.gc,
-  le_l_u := λ S, (algebra.gc (S : set A) (adjoin R S)).1 $ le_refl _,
+  le_l_u := λ S, (algebra.gc (S : set A) (adjoin R S)).1 $ le_rfl,
   choice_eq := λ _ _, subalgebra.copy_eq _ _ _ }
 
 instance : complete_lattice (subalgebra R A) :=

src/algebra/big_operators/order.lean

@@ -619,7 +619,7 @@ begin
   refine finset.induction_on s _ (λ i s hi ih, _),
   { simp },
   { simp only [finset.sum_insert hi],
-  exact (abv.add_le _ _).trans (add_le_add (le_refl _) ih) },
+  exact (abv.add_le _ _).trans (add_le_add le_rfl ih) },
 end
 
 lemma is_absolute_value.abv_sum [semiring R] [ordered_semiring S] (abv : R → S)

src/algebra/direct_limit.lean

@@ -198,7 +198,7 @@ theorem of.zero_exact [is_directed ι (≤)] {i x} (H : of R ι G f i x = 0) :
   ∃ j hij, f i j hij x = (0 : G j) :=
 by haveI : nonempty ι := ⟨i⟩; exact
 let ⟨j, hj, hxj⟩ := of.zero_exact_aux H in
-if hx0 : x = 0 then ⟨i, le_refl _, by simp [hx0]⟩
+if hx0 : x = 0 then ⟨i, le_rfl, by simp [hx0]⟩
 else
   have hij : i ≤ j, from hj _ $
     by simp [direct_sum.apply_eq_component, hx0],

src/algebra/indicator_function.lean

@@ -460,7 +460,7 @@ mul_indicator_apply_le_one (h a)
 
 @[to_additive] lemma mul_indicator_le_mul_indicator (h : f a ≤ g a) :
   mul_indicator s f a ≤ mul_indicator s g a :=
-mul_indicator_rel_mul_indicator (le_refl _) (λ _, h)
+mul_indicator_rel_mul_indicator le_rfl (λ _, h)
 
 attribute [mono] mul_indicator_le_mul_indicator indicator_le_indicator
 
@@ -471,7 +471,7 @@ mul_indicator_apply_le' (λ ha, le_mul_indicator_apply (λ _, le_rfl) (λ hat, (
   (λ ha, one_le_mul_indicator_apply (λ _, hf _))
 
 @[to_additive] lemma mul_indicator_le_self' (hf : ∀ x ∉ s, 1 ≤ f x) : mul_indicator s f ≤ f :=
-mul_indicator_le' (λ _ _, le_refl _) hf
+mul_indicator_le' (λ _ _, le_rfl) hf
 
 @[to_additive] lemma mul_indicator_Union_apply {ι M} [complete_lattice M] [has_one M]
   (h1 : (⊥:M) = 1) (s : ι → set α) (f : α → M) (x : α) :

src/algebra/lie/nilpotent.lean

@@ -114,11 +114,11 @@ begin
   intros l k,
   induction k with k ih generalizing l;
   intros h,
-  { exact (le_zero_iff.mp h).symm ▸ le_refl _, },
+  { exact (le_zero_iff.mp h).symm ▸ le_rfl, },
   { rcases nat.of_le_succ h with hk | hk,
     { rw lower_central_series_succ,
       exact (lie_submodule.mono_lie_right _ _ ⊤ (ih hk)).trans (lie_submodule.lie_le_right _ _), },
-    { exact hk.symm ▸ le_refl _, }, },
+    { exact hk.symm ▸ le_rfl, }, },
 end
 
 lemma trivial_iff_lower_central_eq_bot : is_trivial L M ↔ lower_central_series R L M 1 = ⊥ :=
@@ -160,7 +160,7 @@ lemma derived_series_le_lower_central_series (k : ℕ) :
 begin
   induction k with k h,
   { rw [derived_series_def, derived_series_of_ideal_zero, lower_central_series_zero],
-    exact le_refl _, },
+    exact le_rfl, },
   { have h' : derived_series R L k ≤ ⊤, { by simp only [le_top], },
     rw [derived_series_def, derived_series_of_ideal_succ, lower_central_series_succ],
     exact lie_submodule.mono_lie _ _ _ _ h' h, },

src/algebra/lie/submodule.lean

@@ -604,11 +604,11 @@ variables {f}
 (gc_map_comap f).l_sup
 
 lemma map_comap_le : map f (comap f J) ≤ J :=
-by { rw map_le_iff_le_comap, apply le_refl _, }
+by { rw map_le_iff_le_comap, exact le_rfl, }
 
 /-- See also `lie_ideal.map_comap_eq`. -/
 lemma comap_map_le : I ≤ comap f (map f I) :=
-by { rw ← map_le_iff_le_comap, apply le_refl _, }
+by { rw ← map_le_iff_le_comap, exact le_rfl, }
 
 @[mono] lemma map_mono : monotone (map f) :=
 λ I₁ I₂ h,

src/algebra/order/archimedean.lean

@@ -300,7 +300,7 @@ begin
   refine ⟨(lt_div_iff n0').2 $
     (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩,
   rw [int.cast_add, int.cast_one],
-  refine lt_of_le_of_lt (add_le_add_right ((zh _).1 (le_refl _)) _) _,
+  refine lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) _,
   rwa [← lt_sub_iff_add_lt', ← sub_mul,
        ← div_lt_iff' (sub_pos.2 h), one_div],
   { rw [rat.coe_int_denom, nat.cast_one], exact one_ne_zero },

src/algebra/order/monoid.lean

@@ -280,7 +280,7 @@ begin
   { intros a b h c ca h₂,
     cases b with b,
     { rw le_antisymm h bot_le at h₂,
-      exact ⟨_, h₂, le_refl _⟩ },
+      exact ⟨_, h₂, le_rfl⟩ },
     cases a with a,
     { change c + 0 = some ca at h₂,
       simp at h₂, simp [h₂],

src/algebra/order/pi.lean

@@ -41,7 +41,7 @@ instance {ι : Type*} {Z : ι → Type*} [∀ i, canonically_ordered_monoid (Z i
       { ext i,
         exact (le_iff_exists_mul.mp (w i)).some_spec, }, },
     { rintro ⟨h, rfl⟩,
-      exact λ i, le_mul_right (le_refl _), },
+      exact λ i, le_mul_right le_rfl, },
   end,
   ..pi.order_bot,
   ..pi.ordered_comm_monoid, }

src/algebra/order/ring.lean

@@ -306,7 +306,7 @@ by classical; exact decidable.le_mul_of_one_le_left
 protected lemma decidable.lt_mul_of_one_lt_right [@decidable_rel α (≤)]
   (hb : 0 < b) (h : 1 < a) : b < b * a :=
 suffices b * 1 < b * a, by rwa mul_one at this,
-decidable.mul_lt_mul' (le_refl _) h zero_le_one hb
+decidable.mul_lt_mul' le_rfl h zero_le_one hb
 
 lemma lt_mul_of_one_lt_right : 0 < b → 1 < a → b < b * a :=
 by classical; exact decidable.lt_mul_of_one_lt_right
@@ -315,7 +315,7 @@ by classical; exact decidable.lt_mul_of_one_lt_right
 protected lemma decidable.lt_mul_of_one_lt_left [@decidable_rel α (≤)]
   (hb : 0 < b) (h : 1 < a) : b < a * b :=
 suffices 1 * b < a * b, by rwa one_mul at this,
-decidable.mul_lt_mul h (le_refl _) hb (zero_le_one.trans h.le)
+decidable.mul_lt_mul h le_rfl hb (zero_le_one.trans h.le)
 
 lemma lt_mul_of_one_lt_left : 0 < b → 1 < a → b < a * b :=
 by classical; exact decidable.lt_mul_of_one_lt_left

src/algebra/order/with_zero.lean

@@ -185,7 +185,7 @@ by simpa only [mul_zero, mul_one] using mul_le_mul_left' (@zero_le_one' α _) a
 not_lt_of_le zero_le'
 
 @[simp] lemma le_zero_iff : a ≤ 0 ↔ a = 0 :=
-⟨λ h, le_antisymm h zero_le', λ h, h ▸ le_refl _⟩
+⟨λ h, le_antisymm h zero_le', λ h, h ▸ le_rfl⟩
 
 lemma zero_lt_iff : 0 < a ↔ a ≠ 0 :=
 ⟨ne_of_gt, λ h, lt_of_le_of_ne zero_le' h.symm⟩

src/algebra/tropical/basic.lean

@@ -133,7 +133,7 @@ instance decidable_lt [has_lt R] [decidable_rel ((<) : R → R → Prop)] :
 λ x y, ‹decidable_rel (<)› (untrop x) (untrop y)
 
 instance [preorder R] : preorder (tropical R) :=
-{ le_refl := λ _, le_refl _,
+{ le_refl := λ _, le_rfl,
   le_trans := λ _ _ _ h h', le_trans h h',
   lt_iff_le_not_le := λ _ _, lt_iff_le_not_le,
   ..tropical.has_le,

src/algebraic_topology/simplex_category.lean

@@ -443,15 +443,15 @@ begin
       intros a b h,
       dsimp only [],
       split_ifs with h1 h2 h3,
-      any_goals { exact le_refl _ },
+      any_goals { exact le_rfl },
       { exact bot_le },
       { exact false.elim (h1 (le_trans h h3)) }
     end ⟩,
     set chi_2 : m ⟶ [1] := hom.mk ⟨λ u, if u < x then 0 else 1, begin
       intros a b h,
       dsimp only [],
       split_ifs with h1 h2 h3,
-      any_goals { exact le_refl _ },
+      any_goals { exact le_rfl },
       { exact bot_le },
       { exact false.elim (h1 (lt_of_le_of_lt h h3)) }
     end ⟩,

src/analysis/analytic/basic.lean

@@ -661,7 +661,7 @@ This is not totally obvious as we need to check the convergence of the series. -
 protected lemma formal_multilinear_series.has_fpower_series_on_ball [complete_space F]
   (p : formal_multilinear_series 𝕜 E F) (h : 0 < p.radius) :
   has_fpower_series_on_ball p.sum p 0 p.radius :=
-{ r_le    := le_refl _,
+{ r_le    := le_rfl,
   r_pos   := h,
   has_sum := λ y hy, by { rw zero_add, exact p.has_sum hy } }
 
@@ -951,7 +951,7 @@ theorem has_fpower_series_on_ball.change_origin
   has_fpower_series_on_ball f (p.change_origin y) (x + y) (r - ∥y∥₊) :=
 { r_le := begin
     apply le_trans _ p.change_origin_radius,
-    exact tsub_le_tsub hf.r_le (le_refl _)
+    exact tsub_le_tsub hf.r_le le_rfl
   end,
   r_pos := by simp [h],
   has_sum := λ z hz, begin

src/analysis/asymptotics/asymptotics.lean

@@ -358,7 +358,7 @@ theorem is_O_of_le (hfg : ∀ x, ∥f x∥ ≤ ∥g x∥) : is_O f g l :=
 end
 
 theorem is_O_with_refl (f : α → E) (l : filter α) : is_O_with 1 f f l :=
-is_O_with_of_le l $ λ _, le_refl _
+is_O_with_of_le l $ λ _, le_rfl
 
 theorem is_O_refl (f : α → E) (l : filter α) : is_O f f l := (is_O_with_refl f l).is_O
 

src/analysis/calculus/deriv.lean

@@ -1006,7 +1006,7 @@ theorem has_deriv_within_at.continuous_within_at
 has_deriv_at_filter.tendsto_nhds inf_le_left h
 
 theorem has_deriv_at.continuous_at (h : has_deriv_at f f' x) : continuous_at f x :=
-has_deriv_at_filter.tendsto_nhds (le_refl _) h
+has_deriv_at_filter.tendsto_nhds le_rfl h
 
 protected theorem has_deriv_at.continuous_on {f f' : 𝕜 → F}
   (hderiv : ∀ x ∈ s, has_deriv_at f (f' x) x) : continuous_on f s :=

src/analysis/calculus/fderiv.lean

@@ -625,7 +625,7 @@ has_fderiv_at_filter.tendsto_nhds inf_le_left h
 
 theorem has_fderiv_at.continuous_at (h : has_fderiv_at f f' x) :
   continuous_at f x :=
-has_fderiv_at_filter.tendsto_nhds (le_refl _) h
+has_fderiv_at_filter.tendsto_nhds le_rfl h
 
 lemma differentiable_within_at.continuous_within_at (h : differentiable_within_at 𝕜 f s x) :
   continuous_within_at f s x :=
@@ -1023,7 +1023,7 @@ example {g : F → G} {g' : F →L[𝕜] G}
 begin
   unfold has_fderiv_at_filter at hg,
   have : is_o (λ x', g (f x') - g (f x) - g' (f x' - f x)) (λ x', f x' - f x) L,
-    from hg.comp_tendsto (le_refl _),
+    from hg.comp_tendsto le_rfl,
   have eq₁ : is_o (λ x', g (f x') - g (f x) - g' (f x' - f x)) (λ x', x' - x) L,
     from this.trans_is_O hf.is_O_sub,
   have eq₂ : is_o (λ x', f x' - f x - f' (x' - x)) (λ x', x' - x) L,

src/analysis/calculus/fderiv_measurable.lean

@@ -149,7 +149,7 @@ begin
   simp only [has_fderiv_at, has_fderiv_at_filter, is_o_iff] at this,
   rcases eventually_nhds_iff_ball.1 (this (half_pos hε)) with ⟨R, R_pos, hR⟩,
   refine ⟨R, R_pos, λ r hr, _⟩,
-  have : r ∈ Ioc (r/2) r := ⟨half_lt_self hr.1, le_refl _⟩,
+  have : r ∈ Ioc (r/2) r := ⟨half_lt_self hr.1, le_rfl⟩,
   refine ⟨r, this, λ y hy z hz, _⟩,
   calc  ∥f z - f y - (fderiv 𝕜 f x) (z - y)∥
       = ∥(f z - f x - (fderiv 𝕜 f x) (z - x)) - (f y - f x - (fderiv 𝕜 f x) (y - x))∥ :
@@ -278,18 +278,18 @@ begin
     refine ⟨e, λ e' he', _⟩,
     rw [dist_comm, dist_eq_norm],
     calc ∥L0 e - L0 e'∥
-          ≤ 12 * ∥c∥ * (1/2)^e : M _ _ _ _ _ _ (le_refl _) (le_refl _) (le_refl _) (le_refl _) he'
+          ≤ 12 * ∥c∥ * (1/2)^e : M _ _ _ _ _ _ le_rfl le_rfl le_rfl le_rfl he'
       ... < 12 * ∥c∥ * (ε / (12 * ∥c∥)) :
-        mul_lt_mul' (le_refl _) he (le_of_lt P) (mul_pos (by norm_num) cpos)
+        mul_lt_mul' le_rfl he (le_of_lt P) (mul_pos (by norm_num) cpos)
       ... = ε : by { field_simp [(by norm_num : (12 : ℝ) ≠ 0), ne_of_gt cpos], ring } },
   /- As it is Cauchy, the sequence `L0` converges, to a limit `f'` in `K`.-/
   obtain ⟨f', f'K, hf'⟩ : ∃ f' ∈ K, tendsto L0 at_top (𝓝 f') :=
-    cauchy_seq_tendsto_of_is_complete hK (λ e, (hn e (n e) (n e) (le_refl _) (le_refl _)).1) this,
+    cauchy_seq_tendsto_of_is_complete hK (λ e, (hn e (n e) (n e) le_rfl le_rfl).1) this,
   have Lf' : ∀ e p, n e ≤ p → ∥L e (n e) p - f'∥ ≤ 12 * ∥c∥ * (1/2)^e,
   { assume e p hp,
     apply le_of_tendsto (tendsto_const_nhds.sub hf').norm,
     rw eventually_at_top,
-    exact ⟨e, λ e' he', M _ _ _ _ _ _ (le_refl _) hp (le_refl _) (le_refl _) he'⟩ },
+    exact ⟨e, λ e' he', M _ _ _ _ _ _ le_rfl hp le_rfl le_rfl he'⟩ },
   /- Let us show that `f` has derivative `f'` at `x`. -/
   have : has_fderiv_at f f' x,
   { simp only [has_fderiv_at_iff_is_o_nhds_zero, is_o_iff],
@@ -327,7 +327,7 @@ begin
     -- `f` is well approximated by `L e (n e) k` at the relevant scale
     -- (in fact, we use `m = k - 1` instead of `k` because of the precise definition of `A`).
     have J1 : ∥f (x + y) - f x - L e (n e) m ((x + y) - x)∥ ≤ (1/2) ^ e * (1/2) ^ m,
-    { apply le_of_mem_A (hn e (n e) m (le_refl _) m_ge).2.2,
+    { apply le_of_mem_A (hn e (n e) m le_rfl m_ge).2.2,
       { simp only [mem_closed_ball, dist_self],
         exact div_nonneg (le_of_lt P) (zero_le_two) },
       { simpa only [dist_eq_norm, add_sub_cancel', mem_closed_ball, pow_succ', mul_one_div]

src/analysis/calculus/fderiv_symmetric.lean

@@ -136,7 +136,7 @@ begin
         by simp only [norm_smul, real.norm_eq_abs, hpos.le, abs_of_nonneg, abs_mul, ht.left,
                       mul_assoc]
       ... ≤ h * ∥v∥ + 1 * (h * ∥w∥) :
-        add_le_add (le_refl _) (mul_le_mul_of_nonneg_right ht.2.le
+        add_le_add le_rfl (mul_le_mul_of_nonneg_right ht.2.le
           (mul_nonneg hpos.le (norm_nonneg _)))
       ... = h * (∥v∥ + ∥w∥) : by ring,
     calc ∥g' t∥ = ∥(f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (h • w)∥ :
@@ -163,7 +163,7 @@ begin
       apply mul_le_mul_of_nonneg_right _ (norm_nonneg _),
       apply mul_le_mul_of_nonneg_left _ (εpos.le),
       apply (norm_add_le _ _).trans,
-      refine add_le_add (le_refl _) _,
+      refine add_le_add le_rfl _,
       simp only [norm_smul, real.norm_eq_abs, abs_mul, abs_of_nonneg, ht.1, hpos.le, mul_assoc],
       exact mul_le_of_le_one_left (mul_nonneg hpos.le (norm_nonneg _)) ht.2.le,
     end

src/analysis/calculus/inverse.lean

@@ -272,7 +272,7 @@ begin
       f'symm.nnnorm * (1 - (c * f'symm.nnnorm)^n.succ) / (1 - c * f'symm.nnnorm) * dist (f b) y :=
     calc
       dist (g (u n)) b ≤ dist (g (u n)) (u n) + dist (u n) b : dist_triangle _ _ _
-      ... ≤ f'symm.nnnorm * dist (f (u n)) y + dist (u n) b : add_le_add (A _) (le_refl _)
+      ... ≤ f'symm.nnnorm * dist (f (u n)) y + dist (u n) b : add_le_add (A _) le_rfl
       ... ≤ f'symm.nnnorm * ((c * f'symm.nnnorm)^n * dist (f b) y) +
         f'symm.nnnorm * (1 - (c * f'symm.nnnorm)^n) / (1 - c * f'symm.nnnorm) * dist (f b) y :
           add_le_add (mul_le_mul_of_nonneg_left IH.1 (nnreal.coe_nonneg _)) IH.2

src/analysis/calculus/times_cont_diff.lean

@@ -251,7 +251,7 @@ begin
     { assume m hm,
       apply (H m.succ).fderiv_within m (with_top.coe_lt_coe.2 (lt_add_one m)) },
     { assume m hm,
-      apply (H m).cont m (le_refl _) } }
+      apply (H m).cont m le_rfl } }
 end
 
 /-- If a function has a Taylor series at order at least `1`, then the term of order `1` of this
@@ -315,7 +315,7 @@ begin
   { assume h,
     exact ⟨h.of_le (with_top.coe_le_coe.2 (nat.le_succ n)),
            h.fderiv_within _ (with_top.coe_lt_coe.2 (lt_add_one n)),
-           h.cont (n + 1) (le_refl _)⟩ },
+           h.cont (n + 1) le_rfl⟩ },
   { assume h,
     split,
     { exact h.1.zero_eq },
@@ -420,7 +420,7 @@ lemma times_cont_diff_within_at_nat {n : ℕ} :
   times_cont_diff_within_at 𝕜 n f s x ↔
   ∃ u ∈ 𝓝[insert x s] x, ∃ p : E → formal_multilinear_series 𝕜 E F,
   has_ftaylor_series_up_to_on n f p u :=
-⟨λ H, H n (le_refl _), λ ⟨u, hu, p, hp⟩ m hm, ⟨u, hu, p, hp.of_le hm⟩⟩
+⟨λ H, H n le_rfl, λ ⟨u, hu, p, hp⟩ m hm, ⟨u, hu, p, hp.of_le hm⟩⟩
 
 lemma times_cont_diff_within_at.of_le {m n : with_top ℕ}
   (h : times_cont_diff_within_at 𝕜 n f s x) (hmn : m ≤ n) :
@@ -511,7 +511,7 @@ begin
   rcases h 1 hn with ⟨u, hu, p, H⟩,
   rcases mem_nhds_within.1 hu with ⟨t, t_open, xt, tu⟩,
   rw inter_comm at tu,
-  have := ((H.mono tu).differentiable_on (le_refl _)) x ⟨mem_insert x s, xt⟩,
+  have := ((H.mono tu).differentiable_on le_rfl) x ⟨mem_insert x s, xt⟩,
   exact (differentiable_within_at_inter (is_open.mem_nhds t_open xt)).1 this,
 end
 
@@ -528,7 +528,7 @@ theorem times_cont_diff_within_at_succ_iff_has_fderiv_within_at {n : ℕ} :
 begin
   split,
   { assume h,
-    rcases h n.succ (le_refl _) with ⟨u, hu, p, Hp⟩,
+    rcases h n.succ le_rfl with ⟨u, hu, p, Hp⟩,
     refine ⟨u, hu, λ y, (continuous_multilinear_curry_fin1 𝕜 E F) (p y 1),
       λ y hy, Hp.has_fderiv_within_at (with_top.coe_le_coe.2 (nat.le_add_left 1 n)) hy, _⟩,
     assume m hm,
@@ -540,7 +540,7 @@ begin
       exact Hp.2.2.of_le hm } },
   { rintros ⟨u, hu, f', f'_eq_deriv, Hf'⟩,
     rw times_cont_diff_within_at_nat,
-    rcases Hf' n (le_refl _) with ⟨v, hv, p', Hp'⟩,
+    rcases Hf' n le_rfl with ⟨v, hv, p', Hp'⟩,
     refine ⟨v ∩ u, _, λ x, (p' x).unshift (f x), _⟩,
     { apply filter.inter_mem _ hu,
       apply nhds_within_le_of_mem hu,
@@ -679,7 +679,7 @@ theorem times_cont_diff_on_succ_iff_has_fderiv_within_at {n : ℕ} :
 begin
   split,
   { assume h x hx,
-    rcases (h x hx) n.succ (le_refl _) with ⟨u, hu, p, Hp⟩,
+    rcases (h x hx) n.succ le_rfl with ⟨u, hu, p, Hp⟩,
     refine ⟨u, hu, λ y, (continuous_multilinear_curry_fin1 𝕜 E F) (p y 1),
       λ y hy, Hp.has_fderiv_within_at (with_top.coe_le_coe.2 (nat.le_add_left 1 n)) hy, _⟩,
     rw has_ftaylor_series_up_to_on_succ_iff_right at Hp,
@@ -903,7 +903,7 @@ begin
     have : p x m.succ = ftaylor_series_within 𝕜 f s x m.succ,
     { change p x m.succ = iterated_fderiv_within 𝕜 m.succ f s x,
       rw ← iterated_fderiv_within_inter (is_open.mem_nhds o_open xo) hs hx,
-      exact (Hp.mono ho).eq_ftaylor_series_of_unique_diff_on (le_refl _)
+      exact (Hp.mono ho).eq_ftaylor_series_of_unique_diff_on le_rfl
         (hs.inter o_open) ⟨hx, xo⟩ },
     rw [← this, ← has_fderiv_within_at_inter (is_open.mem_nhds o_open xo)],
     have A : ∀ y ∈ s ∩ o, p y m = ftaylor_series_within 𝕜 f s y m,
@@ -926,9 +926,9 @@ begin
     { rintros y ⟨hy, yo⟩,
       change p y m = iterated_fderiv_within 𝕜 m f s y,
       rw ← iterated_fderiv_within_inter (is_open.mem_nhds o_open yo) hs hy,
-      exact (Hp.mono ho).eq_ftaylor_series_of_unique_diff_on (le_refl _)
+      exact (Hp.mono ho).eq_ftaylor_series_of_unique_diff_on le_rfl
         (hs.inter o_open) ⟨hy, yo⟩ },
-    exact ((Hp.mono ho).cont m (le_refl _)).congr (λ y hy, (A y hy).symm) }
+    exact ((Hp.mono ho).cont m le_rfl).congr (λ y hy, (A y hy).symm) }
 end
 
 lemma times_cont_diff_on_of_continuous_on_differentiable_on {n : with_top ℕ}
@@ -2105,7 +2105,7 @@ begin
     rw image_insert_eq,
     exact insert_subset_insert (image_subset_iff.mpr st) },
   have Z := ((hu.comp (hv.mono (inter_subset_right (f ⁻¹' u) v)) (inter_subset_left _ _))
-    .times_cont_diff_within_at) xmem m (le_refl _),
+    .times_cont_diff_within_at) xmem m le_rfl,
   have : 𝓝[f ⁻¹' u ∩ v] x = 𝓝[insert x s] x,
   { have A : f ⁻¹' u ∩ v = (insert x s) ∩ (f ⁻¹' u ∩ v),
     { apply subset.antisymm _ (inter_subset_right _ _),

src/analysis/inner_product_space/projection.lean

@@ -78,7 +78,7 @@ begin
   -- maybe this should be a separate lemma
   have exists_seq : ∃ w : ℕ → K, ∀ n, ∥u - w n∥ < δ + 1 / (n + 1),
   { have hδ : ∀n:ℕ, δ < δ + 1 / (n + 1), from
-      λ n, lt_add_of_le_of_pos (le_refl _) nat.one_div_pos_of_nat,
+      λ n, lt_add_of_le_of_pos le_rfl nat.one_div_pos_of_nat,
     have h := λ n, exists_lt_of_cinfi_lt (hδ n),
     let w : ℕ → K := λ n, classical.some (h n),
     exact ⟨w, λ n, classical.some_spec (h n)⟩ },