Theorem: Section3sheet1.gf_injective (FormalisingMathematics2024/Section03functions/Sheet3.lean)

State before:
⊢ Injective (g ∘ f)
Tactic:
sorry
State after:
no goals