C : Type u
inst✝² : Category 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
C : Type u
inst✝¹ : Category 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
intros
case sq_hasLift
C : Type u
inst✝² : Category 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), CommSq.HasLift sq
C : Type u
inst✝² : Category 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
constructor
case sq_hasLift
C : Type u
inst✝² : Category 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
⊢ CommSq.HasLift sq
case sq_hasLift
C : Type u
inst✝² : Category 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), CommSq.HasLift sq
intro u v sq
case sq_hasLift
C : Type u
inst✝² : Category 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
⊢ CommSq.HasLift sq
case sq_hasLift
C : Type u
inst✝² : Category 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
⊢ CommSq.HasLift sq
have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by
  rw [←Category.assoc, eq_whisker sq.w, Category.assoc]
no goals
case sq_hasLift
C : Type u
inst✝² : Category 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
⊢ CommSq.HasLift sq
exact CommSq.HasLift.mk' ⟨(CommSq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩
no goals
C : Type u
inst✝² : Category 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
rw [←Category.assoc, eq_whisker sq.w, Category.assoc]
no goals
C : Type u
inst✝² : Category 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 ≫ CommSq.lift (_ : CommSq u z (f ≫ g) (v ≫ g)) = u
simp
no goals
C : Type u
inst✝² : Category 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
⊢ CommSq.lift (_ : CommSq u z (f ≫ g) (v ≫ g)) ≫ f = v
simp [← cancel_epi z, sq.w]