Rishikesh Vaishnav: Lean4Less: A Term-Patching Framework for Eliminating Defitional Equalities in Lean External Video-URL https://www.youtube.com/watch?v=9G8DVGo9aXk Preview-Image Search Engine Exclude no
