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

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

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

State before:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
⊢ x₁ = x₂
Tactic:
have hf := hginj hgf
State after:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
hf : f x₁ = f x₂
⊢ x₁ = x₂

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