Equality of objects of the same structure

Stream: general

[Klaus Mattis]

I have a question regarding structures:
I don't quite understand equality of objects of structures,
for example in the following example:

structure point :=
(x : ℤ)

lemma ext_point (p q : point) (h : p.x = q.x) : p = q :=
begin
  sorry
end

I want to show that two objects of the structure are equal, if they carry the same data.
Is this true? If yes, how does one show this?
If no, could (or should) one add this as an axiom?

Thanks in advance!

[Eric Wieser]

I forget this one every time - I think the answer is cases p, cases q,

[Eric Wieser]

It becomes easier if you put @[ext] before structure point, then your statement is exactly point.ext

[Bryan Gin-ge Chen]

Following Eric's comment (the commented out lines use mathlib):

-- import tactic

-- @[ext]
structure point :=
(x : ℤ)

lemma ext_point (p q : point) (h : p.x = q.x) : p = q :=
begin
  cases p,
  cases q,
  dsimp only at h, -- change p = q at h, -- also works
  rw h,
end

-- lemma ext_point' (p q : point) (h : p.x = q.x) : p = q :=
-- point.ext p q h

[Klaus Mattis]

Great, that works :)
Thanks a lot.

[Patrick Massot]

About your axiom question: when you use the inductive command (or its special case the structure command), Lean does add an axiom to the system, the recursor of the inductive type, here point.rec. If you want to write you proof directly in term of this axiom (and the axiom eq.rec that was created when defining equality), that would be:

structure point :=
(x : ℤ)

lemma point.ext {p q : point} (h : p.x = q.x) : p = q :=
point.rec (λ (n : ℤ) (h' : n = q.x), point.rec (λ (m : ℤ) (H : n = m), eq.rec rfl H) q h') p h

You probably don't want to know more about this, but I thought I would show you just in case.