Zulip Chat Archive

Stream: general

Topic: simp bUnion

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?

Yury G. Kudryashov (Jun 24 2020 at 21:41):

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

Yury G. Kudryashov (Jun 24 2020 at 21:44):

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

Last updated: Dec 20 2023 at 11:08 UTC