Injectivity of coercions

Stream: new members

[Li Yao'an]

Through using library_search, I managed to complete the proof. Nonetheless, I'm still confused about how ↑ actually works. (Actually probably too confused to ask the right questions)

theorem t : ∀ s t : S, ∀ n : nat, ↑s = n ∧ n = ↑t → s = t :=
begin
    intros s t n h, have h2 : ↑ s = ↑ t, rw [h.1, h.2], exact subtype.eq h2,
end

theorem t' : ∀ s t : S, ∀ n : nat, ↑s = n ∧ n = ↑t → s = t :=
begin
    intros s t n h, apply subtype.eq, sorry
end

The issue with the second proof is that ↑t doesn't seem equivalent to t.val, which is used in subtype.eq. So how does the first proof work?

Further, how should this proof be written?

[Mario Carneiro]

↑t is indeed defeq to t.val

[Mario Carneiro]

theorem t' : ∀ s t : S, ∀ n : nat, ↑s = n ∧ n = ↑t → s = t :=
begin
    intros s t n h, apply subtype.eq, exact h.1.trans h.2
end

[Kevin Buzzard]

Now the rws are gone it's a nice exercise to write this proof in term mode.

[Johan Commelin]

The issue with the second proof is that ↑t doesn't seem equivalent to t.val, which is used in subtype.eq. So how does the first proof work?

@Li Yao'an They are not syntactically equal, but the are definitionally equal.