Human oriented tools for theorem proving in Lean

I will present some tactics and tools that I made for Mathlib. I will explain how they work and show them in action with a live demonstration. The main ones are

- A library search tool for finding theorems based on an expression in the tactic state

- The generalized rewriting tactic for rewriting with relations other than equalitys.