The rw_search
tactic has been removed from Mathlib. #
rw_search
has been removed from Mathlib.
Equations
- One or more equations did not get rendered due to their size.
rw_search
tactic has been removed from Mathlib. #rw_search
has been removed from Mathlib.