Commit 2023-09-04 23:28 27866b84
View on Github →feat: documentation for Mathlib.Tactic.Have (#6950)
This PR adds documentation for Mathlib.Tactic.Have
It also deletes content in a namespace that was instructed to be deleted after the merge of https://github.com/leanprover/lean4/pull/2262, which was merged in the 9th of June (2023)