Theorem: Tutorial.Injective.of_comp (Tutorial/Basic/Lecture4.lean)

State before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
⊢ Injective f
Tactic:
rw [Injective]
State after:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
⊢ ∀ {x₁ x₂ : X}, f x₁ = f x₂ → x₁ = x₂

State before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
⊢ ∀ {x₁ x₂ : X}, f x₁ = f x₂ → x₁ = x₂
Tactic:
intro x₁ x₂ hf
State after:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
⊢ x₁ = x₂

State before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
⊢ x₁ = x₂
Tactic:
have h : g (f x₁) = g (f x₂) := by
  sorry
State after:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ x₁ = x₂

State before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ x₁ = x₂
Tactic:
sorry
State after:
no goals

State before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
⊢ g (f x₁) = g (f x₂)
Tactic:
sorry
State after:
no goals