mathlib documentation

tactic.rewrite

meta def tactic.match_fn  :

meta def tactic.mk_assoc  :

meta def tactic.assoc_root  :
exprexprexprtactic (expr × expr)

meta def tactic.assoc_refl'  :
exprexprexprexprtactic expr

meta def tactic.flatten  :
exprexprexprtactic (expr × expr)

assoc_rewrite [h₀,← h₁] at ⊢ h₂ behaves like rewrite [h₀,← h₁] at ⊢ h₂ with the exception that associativity is used implicitly to make rewriting possible.