case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ Mono f
constructor
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : a ≫ f = b ≫ f
⊢ a = b
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
intro Z a b w
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : (fun k => k ≫ g) (a ≫ f) = (fun k => k ≫ g) (b ≫ f)
⊢ a = b
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : a ≫ f = b ≫ f
⊢ a = b
replace w := congr_arg (fun k => k ≫ g) w
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : (a ≫ f) ≫ g = (b ≫ f) ≫ g
⊢ a = b
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : (fun k => k ≫ g) (a ≫ f) = (fun k => k ≫ g) (b ≫ f)
⊢ a = b
dsimp at w
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ a = b
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : (a ≫ f) ≫ g = (b ≫ f) ≫ g
⊢ a = b
rw [Category.assoc, Category.assoc] at w
no goals
case right_cancellation
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ a = b
exact (cancel_mono _).1 w