Zulip Chat Archive

Stream: general

Topic: simp bUnion


view this post on Zulip Yury G. Kudryashov (Jun 24 2020 at 21:32):

Why by simp fails to prove finset.bUnion_coe, see https://github.com/leanprover-community/mathlib/pull/3158/files#diff-b9bd60f00a197d11e68c59a4d223523eR2972? @Gabriel Ebner , do we miss some @[congr] lemma?

view this post on Zulip Yury G. Kudryashov (Jun 24 2020 at 21:41):

simp fails to apply lemmas about a∈s in ⋃ a ∈ s, t a.

view this post on Zulip Yury G. Kudryashov (Jun 24 2020 at 21:44):

(still not sure if this is a bug or a feature)


Last updated: May 12 2021 at 23:13 UTC