Commit 2023-05-03 14:00 d65ed3b2

refactor, fix: MetaM version of rfl tactic and missing whnfR/instantiateMVars (#3758) This PR factors out a MetaM version of the rfl tactic and adds a missing whnfR and instantiateMVars in front of the goal type. This means that a few rws across mathlib4 now close the goal instead of e.g. requiring a trailing exact le_rfl. Note: we do not use whnfR on the return type when adding the refl extension in the first place, as forallMetaTelescopeReducing already performs whnf (here, at reducible transparency). See zulip for some discussion on the internal changes made.