decidable_eq

Stream: new members

[Ashwin Iyengar]

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]

Start your proof with classical,

[Eric Wieser]

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

[Alex Zhang]

What does decidable_eq n mean here?
variables (n : Type) [fintype n] [decidable_eq n]

[Alex Zhang]

Does it mean that the equality relation is decidable on n?

[Eric Wieser]

decidable_eq n is short for Π a b : n, decidable (a = b)

[Eric Wieser]

I think src#decidable_eq shows that