mathlib
3d451c70 - chore(tactic/interactive): propagate tags in `substs` (#6638)

Commit
4 years ago
chore(tactic/interactive): propagate tags in `substs` (#6638) Before this change, the `case left` tactic here did not work: ```lean example {α : Type*} (a b c : α) (h : a = b) : (a = b ∨ a = c) ∧ true := begin with_cases {apply and.intro}, substs' h, case left : { exact or.inl rfl }, case right : { trivial } end ```
Author
Parents
Loading