4. Tactic🔗

Modules in the Tactic slice are grouped from the first path component after the project root.

• Tactic.EqLift.ForMathlib.Kernel 3 declarations

• Tactic.EqLift.ForMathlib.MeasurableEquiv 1 declarations

• Tactic.EqLift.Kernel.Lift 16 declarations

• Tactic.EqLift.Tactic.Kernel.KernelLift 10 declarations

• Tactic.EqLift.Tactic.Lift 7 declarations

• Tactic.EqLift.Tactic.Utils 6 declarations

• Tactic.EqLift.Tactic.Universe 4 declarations

• Tactic.EqLift.Tactic.Location 2 declarations

• Tactic.EqLift.Tactic.Kernel.Utils 4 declarations

• Tactic.EqLift.Tactic.Kernel.KernelUnlift 10 declarations

• Tactic.EqLift.Tactic.Unlift 5 declarations

• Tactic.KernelHom.ForMathlib.LIntegral 1 declarations

• Tactic.KernelHom.Kernel.Hom 21 declarations

• Tactic.KernelHom.Kernel.MonoidalComp 8 declarations

• Tactic.KernelHom.Tactic.Delaborators 4 declarations

• Tactic.KernelHom.Tactic.HomKernel 10 declarations

• Tactic.KernelHom.Tactic.KernelHom 23 declarations

• Tactic.KernelHom.Tactic.Utils 3 declarations

• Tactic.KernelHom.Tactic.KernelCat 3 declarations

• Tactic.KernelHom.Tactic.KernelDiagram 10 declarations

• Tactic.KernelHom.Tactic.Reassoc 6 declarations

Module dependencies

Showing the 17 modules that depend on one another. The other 4 are independent of the rest of the chapter.