Challenge 7: The composition of injective functions is injective
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