Documentation Verification Report

CongrTheorems

📁 Source: Mathlib/Lean/Meta/CongrTheorems.lean

Statistics

Metric	Count
Definitions `FastIsEmpty`, `FastSubsingleton`, `fastSubsingletonElim`, `mkHCongrWithArity'`, `mkRichHCongr`, `withSubsingletonAsFast`	6
Theorems `inst`, `elim`, `helim`, `inst`, `instFastIsEmptyEmpty`, `instFastIsEmptyFalse`, `instFastIsEmptyFinOfNatNat`, `instFastSubsingleton`, `instFastSubsingletonDecidable`, `instFastSubsingletonFinOfNatNat`, `instFastSubsingletonForall`, `instFastSubsingletonForallOfFastIsEmpty`, `instFastSubsingletonOfFastIsEmpty`, `instFastSubsingletonPUnit`	14
Total	20

Lean.Meta

Definitions

Name	Category	Theorems
`FastIsEmpty` 📖	CompData	3 math math: `instFastIsEmptyFalse`, `instFastIsEmptyFinOfNatNat`, `instFastIsEmptyEmpty`
`FastSubsingleton` 📖	CompData	7 math math: `instFastSubsingletonForallOfFastIsEmpty`, `Fintype.instFastSubsingleton`, `instFastSubsingletonDecidable`, `instFastSubsingletonOfFastIsEmpty`, `instFastSubsingleton`, `instFastSubsingletonFinOfNatNat`, `instFastSubsingletonPUnit`
`fastSubsingletonElim` 📖	CompOp	—
`mkHCongrWithArity'` 📖	CompOp	—
`mkRichHCongr` 📖	CompOp	—
`withSubsingletonAsFast` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFastIsEmptyEmpty` 📖	mathematical	—	`FastIsEmpty`	—	`Empty.instIsEmpty`
`instFastIsEmptyFalse` 📖	mathematical	—	`FastIsEmpty`	—	`instIsEmptyFalse`
`instFastIsEmptyFinOfNatNat` 📖	mathematical	—	`FastIsEmpty`	—	`Fin.isEmpty'`
`instFastSubsingleton` 📖	mathematical	—	`FastSubsingleton`	—	—
`instFastSubsingletonDecidable` 📖	mathematical	—	`FastSubsingleton`	—	—
`instFastSubsingletonFinOfNatNat` 📖	mathematical	—	`FastSubsingleton`	—	—
`instFastSubsingletonForall` 📖	—	`FastSubsingleton`	—	—	`FastSubsingleton.inst`
`instFastSubsingletonForallOfFastIsEmpty` 📖	mathematical	—	`FastSubsingleton`	—	`IsEmpty.false` `FastIsEmpty.inst`
`instFastSubsingletonOfFastIsEmpty` 📖	mathematical	—	`FastSubsingleton`	—	`FastIsEmpty.inst` `IsEmpty.instSubsingleton`
`instFastSubsingletonPUnit` 📖	mathematical	—	`FastSubsingleton`	—	—

Lean.Meta.FastIsEmpty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inst` 📖	mathematical	—	`IsEmpty`	—	—

Lean.Meta.FastSubsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim` 📖	—	—	—	—	`inst`
`helim` 📖	—	—	—	—	`inst`
`inst` 📖	—	—	—	—	—

---

← Back to Index