C : Type u
inst✝ : Category C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono (e.inv.left ≫ f ≫ e.hom.right)
C : Type u
inst✝ : Category C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono g
rw [Arrow.iso_w' e]
C : Type u
inst✝ : Category C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
this : Mono (f ≫ e.hom.right)
⊢ Mono (e.inv.left ≫ f ≫ e.hom.right)
C : Type u
inst✝ : Category C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono (e.inv.left ≫ f ≫ e.hom.right)
haveI := mono_comp f e.hom.right
no goals
C : Type u
inst✝ : Category C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
this : Mono (f ≫ e.hom.right)
⊢ Mono (e.inv.left ≫ f ≫ e.hom.right)
apply mono_comp
C : Type u
inst✝¹ : Category C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ HasLiftingProperty z g
C : Type u
inst✝ : Category C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
⊢ ∀ [inst : Epi z], HasLiftingProperty z g
intro
no goals
C : Type u
inst✝¹ : Category C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ HasLiftingProperty z g
apply HasLiftingProperty.of_arrow_iso_right z e