English
Corecursor roll: composing corec after f and g is equivalent to corec', via map composition.
Русский
Упаковка corec с Roll: композиция corec и f,g эквивалентна corec' через отображение.
LaTeX
$$$\\forall f:\\ X\\to Y,\\; g:\\ Y \\to F(\\alpha ::: X),\\; Cofix.corec (g \\circ f) x = Cofix.corec (MvFunctor.map (id ::: f) \\circ g) (f\\ x).$$$
Lean4
/-- tactic for proof by bisimulation -/
@[tactic_parser 1000]
public meta def tacticMv_bisim___With___ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.MvBisim.tacticMv_bisim___With___ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "mv_bisim" false✝)
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.cat✝ `term 0)))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with")
(ParserDescr.unary✝ `many1
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
Lean.binderIdent)))))
