Lean4
/-- Attempts to generate a `Nontrivial α` hypothesis.
The tactic first checks to see that there is not already a `Nontrivial α` instance
before trying to synthesize one using other techniques.
If the goal is an (in)equality, the type `α` is inferred from the goal.
Otherwise, the type needs to be specified in the tactic invocation, as `nontriviality α`.
The `nontriviality` tactic will first look for strict inequalities amongst the hypotheses,
and use these to derive the `Nontrivial` instance directly.
Otherwise, it will perform a case split on `Subsingleton α ∨ Nontrivial α`, and attempt to discharge
the `Subsingleton` goal using `simp [h₁, h₂, ..., hₙ, nontriviality]`, where `[h₁, h₂, ..., hₙ]` is
a list of additional `simp` lemmas that can be passed to `nontriviality` using the syntax
`nontriviality α using h₁, h₂, ..., hₙ`.
```
example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : 0 < a := by
nontriviality -- There is now a `Nontrivial R` hypothesis available.
assumption
```
```
example {R : Type} [CommRing R] {r s : R} : r * s = s * r := by
nontriviality -- There is now a `Nontrivial R` hypothesis available.
apply mul_comm
```
```
example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 := by
nontriviality R -- there is now a `Nontrivial R` hypothesis available.
dec_trivial
```
```
def myeq {α : Type} (a b : α) : Prop := a = b
example {α : Type} (a b : α) (h : a = b) : myeq a b := by
success_if_fail nontriviality α -- Fails
nontriviality α using myeq -- There is now a `Nontrivial α` hypothesis available
assumption
```
-/
@[tactic_parser 1000]
public meta def nontriviality : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Nontriviality.nontriviality 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "nontriviality" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.cat✝ `term 0))))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ")
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) Lean.Parser.Tactic.simpArg "," (ParserDescr.symbol✝ ", ")
Bool.false✝))))
