Theorem: Tutorial.Injective.of_comp (Solution/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
   rw [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₂
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:
apply hgfinj
State after:
case a
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₂)
⊢ (g ∘ f) x₁ = (g ∘ f) x₂

State before:
case a
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₂)
⊢ (g ∘ f) x₁ = (g ∘ f) x₂
Tactic:
simp
State after:
case a
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₂)
⊢ g (f x₁) = g (f x₂)

State before:
case a
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₂)
⊢ g (f x₁) = g (f x₂)
Tactic:
apply h
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:
rw [hf]
State after:
no goals