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.

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'.

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

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

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

The core function for monoidal and bicategory tactics.