Identifying equal (?) sets

Stream: maths

[Ashvni Narayanan]

def clopen_basis' : set (clopen_sets ((zmod d) × ℤ_[p])) :=
{x : clopen_sets ((zmod d) × ℤ_[p]) | ∃ (n : ℕ) (a : zmod (d * (p^n))),
  x = ⟨({a} : set (zmod d)).prod (set.preimage (padic_int.to_zmod_pow n) {(a : zmod (p^n))}),
    is_clopen_prod (is_clopen_discrete (a : zmod d))
      (proj_lim_preimage_clopen p d n a) ⟩ }

The definition above describes a clopen basis, of type set (clopen_sets ((zmod d) × ℤ_[p])) . I am trying to prove a lemma which gives me as input U : clopen_sets clopen_sets ((zmod d) × ℤ_[p]) and hU : U ∈ clopen_basis' p d. I want to use this information to construct V : clopen_basis' p d, such that, (mathematically) V = U. When I try set V := ⟨U, hU⟩ with hV,, I get the following error :

invalid constructor ⟨...⟩, expected type is not an inductive type
  ?m_1

However, if I do have V : clopen_basis' p d := ⟨U, hU⟩, this works. This is not useful though, since Lean does not remember the proof of the statement.

Another option that works is set V := subtype.mk U hU with hV, however, it does not recognize V to have the desired type, instead, V has type {x // x ∈ clopen_basis' p d}. This makes complete sense, but there must be a way to identify this to be the same as clopen_basis' p d.

Any help is appreciated, thank you!

[Adam Topaz]

Does set V : clopen_basis' p d := ⟨U, hU⟩ with hV work? It's hard to tell what's going on without a #mwe

[Ashvni Narayanan]

Apologies, it is a little difficult to provide an MWE for this, let me try.

[Ashvni Narayanan]

Adam Topaz said:

Does set V : clopen_basis' p d := ⟨U, hU⟩ with hV work? It's hard to tell what's going on without a #mwe

I get the following error :

invalid definev tactic, value has type
  {x // x ∈ clopen_basis' p d}
but is expected to have type
  clopen_basis' p d

[Adam Topaz]

Ah. Try set V : ↥(clopen_basis' p d) := ⟨U, hU⟩ with hV

[Ashvni Narayanan]

Ah, thank you!
Alternatively, I just realized I could convert clopen_basis' p d into a subtype, and that might just end up working out.

[Adam Topaz]

I don't really know what you're trying to prove here, but you might want to use docs#is_topological_basis_clopen

[Adam Topaz]

and docs#is_topological_basis_infi

[Ashvni Narayanan]

I will keep those in mind, thank you! :)

[Adam Topaz]

docs#topological_space.is_topological_basis.prod might also be useful