mathlib3
fix(tactic/induction): fix generalisation with complex major premise
#7707

Open

fix(tactic/induction): fix generalisation with complex major premise #7707

JLimperg wants to merge 2 commits into master from induction-bug-complex-major-premise-generalisation

JLimperg added WIP

JLimperg added t-meta

JLimperg removed WIP

JLimperg added awaiting-review

eric-wieser commented on 2021-05-25

Vierkantor commented on 2021-06-01

Vierkantor removed awaiting-review

Vierkantor added awaiting-author

github-actions added merge-conflict

fix(tactic/induction): fix generalisation with complex major premise

ff959b99

Make test case more rigid

f13a7b91

JLimperg force pushed from 9168b688 to f13a7b91 4 years ago

github-actions removed merge-conflict

kim-em added too-late

eric-wieser requested a review 2 years ago

Reviewers

Vierkantor

eric-wieser

Assignees

No one assigned

Labels

awaiting-author t-meta too-late

Milestone

No milestone