Theorem: gf_injective (FM2023Exrcise/section03_functions/sheet3.lean)

State before:
⊢ Injective (g ∘ f)
Tactic:
rw [Injective]
State after:
⊢ ∀ ⦃a₁ a₂ : X⦄, (g ∘ f) a₁ = (g ∘ f) a₂ → a₁ = a₂

State before:
⊢ ∀ ⦃a₁ a₂ : X⦄, (g ∘ f) a₁ = (g ∘ f) a₂ → a₁ = a₂
Tactic:
intro x₁ x₂ hgf
State after:
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
⊢ x₁ = x₂

State before:
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
⊢ x₁ = x₂
Tactic:
cases x₁
State after:
case a
x₂ : X
hgf : (g ∘ f) X.a = (g ∘ f) x₂
⊢ X.a = x₂

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

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