case left_cancellation
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z
inst✝ : Epi g
⊢ ∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), (f ≫ g) ≫ g_1 = (f ≫ g) ≫ h → g_1 = h
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z
inst✝ : Epi g
⊢ Epi (f ≫ g)
constructor
case left_cancellation
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ a = b
case left_cancellation
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z
inst✝ : Epi g
⊢ ∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), (f ≫ g) ≫ g_1 = (f ≫ g) ≫ h → g_1 = h
intro Z a b w
case left_cancellation
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ g ≫ a = g ≫ b
case left_cancellation
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ a = b
apply (cancel_epi g).1
case left_cancellation
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ f ≫ g ≫ a = f ≫ g ≫ b
case left_cancellation
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ g ≫ a = g ≫ b
apply (cancel_epi f).1
no goals
case left_cancellation
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ f ≫ g ≫ a = f ≫ g ≫ b
simpa using w