PR #17958 fix(tactic/tauto) fix some bugs in symm_eq

fix(tactic/tauto) avoid returning invalid rfl proof from symm_eq

dwrensha committed 3 years ago

avoid adding edge which could create cycles

dwrensha committed 3 years ago

simplify, and add a bit more documentation

dwrensha committed 3 years ago

fix an add_edge

dwrensha committed 3 years ago

fix 'implies' case of symm_eq

dwrensha committed 3 years ago

mathlib3 fix(tactic/tauto) fix some bugs in symm_eq #17958 Open