Skip to main content

Challenge 7: The composition of injective functions is injective

Also available in:

Español

Prove that the composition of injective functions is injective.

To do so, complete the following Lean 4 theory:

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by sorry

1. Proofs in natural language (NL)

Proof 1 in NL

We have to prove that \[ (∀ x, y) [(g ∘ f)(x) = (g ∘ f)(y) → x = y] \] Let \(x\), \(y\) be such that \[ (g ∘ f)(x) = (g ∘ f)(y) \tag{1} \] and we have to prove that \[ x = y \tag{2} \] The goal (2), using that \(f\) is injective, reduces to \[ f(x) = f(y) \] which, using that \(g\) is injective, reduces to \[ g(f(x)) = g(f(y)) \] which, by the definition of composition, coincides with (1).

Proof 2 in NL

We have to prove that \[ (∀ x, y) [(g ∘ f)(x) = (g ∘ f)(y) → x = y] \] Let \(x\), \(y\) be such that \[ (g ∘ f)(x) = (g ∘ f)(y) \] Then, by the definition of composition, \[ g(f(x)) = g(f(y)) \] and, since \(g\) is injective, \[ f(x) = f(y) \] and, since \(f\) is injective, \[ x = y \]

2. Proofs in Lean 4

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

-- Proof 1 (based on Proof 1 in NL)
-- ================================

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by
  intros x y h
  -- x y : α
  -- h : (g ∘ f) x = (g ∘ f) y
  -- ⊢ x = y
  apply hf
  -- ⊢ f x = f y
  apply hg
  -- ⊢ g (f x) = g (f y)
  exact h

-- Proof 2
-- =======

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by
  intros x y h
  -- x y : α
  -- h : (g ∘ f) x = (g ∘ f) y
  -- ⊢ x = y
  apply hf
  -- ⊢ f x = f y
  apply hg h

-- Proof 3
-- =======

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by
  intros x y h
  -- x y : α
  -- h : (g ∘ f) x = (g ∘ f) y
  -- ⊢ x = y
  exact hf (hg h)

-- Proof 4
-- =======

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
fun _ _ h => hf (hg h)

-- Proof 5 (based on Proof 2 in NL)
-- ================================

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by
  intro x y h1
  -- x y : α
  -- h1 : (g ∘ f) x = (g ∘ f) y
  -- ⊢ x = y
  have h2 : g (f x) = g (f y) := h1
  have h3 : f x = f y := hg h2
  exact hf h3

-- Proof 6
-- =======

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by
  intro x y h1
  -- x y : α
  -- h1 : (g ∘ f) x = (g ∘ f) y
  -- ⊢ x = y
  have h3 : f x = f y := hg h1
  exact hf h3

-- Proof 7
-- =======

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by
  intro x y h
  -- x y : α
  -- h : (g ∘ f) x = (g ∘ f) y
  -- ⊢ x = y
  exact hf (hg h)

-- Proof 8
-- =======

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
fun _ _ h ↦ hf (hg h)

-- Proof 9
-- =======

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by simp_all

-- Proof 10
-- ========

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
Injective.comp hg hf

-- Lemmas used
-- ===========

#check (Injective.comp : Injective g → Injective f → Injective (g ∘ f))

The following video explains step by step how the solutions are built:

You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.

3. Collaborative solutions

Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:

  • Write your proof in live.lean-lang.org and check that it compiles without errors.
  • Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean
   -- your proof
```

Comments