C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ (p : Subobject Y), (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
p : Subobject Y
⊢ (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
revert p
case h
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ (a : MonoOver Y),
    (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ (p : Subobject Y), (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
apply Quotient.ind'
case h
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
case h
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ (a : MonoOver Y),
    (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
intro a
case h.a
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
case h
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
apply Quotient.sound
case h.a.f
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)

case h.a.g
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)
case h.a
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
apply ThinSkeleton.equiv_of_both_ways
case h.a.f
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom =
    MonoOver.arrow ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)) ≫ k
case h.a.f
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
refine' MonoOver.homMk (pullback.lift pullback.fst _ _) (pullback.lift_snd _ _ _)
case h.a.f
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ MonoOver.arrow a ≫ h = (pullback.snd ≫ g) ≫ k
case h.a.f
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom =
    MonoOver.arrow ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)) ≫ k
change _ ≫ a.arrow ≫ h = (pullback.snd ≫ g) ≫ _
no goals
case h.a.f
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ MonoOver.arrow a ≫ h = (pullback.snd ≫ g) ≫ k
rw [assoc, ← comm, pullback.condition_assoc]
case h.a.g.refine'_1
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) ≫ h = pullback.snd ≫ k

case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.lift pullback.fst
        (PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd ?h.a.g.refine'_1)
        (_ :
          pullback.fst ≫ ((MonoOver.forget Y).obj a).hom =
            PullbackCone.IsLimit.lift t (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) pullback.snd ?h.a.g.refine'_1 ≫
              PullbackCone.fst (PullbackCone.mk f g comm)) ≫
      MonoOver.arrow ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)) =
    MonoOver.arrow ((MonoOver.pullback k).obj ((MonoOver.map h).obj a))
case h.a.g
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)
refine' MonoOver.homMk (pullback.lift pullback.fst
  (PullbackCone.IsLimit.lift t (pullback.fst ≫ a.arrow) pullback.snd _)
  (PullbackCone.IsLimit.lift_fst _ _ _ _).symm) _
case h.a.g.refine'_1
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ ((MonoOver.forget Y).obj a).hom ≫ h =
    pullback.fst ≫ ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom
case h.a.g.refine'_1
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) ≫ h = pullback.snd ≫ k
rw [← pullback.condition, assoc]
no goals
case h.a.g.refine'_1
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ ((MonoOver.forget Y).obj a).hom ≫ h =
    pullback.fst ≫ ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom
rfl
case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.lift pullback.fst
        (PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
          (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k))
        (_ :
          pullback.fst ≫ MonoOver.arrow a =
            PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
                (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k) ≫
              f) ≫
      pullback.snd ≫ g =
    pullback.snd
case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.lift pullback.fst
        (PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
          (_ : (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) ≫ h = pullback.snd ≫ k))
        (_ :
          pullback.fst ≫ ((MonoOver.forget Y).obj a).hom =
            PullbackCone.IsLimit.lift t (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) pullback.snd
                (_ : (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) ≫ h = pullback.snd ≫ k) ≫
              PullbackCone.fst (PullbackCone.mk f g comm)) ≫
      MonoOver.arrow ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)) =
    MonoOver.arrow ((MonoOver.pullback k).obj ((MonoOver.map h).obj a))
dsimp
case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
        (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k) ≫
      g =
    pullback.snd
case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.lift pullback.fst
        (PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
          (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k))
        (_ :
          pullback.fst ≫ MonoOver.arrow a =
            PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
                (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k) ≫
              f) ≫
      pullback.snd ≫ g =
    pullback.snd
rw [pullback.lift_snd_assoc]
no goals
case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
        (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k) ≫
      g =
    pullback.snd
apply PullbackCone.IsLimit.lift_snd