The slice tactic

Applies a tactic to an interval of terms from a term obtained by repeated application of Category.comp.

def Mathlib.Tactic.Slice.slice : Lean.ParserDescr

slice is a conv tactic; if the current focus is a composition of several morphisms, slice a b reassociates as needed, and zooms in on the a-th through b-th morphisms. Thus if the current focus is (a ≫ b) ≫ ((c ≫ d) ≫ e), then slice 2 3 zooms to b ≫ c.

def Mathlib.Tactic.Slice.evalSlice (a b : ℕ) : Lean.Elab.Tactic.TacticM Unit

evalSlice

• rewrites the target expression using Category.assoc.
• uses congr to split off the first a-1 terms and rotates to a-th (last) term
• counts the number k of rewrites as it uses ←Category.assoc to bring the target to left associated form; from the first step this is the total number of remaining terms from C
• it now splits off b-a terms from target using congr leaving the desired subterm
• finally, it rewrites it once more using Category.assoc to bring it to right-associated normal form

def Mathlib.Tactic.Slice.convSlice___ : Lean.ParserDescr

slice is implemented by evalSlice.

def Mathlib.Tactic.Slice.sliceLHS : Lean.ParserDescr

slice_lhs a b => tac zooms to the left-hand side, uses associativity for categorical composition as needed, zooms in on the a-th through b-th morphisms, and invokes tac.

def Mathlib.Tactic.Slice.sliceRHS : Lean.ParserDescr

slice_rhs a b => tac zooms to the right-hand side, uses associativity for categorical composition as needed, zooms in on the a-th through b-th morphisms, and invokes tac.