## Stream: new members

### Topic: decidable_eq

#### 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.

#### Eric Wieser (Feb 18 2021 at 15:28):

Start your proof with classical,

#### 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