(a, b) = (c,d)

Stream: new members

[Kind Bubble]

can anyone solve my puzzle exactly?

Here it is:

universe u
def F {A : u} {B : u} {a1 : A} {a2 : A} {b1 : B} {b2 : B} (p : a1 = b1) (q : a2 = b2) : (a1, a2) = (b1, b2) := sorry

[Patrick Johnson]

Your snippet has syntax and semantic errors. Do you mean Type u instead of u? Do you also mean {a1 : A} {a2 : B} {b1 : A} {b2 : B} instead? If so, here is the proof (it should be lemma, not a def):

universe u
lemma F {A B : Type u} {a1 : A} {a2 : B} {b1 : A} {b2 : B}
  (p : a1 = b1) (q : a2 = b2) : (a1, a2) = (b1, b2) := by rw [p, q]