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

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

dwrensha wants to merge 5 commits into master from dwrensha-tauto-cleanup

dwrensha force pushed from b04c6c9c to ea58bd0e 3 years ago

dwrensha force pushed from ea58bd0e to b138ce00 3 years ago

dwrensha commented on 2022-12-20

dwrensha marked this pull request as ready for review 3 years ago

dwrensha requested a review 3 years ago

dwrensha added awaiting-review

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

fcd7a470

avoid adding edge which could create cycles

77823910

simplify, and add a bit more documentation

30663881

fix an add_edge

58cd9502

fix 'implies' case of symm_eq

f4642c83

dwrensha force pushed from 2c4b787d to f4642c83 3 years ago

dwrensha changed the title ~~fix(tactic/tauto) avoid returning invalid rfl proof from symm_eq~~ fix(tactic/tauto) fix some bugs in symm_eq 3 years ago

dwrensha commented on 2022-12-21

eric-wieser requested a review from

digama0 3 years ago

eric-wieser added t-meta

eric-wieser added not-too-late

kim-em removed not-too-late

kim-em added too-late

kim-em removed review request 2 years ago

Reviewers

digama0

Assignees

No one assigned

Labels

awaiting-review t-meta too-late

Milestone

No milestone

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

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

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

Open