# Zulip Chat Archive

## Stream: new members

### Topic: composite of injectives

#### Jakob Scholbach (Jan 31 2021 at 14:45):

I am working through §3 of the mathematics in lean tutorial. I am stuck with the composition of injectivity.

```
open function
-- BEGIN
variables {α : Type*} {β : Type*} {γ : Type*}
variables {g : β → γ} {f : α → β}
example (injg : injective g) (injf : injective f) :
injective (λ x, g (f x)) :=
begin
intro x1,
intro x2,
dsimp,
apply injg (injf),
end
```

I am not quite able to find the right syntax for saying : apply injg to f(x1) and f(x2 (in the last line of the proof). How is this done? Thanks!

#### Adam Topaz (Jan 31 2021 at 14:55):

You can apply them separately

#### Adam Topaz (Jan 31 2021 at 15:03):

Oh you probably need to introduce another thing, saying that `g (f x1) = g (f x2)`

, with the goal `x1 = x2`

. Then you can apply `injf`

, then apply `injg`

, etc

#### Patrick Massot (Jan 31 2021 at 15:35):

Yes, if you want to do it fully backward then:

```
example (injg : injective g) (injf : injective f) :
injective (λ x, g (f x)) :=
begin
intro x1,
intro x2,
intro h,
apply injf,
apply injg,
exact h,
end
```

#### Patrick Massot (Jan 31 2021 at 15:39):

I don't know how much was explained in MIL at the point you are reading, but note that nothing in Lean forces you to write such an inscrutable proof script that looks like nothing you would write on paper. You can perfectly write:

```
example (injg : injective g) (injf : injective f) :
injective (λ x, g (f x)) :=
begin
assume (x₁ x₂ : α) (h : g (f x₁) = g (f x₂)),
show x₁ = x₂,
have fact : f x₁ = f x₂, from injg h,
exact injf fact,
end
```

#### Kevin Buzzard (Jan 31 2021 at 15:56):

Alternatively you can go full inscrutable:

```
open function
-- BEGIN
variables {α : Type*} {β : Type*} {γ : Type*}
variables {g : β → γ} {f : α → β}
example (injg : injective g) (injf : injective f) :
injective (λ x, g (f x)) :=
λ x₁ x₂ h, injf $ injg h
```

#### Kevin Buzzard (Jan 31 2021 at 15:57):

This way makes it clearer that a proof is just a function.

#### Eric Wieser (Jan 31 2021 at 16:04):

Nah, I think full inscrutable is

```
example (injg : injective g) (injf : injective f) :
injective (g ∘ f) :=
λ x₁ x₂, @@injf ∘ @@injg
```

#### Jakob Scholbach (Jan 31 2021 at 19:24):

Ah, thanks -- I was missing the `exact h`

in Patrick's solution. It is nice to know that there are less readable :) versions of this, too. I am currently at the level where I try to write down the proof as slowly as possible, because it gives me more safety what the prover does at each point. In the lambda-calculus notation I find it much less clear what is going on, so at best I am able to compress a several-lines-proof a posteriori into a single-line-proof.

#### Kevin Buzzard (Jan 31 2021 at 19:28):

`λ x₁ x₂ h, injf $ injg h`

, known less brutally as `λ x₁ x₂ h, injf (injg h)`

, is a proof that $g\circ f$ is injective. Here's how to read it. It is supposed to be a function which takes three inputs, namely two elements $x_1$ and $x_2$ of $\alpha$ and a proof `h`

that $g(f(x_1))=g(f(x_2))$, and spits out a proof that $x_1=x_2$ (proofs and elements are both "things" in type theory, so functions can eat proofs as well as elements). So the claim now is that `injf (injg h)`

is a proof that $x_1=x_2$. And you can see that it is: `injg`

is a function which takes in a proof that $g(a)=g(b)$ and returns a proof that $a=b$, and so `injg h`

is a proof that $f(x_1)=f(x_2)$. And `injf`

takes a proof that $f(x_1)=f(x_2)$ and returns a proof that $x_1=x_2$.

#### Kevin Buzzard (Jan 31 2021 at 19:31):

Note also that Patrick's tactic proof literally just reads the terms in `λ x₁ x₂ h, injf (injg h)`

, in that order, so it is just literally building the function piece by piece. This is why the "backwards" argument (using injectivity of `f`

before injectivity of `g`

) is so natural to computer scientists, because that's how they build the function.

Last updated: May 16 2021 at 05:21 UTC