case sq_hasLift
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ ∀ {f : Q ⟶ X} {g_1 : R ⟶ Y} (sq : CommSq f g z g_1), CommSq.HasLift sq
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ HasLiftingProperty g z
constructor
case sq_hasLift
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ CommSq.HasLift sq
case sq_hasLift
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ ∀ {f : Q ⟶ X} {g_1 : R ⟶ Y} (sq : CommSq f g z g_1), 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✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ CommSq.HasLift sq
case sq_hasLift
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ CommSq.HasLift sq
have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
no goals
case sq_hasLift
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ CommSq.HasLift sq
exact
  CommSq.HasLift.mk'
    ⟨(CommSq.mk h₀).lift, by
      simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩
no goals
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ (f ≫ u) ≫ z = (f ≫ g) ≫ v
simp only [Category.assoc, sq.w]
no goals
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ g ≫ CommSq.lift (_ : CommSq (f ≫ u) (f ≫ g) z v) = u
simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w]
no goals
C : Type u
inst✝¹ : Category C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ CommSq.lift (_ : CommSq (f ≫ u) (f ≫ g) z v) ≫ z = v
simp