Def Mathlib.Tactic.Nontriviality.elabNontriviality

Modification history

2022-11-21 03:50
Mathlib/Tactic/Nontriviality/Core.lean
feat: `nontriviality` tactic (#600) …
Added Mathlib.Tactic.Nontriviality.elabNontrivialityView on Github →