The Core function for monoidal and bicategory tactics

This file provides the function BicategoryLike.main for proving equalities in monoidal categories and bicategories. Using main, we will define the following tactics:

• monoidal at Mathlib/Tactic/CategoryTheory/Monoidal/Basic.lean
• bicategory at Mathlib/Tactic/CategoryTheory/Bicategory/Basic.lean

The main first normalizes the both sides using eval, then compares the corresponding components. It closes the goal at non-structural parts with rfl and the goal at structural parts by pureCoherence.

theorem Mathlib.Tactic.BicategoryLike.mk_eq {α : Type u_1} (a b a' b' : α) (ha : a = a') (hb : b = b') (h : a' = b') : a = b

def Mathlib.Tactic.BicategoryLike.normalForm (ρ : Type) [Context ρ] [MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)] [MonadNormalExpr (CoherenceM ρ)] [MkEval (CoherenceM ρ)] [MkMor₂ (CoherenceM ρ)] [MonadMor₂ (CoherenceM ρ)] (nm : Lean.Name) (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Transform an equality between 2-morphisms into the equality between their normalizations.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Tactic.BicategoryLike.mk_eq_of_cons {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {f₁ f₂ f₃ f₄ : C} (α α' : f₁ ⟶ f₂) (η η' : f₂ ⟶ f₃) (ηs ηs' : f₃ ⟶ f₄) (e_α : α = α') (e_η : η = η') (e_ηs : ηs = ηs') : CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp η ηs) = CategoryTheory.CategoryStruct.comp α' (CategoryTheory.CategoryStruct.comp η' ηs')

def Mathlib.Tactic.BicategoryLike.ofNormalizedEq (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Split the goal α ≫ η ≫ ηs = α' ≫ η' ≫ ηs' into α = α', η = η', and ηs = ηs'.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.BicategoryLike.List.splitEvenOdd {α : Type u} : List α → List α × List α

List.splitEvenOdd [0, 1, 2, 3, 4] = ([0, 2, 4], [1, 3])

Equations

• Mathlib.Tactic.BicategoryLike.List.splitEvenOdd [] = ([], [])
• Mathlib.Tactic.BicategoryLike.List.splitEvenOdd [a] = ([a], [])
• Mathlib.Tactic.BicategoryLike.List.splitEvenOdd (a :: b :: xs) = match Mathlib.Tactic.BicategoryLike.List.splitEvenOdd xs with | (as, bs) => (a :: as, b :: bs)

def Mathlib.Tactic.BicategoryLike.main (ρ : Type) [Context ρ] [MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)] [MonadNormalExpr (CoherenceM ρ)] [MkEval (CoherenceM ρ)] [MkMor₂ (CoherenceM ρ)] [MonadMor₂ (CoherenceM ρ)] [MonadCoherenceHom (CoherenceM ρ)] [MonadNormalizeNaturality (CoherenceM ρ)] [MkEqOfNaturality (CoherenceM ρ)] (nm : Lean.Name) (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

The core function for monoidal and bicategory tactics.

Equations

• One or more equations did not get rendered due to their size.