Documentation Verification Report

Core

📁 Source: Mathlib/Tactic/GCongr/Core.lean

Statistics

Metric	Count
Definitions `applyWithArity`, `gcongr`, `gcongrForward`, `GCongrKey`, `arity`, `head`, `relName`, `GCongrLemma`, `declName`, `key`, `mainSubgoals`, `numHyps`, `numVarying`, `prio`, `prioLE`, `GCongrLemmas`, `addGCongrLemmaEntry`, `containsHoleAnnotation`, `elabCHoleExpand`, `exact`, `exactRefl`, `gcongrDischarger`, `gcongrExt`, `gcongrForwardDischarger`, `gcongrHoleExpand`, `getCongrAppFnArgs`, `getRel`, `hasHoleAnnotation`, `instBEqGCongrKey`, `beq`, `instInhabitedGCongrKey`, `default`, `instInhabitedGCongrLemma`, `default`, `instOrdGCongrKey`, `makeGCongrLemma`, `mkHoleAnnotation`, `relImpRelLemma`, `symmExact`, `tacticGcongr___With___`, `tacticGcongr_discharger`, `updateRel`, `«tacticRel[_]»`	43
Theorems `rel_imp_rel`	1
Total	44

Lean.MVarId

Definitions

Name	Category	Theorems
`applyWithArity` 📖	CompOp	—
`gcongr` 📖	CompOp	—
`gcongrForward` 📖	CompOp	—

Mathlib.Tactic.GCongr

Definitions

Name	Category	Theorems
`GCongrKey` 📖	CompData	—
`GCongrLemma` 📖	CompData	—
`GCongrLemmas` 📖	CompOp	—
`addGCongrLemmaEntry` 📖	CompOp	—
`containsHoleAnnotation` 📖	CompOp	—
`elabCHoleExpand` 📖	CompOp	—
`exact` 📖	CompOp	—
`exactRefl` 📖	CompOp	—
`gcongrDischarger` 📖	CompOp	—
`gcongrExt` 📖	CompOp	—
`gcongrForwardDischarger` 📖	CompOp	—
`gcongrHoleExpand` 📖	CompOp	—
`getCongrAppFnArgs` 📖	CompOp	—
`getRel` 📖	CompOp	—
`hasHoleAnnotation` 📖	CompOp	—
`instBEqGCongrKey` 📖	CompOp	—
`instInhabitedGCongrKey` 📖	CompOp	—
`instInhabitedGCongrLemma` 📖	CompOp	—
`instOrdGCongrKey` 📖	CompOp	—
`makeGCongrLemma` 📖	CompOp	—
`mkHoleAnnotation` 📖	CompOp	—
`relImpRelLemma` 📖	CompOp	—
`symmExact` 📖	CompOp	—
`tacticGcongr___With___` 📖	CompOp	—
`tacticGcongr_discharger` 📖	CompOp	—
`updateRel` 📖	CompOp	—
`«tacticRel[_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rel_imp_rel` 📖	—	—	—	—	`IsTrans.trans`

Mathlib.Tactic.GCongr.GCongrKey

Definitions

Name	Category	Theorems
`arity` 📖	CompOp	—
`head` 📖	CompOp	—
`relName` 📖	CompOp	—

Mathlib.Tactic.GCongr.GCongrLemma

Definitions

Name	Category	Theorems
`declName` 📖	CompOp	—
`key` 📖	CompOp	—
`mainSubgoals` 📖	CompOp	—
`numHyps` 📖	CompOp	—
`numVarying` 📖	CompOp	—
`prio` 📖	CompOp	—
`prioLE` 📖	CompOp	—

Mathlib.Tactic.GCongr.instBEqGCongrKey

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Tactic.GCongr.instInhabitedGCongrKey

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Tactic.GCongr.instInhabitedGCongrLemma

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index