If f ∘ f is bijective, then f is bijective
Prove that if \(f ∘ f\) is bijective, then \(f\) is bijective.
To do this, complete the following Lean4 theory:
import Mathlib.Tactic open Function variable {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} example (f : X → X) (h : Bijective (f ∘ f)) : Bijective f := by sorry