What even is definitional equality in structures?

Stream: new members

[Mantas Baksys]

After spending some time pondering the following issue and coming up with exactly nothing, I think's it's time to ask this question here :smiley: Below I post an example of a 'trivial' statement that I cannot close by refl, which baffles me.

import data.real.basic

structure dissection (a b : ℝ) (S : finset ℝ) :=
(N := S.card)
(mem_Icc: ∀ x ∈ S, a ≤  x ∧ x ≤ b)
(mem_endpoints : ∃ x ∈ S, x = a ∧ ∃ y ∈ S, y = b)

lemma dissection_card_def {a b: ℝ} {S: finset ℝ} (D: dissection a b S) : D.N = S.card :=
begin
   sorry,
end

I'm really lost why this happens (and what do I need to fix it), so I'll appreciate any help I get!

[Scott Morrison]

When you write N := S.card, you are not saying that "N is always S.card". You are only providing a default value.

[Scott Morrison]

Why is N even a field of dissection, rather than a separate def?

[Mantas Baksys]

Thanks @Scott Morrison , I'll define it separately. I wanted to define N inside dissection for elegance in notation (it's tiresome to always write S.card). But there's probably an easier way (and actually working) way to do this, I'm guessing.

[Scott Morrison]

Just def dissection.N (a b : ℝ) (S : finset ℝ) (D : dissection a b S) : nat := S.card.

[Mantas Baksys]

Thank you so much, @Scott Morrison. I'll just use def every time I want to say 'this is true by definition'. It's really obvious in hindsight, but surprisingly it wasn't at first.

[Eric Wieser]

def says "this is the definition", not "this is true"

[Eric Wieser]

Since the statement "nat is true" is nonsense

[Mantas Baksys]

Pardon my language, I completely agree @Eric Wieser .