case mp
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
a✝ : StrongMono f
⊢ StrongMono g

case mpr
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
a✝ : StrongMono g
⊢ StrongMono f
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
⊢ StrongMono f ↔ StrongMono g
constructor <;> intro
no goals
case mp
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
a✝ : StrongMono f
⊢ StrongMono g

case mpr
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
a✝ : StrongMono g
⊢ StrongMono f
exacts [StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]