[GOAL]
C : Type ?u.30361
inst✝ : Category.{?u.30362, ?u.30361} C
X Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f
[PROOFSTEP]
simp
[GOAL]
C : Type ?u.30529
inst✝ : Category.{?u.30530, ?u.30529} C
X Y : C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : f = g
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h
[PROOFSTEP]
rw [w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
w : g = h
⊢ f ≫ g = f ≫ h
[PROOFSTEP]
rw [w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = g
[PROOFSTEP]
convert w (𝟙 Y)
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = f ≫ 𝟙 Y
[PROOFSTEP]
aesop
[GOAL]
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ g = g ≫ 𝟙 Y
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : Y ⟶ Z
w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
⊢ f = g
[PROOFSTEP]
convert w (𝟙 Y)
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : Y ⟶ Z
w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
⊢ f = 𝟙 Y ≫ f
[PROOFSTEP]
aesop
[GOAL]
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : Y ⟶ Z
w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
⊢ g = 𝟙 Y ≫ g
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z✝ : C
f g : X ⟶ Y
w : (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h
[PROOFSTEP]
convert congr_fun (congr_fun w Z) h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f g : Y ⟶ Z
w : (fun {X} h => h ≫ f) = fun {X} h => h ≫ g
X : C
h : X ⟶ Y
⊢ h ≫ f = h ≫ g
[PROOFSTEP]
convert congr_fun (congr_fun w X) h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = 𝟙 X
[PROOFSTEP]
convert w (𝟙 X)
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
⊢ f = 𝟙 X
[PROOFSTEP]
convert w (𝟙 X)
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
g : Y ⟶ Z
⊢ (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z X Z✝ : C
g h : X ⟶ Z✝
w : 𝟙 X ≫ g = 𝟙 X ≫ h
⊢ g = h
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z X Z✝ : C
g h : Z✝ ⟶ X
w : g ≫ 𝟙 X = h ≫ 𝟙 X
⊢ g = h
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f ≫ h = f ↔ h = 𝟙 Y
[PROOFSTEP]
convert cancel_epi f
[GOAL]
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
g : X ⟶ X
⊢ g ≫ f = f ↔ g = 𝟙 X
[PROOFSTEP]
convert cancel_mono f
[GOAL]
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
g : X ⟶ X
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z
inst✝ : Epi g
⊢ Epi (f ≫ g)
[PROOFSTEP]
constructor
[GOAL]
case left_cancellation
C : Type u
inst✝² : Category.{v, u} 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
[PROOFSTEP]
intro Z a b w
[GOAL]
case left_cancellation
C : Type u
inst✝² : Category.{v, u} 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
[PROOFSTEP]
apply (cancel_epi g).1
[GOAL]
case left_cancellation
C : Type u
inst✝² : Category.{v, u} 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
[PROOFSTEP]
apply (cancel_epi f).1
[GOAL]
case left_cancellation
C : Type u
inst✝² : Category.{v, u} 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
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z
inst✝ : Mono g
⊢ Mono (f ≫ g)
[PROOFSTEP]
constructor
[GOAL]
case right_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z
inst✝ : Mono g
⊢ ∀ {Z_1 : C} (g_1 h : Z_1 ⟶ X), g_1 ≫ f ≫ g = h ≫ f ≫ g → g_1 = h
[PROOFSTEP]
intro Z a b w
[GOAL]
case right_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z✝
inst✝ : Mono g
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ a = b
[PROOFSTEP]
apply (cancel_mono f).1
[GOAL]
case right_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z✝
inst✝ : Mono g
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ a ≫ f = b ≫ f
[PROOFSTEP]
apply (cancel_mono g).1
[GOAL]
case right_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z✝
inst✝ : Mono g
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ (a ≫ f) ≫ g = (b ≫ f) ≫ g
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ Mono f
[PROOFSTEP]
constructor
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} 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
[PROOFSTEP]
intro Z a b w
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} 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
[PROOFSTEP]
replace w := congr_arg (fun k => k ≫ g) w
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} 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
[PROOFSTEP]
dsimp at w 
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} 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
[PROOFSTEP]
rw [Category.assoc, Category.assoc] at w 
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} 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
[PROOFSTEP]
exact (cancel_mono _).1 w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Mono h
w : f ≫ g = h
⊢ Mono f
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ Mono f
[PROOFSTEP]
exact mono_of_mono f g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g
[PROOFSTEP]
constructor
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ ∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), g ≫ g_1 = g ≫ h → g_1 = h
[PROOFSTEP]
intro Z a b w
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Epi (f ≫ g)
Z : C
a b : Z✝ ⟶ Z
w : g ≫ a = g ≫ b
⊢ a = b
[PROOFSTEP]
replace w := congr_arg (fun k => f ≫ k) w
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Epi (f ≫ g)
Z : C
a b : Z✝ ⟶ Z
w : (fun k => f ≫ k) (g ≫ a) = (fun k => f ≫ k) (g ≫ b)
⊢ a = b
[PROOFSTEP]
dsimp at w 
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Epi (f ≫ g)
Z : C
a b : Z✝ ⟶ Z
w : f ≫ g ≫ a = f ≫ g ≫ b
⊢ a = b
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc] at w 
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Epi (f ≫ g)
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ a = b
[PROOFSTEP]
exact (cancel_epi _).1 w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Epi h
w : f ≫ g = h
⊢ Epi g
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g
[PROOFSTEP]
exact epi_of_epi f g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ LargeCategory (ULift D)
[PROOFSTEP]
infer_instance
