ExistsAndEq
📁 Source: Mathlib/Tactic/Simproc/ExistsAndEq.lean
Statistics
| Metric | Count |
|---|---|
| 19 | |
| Theorems | 0 |
| Total | 19 |
ExistsAndEq
Definitions
| Name | Category | Theorems |
|---|---|---|
GoTo 📖 | CompData | — |
HypQ 📖 | CompOp | — |
VarQ 📖 | CompOp | — |
existsAndEq 📖 | CompOp | — |
findEq 📖 | CompOp | — |
findEqPath 📖 | CompOp | — |
instBEqGoTo 📖 | CompOp | — |
instInhabitedGoTo 📖 | CompOp | — |
instInhabitedHypQ 📖 | CompOp | — |
instInhabitedVarQ 📖 | CompOp | — |
mkAfterToBefore 📖 | CompOp | — |
mkBeforeToAfter 📖 | CompOp | — |
mkNestedExists 📖 | CompOp | — |
withExistsElimAlongPath 📖 | CompOp | — |
withExistsElimAlongPathImp 📖 | CompOp | — |
withNestedExistsElim 📖 | CompOp | — |
withNestedExistsIntro 📖 | CompOp | — |
ExistsAndEq.instBEqGoTo
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
ExistsAndEq.instInhabitedGoTo
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---