The check_compositions tactic, which checks the typing of categorical compositions in the goal, reporting discrepancies at "instances and reducible" transparency.

Reports from this tactic do not necessarily indicate a problem, although typically simp should reduce rather than increase the reported discrepancies.

check_compositions may be useful in diagnosing uses of erw in the category theory library.

def Mathlib.Tactic.CheckCompositions.forEachComposition (e : Lean.Expr) (f : Lean.Expr → Lean.MetaM Unit) : Lean.MetaM Unit

Find appearances of CategoryStruct.comp C inst X Y Z f g, and apply f to each.

Equations

• Mathlib.Tactic.CheckCompositions.forEachComposition e f = e.forEach fun (e : Lean.Expr) => if e.isAppOfArity `CategoryTheory.CategoryStruct.comp 7 = true then f e else pure ()

def Mathlib.Tactic.CheckCompositions.checkComposition (e : Lean.Expr) : Lean.MetaM Unit

Given a composition CategoryStruct.comp _ _ X Y Z f g, infer the types of f and g and check whether their sources and targets agree, at "instances and reducible" transparency, with X, Y, and Z, reporting any discrepancies.

Equations

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

def Mathlib.Tactic.CheckCompositions.checkCompositions (e : Lean.Expr) : Lean.MetaM Unit

Check the typing of categorical compositions in an expression.

Equations

• Mathlib.Tactic.CheckCompositions.checkCompositions e = Mathlib.Tactic.CheckCompositions.forEachComposition e Mathlib.Tactic.CheckCompositions.checkComposition

def Mathlib.Tactic.CheckCompositions.checkCompositionsTac : Lean.Elab.Tactic.TacticM Unit

Check the typing of categorical compositions in the goal.

Equations

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

def Mathlib.Tactic.CheckCompositions.tacticCheck_compositions : Lean.ParserDescr

For each composition f ≫ g in the goal, which internally is represented as CategoryStruct.comp C inst X Y Z f g, infer the types of f and g and check whether their sources and targets agree with X, Y, and Z at "instances and reducible" transparency, reporting any discrepancies.

An example:

example (j : J) :
    colimit.ι ((F ⋙ G) ⋙ H) j ≫ (preservesColimitIso (G ⋙ H) F).inv =
      H.map (G.map (colimit.ι F j)) := by

  -- We know which lemma we want to use, and it's even a simp lemma, but `rw`
  -- won't let us apply it
  fail_if_success rw [ι_preservesColimitIso_inv]
  fail_if_success rw [ι_preservesColimitIso_inv (G ⋙ H)]
  fail_if_success simp only [ι_preservesColimitIso_inv]

  -- This would work:
  -- erw [ι_preservesColimitIso_inv (G ⋙ H)]

  -- `check_compositions` checks if the two morphisms we're composing are
  -- composed by abusing defeq, and indeed it tells us that we are abusing
  -- definitional associativity of composition of functors here: it prints
  -- the following.

  -- info: In composition
  --   colimit.ι ((F ⋙ G) ⋙ H) j ≫ (preservesColimitIso (G ⋙ H) F).inv
  -- the source of
  --   (preservesColimitIso (G ⋙ H) F).inv
  -- is
  --   colimit (F ⋙ G ⋙ H)
  -- but should be
  --   colimit ((F ⋙ G) ⋙ H)

  check_compositions

  -- In this case, we can "fix" this by reassociating in the goal, but
  -- usually at this point the right thing to do is to back off and
  -- check how we ended up with a bad goal in the first place.
  dsimp only [Functor.assoc]

  -- This would work now, but it is not needed, because simp works as well
  -- rw [ι_preservesColimitIso_inv]

  simp

Equations

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