-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem strongMono_of_strongMono [StrongMono (f ≫ g)] : StrongMono f :=
  { mono := mono_of_mono f g
    rlp := fun {X Y} z => by
      intros
      constructor
      intro u v sq
      have h₀ : u ≫ f ≫ g = z ≫ v ≫ g

Proof state:
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ sq.HasLift

Tactic:
exact CommSq.HasLift.mk' ⟨(CommSq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩

Result:
no goals

Proof state:
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ ∀ {f_1 : X ⟶ P} {g : Y ⟶ Q} (sq : CommSq f_1 z f g), sq.HasLift

Tactic:
intro u v sq

Result:
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
⊢ sq.HasLift

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
⊢ u ≫ f ≫ g = z ≫ v ≫ g

Tactic:
rw [← Category.assoc, eq_whisker sq.w, Category.assoc]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ HasLiftingProperty z f

Tactic:
constructor

Result:
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ ∀ {f_1 : X ⟶ P} {g : Y ⟶ Q} (sq : CommSq f_1 z f g), sq.HasLift

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ z ≫ ⋯.lift = u

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
⊢ ∀ [inst : Epi z], HasLiftingProperty z f

Tactic:
intros

Result:
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ HasLiftingProperty z f

Proof state:
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
⊢ sq.HasLift

Tactic:
have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by
  rw [← Category.assoc, eq_whisker sq.w, Category.assoc]

Result:
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ sq.HasLift

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ ⋯.lift ≫ f = v

Tactic:
simp [← cancel_epi z, sq.w]

Result:
no goals