Commit 2023-01-08 01:33 02752cba
View on Github →feat: port the lift tactic (#723)
Mostly works, doesn't simplify if used as lift a to α with b hb.
Based on leanprover-community/mathlib@e50b8c2
feat: port the lift tactic (#723)
Mostly works, doesn't simplify if used as lift a to α with b hb.
Based on leanprover-community/mathlib@e50b8c2