Commit 2022-11-21 03:50 14429705

View on Github →

feat: nontriviality tactic (#600) Supercedes #548.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/LibrarySearch.lean

modified def Mathlib.Tactic.LibrarySearch.solveByElim

Created Mathlib/Tactic/Nontriviality.lean

Created Mathlib/Tactic/Nontriviality/Core.lean

added def Mathlib.Tactic.Nontriviality.elabNontriviality

added def Mathlib.Tactic.Nontriviality.nontrivialityByAssumption

added def Mathlib.Tactic.Nontriviality.nontrivialityByElim

added theorem Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim

Modified Mathlib/Tactic/SolveByElim.lean

Created test/nontriviality.lean

added def EmptyOrUniv

added theorem Set.empty_union

added theorem Subsingleton.set_empty_or_univ'

added theorem Subsingleton.set_empty_or_univ

added theorem zero_le_one

added theorem zero_le_two