Def Lean.MVarId.applyWithArity

Modification history

2026-06-07 02:12
Mathlib/Tactic/GCongr/Core.lean
feat(GRewrite): new `grw` implementation (#38318) …
Deleted Lean.MVarId.applyWithArityView on Github →
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 →