Zulip Chat Archive

Stream: new members

Topic: coe_eq_self

Alex Zhang (Jul 17 2021 at 21:45):

I am facing a goal ⊢ univ.card = univ.card
Is there a way to make lean kind of fully express the LHS and RHS?

Eric Wieser (Jul 17 2021 at 21:53):

set_option pp.implicit true

Eric Wieser (Jul 17 2021 at 21:54):

congr ~~will~~ may close that goal

Alex Zhang (Jul 17 2021 at 22:01):

After exploring things, I think the issue I face is the following (possibly because of improper previous steps for the proof). But is it possible to prove?

import data.fintype.card
variables {I : Type*}

lemma coe_univ_eq_self :
  ↥(@set.univ I) = I :=
begin
  simp [coe_sort, has_coe_to_sort.coe],
  sorry
end

Floris van Doorn (Jul 18 2021 at 13:14):

But you are able to show that they have the same cardinality.

Floris van Doorn (Jul 18 2021 at 13:53):

import data.fintype.card
variables {I : Type*} [fintype I]

lemma coe_univ_eq_self :
  fintype.card (@set.univ I) = fintype.card I :=
fintype.card_of_subtype finset.univ $ by simp

Last updated: Dec 20 2023 at 11:08 UTC