Lean4
/-- 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
```
-/
@[tactic_parser 1000]
public meta def tacticCheck_compositions : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.CheckCompositions.tacticCheck_compositions 1024
(ParserDescr.nonReservedSymbol✝ "check_compositions" false✝)
