Lean4
/-- The `subsingleton` tactic tries to prove a goal of the form `x = y` or `x ≍ y`
using the fact that the types involved are *subsingletons*
(a type with exactly zero or one terms).
To a first approximation, it does `apply Subsingleton.elim`.
As a nicety, `subsingleton` first runs the `intros` tactic.
- If the goal is an equality, it either closes the goal or fails.
- `subsingleton [inst1, inst2, ...]` can be used to add additional `Subsingleton` instances
to the local context. This can be more flexible than
`have := inst1; have := inst2; ...; subsingleton` since the tactic does not require that
all placeholders be solved for.
Techniques the `subsingleton` tactic can apply:
- proof irrelevance
- heterogeneous proof irrelevance (via `proof_irrel_heq`)
- using `Subsingleton` (via `Subsingleton.elim`)
- proving `BEq` instances are equal if they are both lawful (via `lawful_beq_subsingleton`)
### Properties
The tactic is careful not to accidentally specialize `Sort _` to `Prop`,
avoiding the following surprising behavior of `apply Subsingleton.elim`:
```lean
example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim
```
The reason this `example` goes through is that
it applies the `∀ (p : Prop), Subsingleton p` instance,
specializing the universe level metavariable in `Sort _` to `0`.
-/
@[tactic_parser 1000]
public meta def subsingletonStx : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.subsingletonStx 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "subsingleton" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.symbol✝ "["))
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
(ParserDescr.symbol✝ "]"))))
