Theorem: Section3sheet1solutions.gf_injective (FormalisingMathematics2024/Solutions/Section03functions/Sheet3.lean)

State before:
⊢ Injective (g ∘ f)
Tactic:
rintro ⟨_⟩ ⟨_⟩ _
State after:
case a.a
a✝ : (g ∘ f) X.a = (g ∘ f) X.a
⊢ X.a = X.a

State before:
case a.a
a✝ : (g ∘ f) X.a = (g ∘ f) X.a
⊢ X.a = X.a
Tactic:
rfl
State after:
no goals