Commit 2022-12-01 21:54 c8ba7d09

View on Github →

feat: port a basic version of applyAssumption (#708) This is the most boring version of apply_assumption that does not symmetry and so on, but I think it might be better to include this into mathlib4 now, maybe it solves some porting issues already. The other features are probably less trivial.

Estimated changes