# Zulip Chat Archive

## Stream: new members

### Topic: cases under equality

#### Pedro Minicz (Mar 03 2021 at 20:16):

What is the name of the tactic that turns goals of the form `(a, b) = (c, d)`

into goals of the form `a = c`

and `b = d`

? I know a generic tactic that does this and that works for any constructor exists, but I forgot its name.

#### Pedro Minicz (Mar 03 2021 at 20:16):

I had no luck finding it on the documentation thus far.

#### Kevin Buzzard (Mar 03 2021 at 20:16):

extensionality -- `ext`

. It's a general principle that says that objects are equal if they have the same "external properties" (e.g. in your case, the same first and second elements) even if they have been defined in different ways. https://en.wikipedia.org/wiki/Extensionality . An example of when you might not want to consider two extensionally equal objects to be equal would be two sorting algorithms, which might have different run times, but which both do the same thing to the same input.

#### Yakov Pechersky (Mar 03 2021 at 20:18):

Or `congr`

in this particular case too

#### Pedro Minicz (Mar 03 2021 at 20:20):

Oh, `congr`

(or `ext`

) is exactly what I was looking for. I guess forgetting this stuff is what happens when you take a few months break from lean. Thanks everyone!

#### Pedro Minicz (Mar 03 2021 at 20:36):

Knowing the tactic name was all I needed to finish my first small proof in the last few months.

```
import tactic
-- https://www.youtube.com/watch?v=l1FCXUi6Vlw
namespace yoneda
class functor (f : Type → Type) : Type 1 :=
(map : ∀ {α β : Type}, (α → β) → f α → f β)
(id_map : ∀ {α : Type}, map (id : α → α) = id)
(comp_map : ∀ {α β γ : Type} (g : α → β) (h : β → γ), map h ∘ map g = map (h ∘ g))
open yoneda.functor
class natural_transformation (f : Type → Type) (g : Type → Type) [functor f] [functor g] :=
(app : ∀ (α : Type), f α → g α)
(naturality : ∀ {α β : Type} (h : α → β), map h ∘ app α = app β ∘ map h)
open natural_transformation
@[reducible] def reader (ρ α : Type) : Type := ρ → α
instance {ρ : Type} : functor (reader ρ) :=
begin
refine { map := _, id_map := _, comp_map := _ },
{ intros α β f g, exact f ∘ g },
{ intros α, ext, simp },
{ intros α β γ g h, ext, simp }
end
def yoneda (f : Type → Type) [functor f] (α : Type) := natural_transformation (reader α) f
lemma yoneda_lemma (f : Type → Type) [functor f] (α : Type) : yoneda f α ≃ f α :=
begin
refine { to_fun := _, inv_fun := _, left_inv := _, right_inv := _ },
{ intro η,
apply η.app,
unfold reader,
apply id },
{ intro x,
refine { app := _, naturality := _ },
{ intros β g, exact map g x },
{ intros β γ g,
ext y,
rw [function.comp_app, function.comp_app],
rw [←function.comp_app (map g), yoneda.functor.comp_map],
refl } },
{ intros η,
cases η,
congr,
ext β g,
have h := η_naturality g,
simp [←function.comp_app (map g), h, map] },
{ intros x,
simp [yoneda.functor.id_map] }
end
end yoneda
```

#### Yakov Pechersky (Mar 03 2021 at 21:59):

Should `yoneda_lemma`

be a `def`

since an `equiv`

is data?

```
import tactic
-- https://www.youtube.com/watch?v=l1FCXUi6Vlw
namespace yoneda
class functor (f : Type → Type) : Type 1 :=
(map : ∀ {α β : Type}, (α → β) → f α → f β)
(id_map : ∀ {α : Type}, map (id : α → α) = id)
(comp_map : ∀ {α β γ : Type} (g : α → β) (h : β → γ), map h ∘ map g = map (h ∘ g))
open yoneda.functor
structure natural_transformation (f : Type → Type) (g : Type → Type) [functor f] [functor g] :=
(app : ∀ (α : Type), f α → g α)
(naturality : ∀ {α β : Type} (h : α → β), map h ∘ app α = app β ∘ map h)
open natural_transformation
@[reducible] def reader (ρ α : Type) : Type := ρ → α
instance {ρ : Type} : functor (reader ρ) :=
{ map := λ _ _, (∘),
id_map := λ _, rfl,
comp_map := λ _ _ _ _ _, rfl }
def yoneda (f : Type → Type) [functor f] (α : Type) := natural_transformation (reader α) f
def yoneda_lemma (f : Type → Type) [functor f] (α : Type) : yoneda f α ≃ f α :=
{ to_fun := λ η, η.app _ id,
inv_fun := λ x, { app := λ _, flip map x, naturality := λ _ _ _, by {
ext,
dsimp [flip],
rw [←function.comp_app (map _), functor.comp_map],
refl } },
left_inv := λ ⟨_, natur⟩, by {
dsimp [flip],
congr,
ext,
simp [←function.comp_app (map _), natur, map] },
right_inv := λ _, by simp [flip, functor.id_map] }
end yoneda
```

#### Scott Morrison (Mar 03 2021 at 22:05):

Yakov Pechersky said:

Should

`yoneda_lemma`

be a`def`

since an`equiv`

is data?

Yes. In the library `yoneda_lemma`

is this equivalence, bundled with the fact that it is natural with respect to both `f`

and `α`

. If you used `lemma`

here instead of `def`

it wouldn't be possible to even state naturality.

#### Eric Wieser (Mar 03 2021 at 22:25):

Is tactic#injection related to the original question?

#### Eric Wieser (Mar 03 2021 at 22:25):

Ah, that for hypotheses not goals

Last updated: May 15 2021 at 23:13 UTC