## Stream: new members

### Topic: Equality in prod

#### Marcus Rossel (Dec 30 2020 at 17:24):

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 (Dec 30 2020 at 17:25):

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

#### Sebastien Gouezel (Dec 30 2020 at 17:26):

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


#### Rob Lewis (Dec 30 2020 at 17:28):

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


#### Mario Carneiro (Dec 30 2020 at 22:47):

I would suggest cases h though

#### Mario Carneiro (Dec 30 2020 at 22:48):

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

#### Marcus Rossel (Mar 05 2021 at 15:59):

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 (Mar 05 2021 at 16:01):

Tag with ext:

@[ext]
structure s := ...


and write an ext_iff

#### Eric Wieser (Mar 05 2021 at 16:03):

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


#### Eric Wieser (Mar 05 2021 at 16:03):

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

#### Marcus Rossel (Mar 05 2021 at 16:05):

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

#### Eric Wieser (Mar 05 2021 at 16:06):

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

#### Marcus Rossel (Mar 08 2021 at 18:39):

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 (Mar 08 2021 at 18:41):

@Marcus Rossel

intro h,
apply_assumption,
ext,
assumption'


#### Johan Commelin (Mar 08 2021 at 18:41):

(I didn't test this)

#### Marcus Rossel (Mar 08 2021 at 18:42):

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

#### Ruben Van de Velde (Mar 08 2021 at 18:46):

TIL apply_assumption (though apply hₙ might be clearer)

#### Johan Commelin (Mar 08 2021 at 18:52):

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

Last updated: May 17 2021 at 23:14 UTC