## 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

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,
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

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