mathlib3

32c082f5 - fix(tactic/library_search): group monotone lemmas with le lemmas (#3471)

fix(tactic/library_search): group monotone lemmas with le lemmas (#3471) This lets `library_search` use `monotone` lemmas to prove `\le` goals, and vice versa, resolving a problem people were experiencing in Patrick's exercises at LftCM2020: ``` import order.filter.basic open filter example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ} (hf : tendsto f A B) (hg : tendsto g B C) : tendsto (g ∘ f) A C := calc map (g ∘ f) A = map g (map f A) : by library_search ... ≤ map g B : by library_search! ... ≤ C : by library_search! ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com>