monoidal tactic

This file provides monoidal tactic, which solves equations in a monoidal category, where the two sides only differ by replacing strings of monoidal structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target. In other words, monoidal solves equalities where both sides have the same string diagrams.

The core function for the monoidal tactic is provided in Mathlib.Tactic.CategoryTheory.Coherence.Basic. See this file for more details about the implementation.

def Mathlib.Tactic.Monoidal.monoidalNf (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Normalize the both sides of an equality.

Equations

• Mathlib.Tactic.Monoidal.monoidalNf mvarId = Mathlib.Tactic.BicategoryLike.normalForm Mathlib.Tactic.Monoidal.Context `monoidal mvarId

def Mathlib.Tactic.Monoidal.tacticMonoidal_nf : Lean.ParserDescr

Normalize the both sides of an equality.

Equations

• Mathlib.Tactic.Monoidal.tacticMonoidal_nf = Lean.ParserDescr.node `Mathlib.Tactic.Monoidal.tacticMonoidal_nf 1024 (Lean.ParserDescr.nonReservedSymbol "monoidal_nf" false)

def Mathlib.Tactic.Monoidal.monoidal (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Use the coherence theorem for monoidal categories to solve equations in a monoidal category, where the two sides only differ by replacing strings of monoidal structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, monoidal can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using monoidal_coherence.

Equations

• Mathlib.Tactic.Monoidal.monoidal mvarId = Mathlib.Tactic.BicategoryLike.main Mathlib.Tactic.Monoidal.Context `monoidal mvarId

def Mathlib.Tactic.Monoidal.tacticMonoidal : Lean.ParserDescr

Use the coherence theorem for monoidal categories to solve equations in a monoidal category, where the two sides only differ by replacing strings of monoidal structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, monoidal can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using monoidal_coherence.

Equations

• Mathlib.Tactic.Monoidal.tacticMonoidal = Lean.ParserDescr.node `Mathlib.Tactic.Monoidal.tacticMonoidal 1024 (Lean.ParserDescr.nonReservedSymbol "monoidal" false)