How to prove equality of structure

Stream: new members

[Keyao Peng]

For example

variable (α : Type)
structure pair α  :=
(x : α)
(y : α)

def foo:  pair α -> pair α ->pair α :=
λ a b , {x := fx a.x b.x ,y := fy a.y b.y}

now I want to prove something like for some A B C : pair α

lemma bar: foo A B = C

which tactics I can use to reduce the goal to, {x := fx A.x B.x ,y := fy A.y B.y}={x :=C.x,y :=C.y} and finally become fx A.x B.x =C.x ∧ fy A.y B.y =C.y?

[Kevin Buzzard]

This question would be much easier to work with if what you posted compiled.

[Kevin Buzzard]

but cases A; cases B will get you started.

[Kevin Buzzard]

In general you should probably prove an ext lemma before you embark on proving bar

[Kevin Buzzard]

There's a way of getting the derive handler to derive ext but I can never remember how to do it and I don't know how to look it up :-(

[Rob Lewis]

@[ext]?

[Johan Commelin]

@Keyao Peng You are looking for cases A, cases B, cases C, congr,

[Keyao Peng]

Kevin Buzzard said:

but cases A; cases B will get you started.

when use cases A; cases B;cases C it just becomes foo {x := A.x , y:=A.y} {x := B.x , y:=B.y} = {x := C.x , y:=C.y}, but I want {x := fx A.x B.x ,y := fy A.y B.y}={x :=C.x,y :=C.y}

[Kevin Buzzard]

import tactic

variable {α : Type}

@[ext] structure pair (α : Type) :=
(x : α)
(y : α)

def foo (fx fy : α → α → α):  pair α -> pair α ->pair α :=
λ a b, {x := fx a.x b.x ,y := fy a.y b.y}

lemma bar (fx fy : α → α → α) (A B C : pair α):
  foo fx fy A B = C :=
begin
  ext,
  /-
2 goals
α : Type,
fx fy : α → α → α,
A B C : pair α
⊢ (foo fx fy A B).x = C.x

α : Type,
fx fy : α → α → α,
A B C : pair α
⊢ (foo fx fy A B).y = C.y
  -/
  cases A, cases B, cases C, all_goals {dsimp [foo]},
  /-
α : Type,
fx fy : α → α → α,
A_x A_y B_x B_y C_x C_y : α
⊢ fx A_x B_x = C_x

α : Type,
fx fy : α → α → α,
A B C : pair α
⊢ fy A.y B.y = C.y
-/
  sorry, sorry
end

[Kevin Buzzard]

that non-ascii comma in the original post threw me for a while

[ROCKY KAMEN-RUBIO]

Kevin's twitch stream about the complex number game gives an overview of this using a locally defined complex number structure as an example.
Edit: I'm having trouble finding it on twitch and am only seeing this clip. Does anyone know what happened to it?
https://www.twitch.tv/kbuzzard/clip/CrepuscularSmoggyCroissantPeanutButterJellyTime

[Kevin Buzzard]

Try the Xena project YouTube channel. NB if anyone has any ideas about how to set up a YouTube channel I'd be interested to hear them

[Jalex Stark]

@Kevin Buzzard if you kick twitch $5/month, they'll keep your videos for 90 days instead of 14 days (I don't have advice about youtube, but this will buy some time so that getting the details of the youtube channel correct isn't critical right now)

[ROCKY KAMEN-RUBIO]

The channel seems to be stable and have the complete stream. Here's a link if anyone's interested https://www.youtube.com/watch?v=OEZCp63GES8