Def Mathlib.Tactic.Nontriviality.nontrivialityByElim

Modification history

2024-07-15 14:00
Mathlib/Tactic/Nontriviality/Core.lean
chore(Tactic): reduce use of Implicit, part 2 (#14726)
Modified Mathlib.Tactic.Nontriviality.nontrivialityByElimView on Github →
2022-11-21 03:50
Mathlib/Tactic/Nontriviality/Core.lean
feat: `nontriviality` tactic (#600) …
Added Mathlib.Tactic.Nontriviality.nontrivialityByElimView on Github →