Equality in `prod`

Stream: new members

[Marcus Rossel]

I have a proof that (n, m) = (x, y). How can I get a proof from this, that (n = x) ∧ (m = y)?

[Bryan Gin-ge Chen]

You should be able to rewrite with docs#mk.inj_iff.

[Sebastien Gouezel]

lemma foo {α β : Type*} (x m : α) (y n : β) (h : ((x, y) : (α × β)) = (m, n)) :
  x = m ∧ y = n :=
begin
  simpa using h,
end

[Rob Lewis]

More importantly, to find the answer on your own:

example {α} (a b c d : α) (h : (a, b) = (c, d)) : a = c ∧ b = d :=
by library_search     -- prod.mk.inj h

[Mario Carneiro]

I would suggest cases h though

[Mario Carneiro]

injection h does more directly what you are looking for, but if those variables are actually variables and not expressions then cases h will perform the substitution of one for the other in your goal

[Eric Wieser]

Link for the lazy: tactic#injection

[Marcus Rossel]

I don't understand how to use injection. E.g.:

structure s :=
  (a : int)
  (b : nat)

example {x x' : s} (h : x = x') : true :=
begin
  injection h,
  -- injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor
end

So how can I add the hypothesis x.a = x'.a and x.b = x'.b?

[Yakov Pechersky]

Tag with ext:

@[ext]
structure s := ...

and write an ext_iff

[Eric Wieser]

example {x x' : s} (h : x = x') : true :=
begin
  cases x,
  cases x',
  injection h,
  sorry
end

[Eric Wieser]

But @Yakov Pechersky is correct that @[ext] will probably do what you're actually trying to do

[Marcus Rossel]

Indeed: @[ext] causes invalid definition, a declaration named 's.ext_iff' has already been declared when trying to declare it manually.

[Eric Wieser]

s.mk.inj is also close to what you want, and exists even without ext

[Marcus Rossel]

How does this work for inequalities? E.g:

@[ext] structure thing := (a : ℕ) (b : ℤ)

example (t t' : thing) (hₙ : t ≠ t') (hₑ : t.a = t'.a) : t.b ≠ t'.b :=
  sorry

[Johan Commelin]

@Marcus Rossel

intro h,
apply_assumption,
ext,
assumption'

[Johan Commelin]

(I didn't test this)

[Marcus Rossel]

This does indeed work, but I don't understand it yet. I'll have to read up on the tactics.

[Ruben Van de Velde]

TIL apply_assumption (though apply hₙ might be clearer)

[Johan Commelin]

/me was to lazy to copy the unicode symbols (-;