Theorem: Tutorial.Injective.comp (Solution/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:
apply hfinj
State after:
case a
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₂
⊢ f x₁ = f x₂

State before:
case a
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₂
⊢ f x₁ = f x₂
Tactic:
apply hf
State after:
no goals