Commit 2020-05-02 09:41 b902f6e0
View on Github →feat(*): several @[simp] lemmas (#2579)
Also add an explicit instance for submodule.has_coe_to_sort.
This way rintro ⟨x, hx⟩ results in (hx : x ∈ p).
Also fixes some timeouts introduced by #2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code