Def Lean.MVarId.applyWithArity

Modification history

2025-07-31 09:17
Mathlib/Tactic/GCongr/Core.lean
feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907) …
Added Lean.MVarId.applyWithArityView on Github →