Zulip Chat Archive

Stream: new members

Topic: decidable_eq


view this post on Zulip Ashwin Iyengar (Feb 18 2021 at 15:13):

Is there an easy way around this kind of decidable_eq issue?

import ring_theory.power_series.basic

variables (σ R : Type*)

lemma test (P : (σ →₀ )  Prop) (Y : set (σ →₀ )) (h : Y.finite) : {x : σ →₀  | P x}.finite :=
begin
  apply (h.bUnion (λ i _, (finset.image (λ x : (σ →₀ ) × (σ →₀ ), x.1) i.antidiagonal.support).finite_to_set)).subset,
end

Basically I want to prove that a certain set of indices is finite, and to do so I want to refine the goal to say that the elements of my set appear as the first (or second, doesn't really matter) member of a pair appearing in the union of the (finite) antidiagonals taken over the elements of some auxiliary finite set of indices.

view this post on Zulip Eric Wieser (Feb 18 2021 at 15:28):

Start your proof with classical,

view this post on Zulip Eric Wieser (Feb 18 2021 at 15:29):

Or for more precision, haveI : decidable_eq σ := classical.dec_eq _,, which is less likely to cause trouble with conflicting instances


Last updated: May 13 2021 at 05:21 UTC