## 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)) :=

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