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
• bicategory at Mathlib.Tactic.CategoryTheory.Bicategory.Basic

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) [Mathlib.Tactic.BicategoryLike.Context ρ] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂ (Mathlib.Tactic.BicategoryLike.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₁ : C} {f₂ : C} {f₃ : C} {f₄ : C} (α : f₁ ⟶ f₂) (α' : f₁ ⟶ f₂) (η : f₂ ⟶ f₃) (η' : f₂ ⟶ f₃) (ηs : f₃ ⟶ f₄) (η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) [Mathlib.Tactic.BicategoryLike.Context ρ] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEqOfNaturality (Mathlib.Tactic.BicategoryLike.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.