mathlib3
feat(tactic/lift): prevent `lift` from failing if goal contains the hypothesis used to `lift`
#17869

Open

feat(tactic/lift): prevent `lift` from failing if goal contains the hypothesis used to `lift` #17869

adomani wants to merge 3 commits into master from adomani_yael_lift

yael's suggested change to lift

be654c59

adomani requested a review 3 years ago

more robust checks and a test

1dfdc6c5

eric-wieser commented on 2022-12-08

simpler test

c432be59

eric-wieser added awaiting-author

kim-em added too-late

kim-em removed review request 2 years ago

Reviewers

eric-wieser

Assignees

No one assigned

Labels

awaiting-author too-late

Milestone

No milestone