mathlib

efdc8504 - feat(tactic/conv/apply_congr): using congruence lemmas inside conv (#2221)

feat(tactic/conv/apply_congr): using congruence lemmas inside conv (#2221) * Update interactive.lean Added Keeley Hoeks Zoom tactic. * Add files via upload Added operand.lean file to the tactic folder. * Add files via upload Added the test files for zoom and operand. * Rename operand_test.lean to operand.lean * Update and rename zoom_test.lean to zoom.lean Fixed the imports * Update operand.lean * Update tactics.md * Update operand.lean Fixed the lamda problem. * Update operand.lean Added tests without lamdas * Update operand.lean Added header * Update operand.lean Added header * Update operand.lean deleted zoom * Update zoom.lean Added comment to self * Update operand.lean Added doc_string to operand * Update interactive.lean Added doc_string to zoom * Update tactics.md Fixed colon and brackets in operand doc * Update operand.lean Fixed colon placements and brackets * merge * feat(tactic/converter/apply_congr): apply congruence lemmas in conv * last example * fix docs * Apply suggestions from code review Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * remove docs from tactics.md * merge doc comment fragments * import in tactic.basic * docs * add to conv doc tactic Co-authored-by: u6338192 <51683915+u6338192@users.noreply.github.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>