[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
g h : Over Y
k : g ⟶ h
⊢ (pullback.fst ≫ k.left) ≫ h.hom = pullback.snd ≫ f
[PROOFSTEP]
simp [pullback.condition]
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ (map f).obj g ⟶ h
[PROOFSTEP]
refine' Over.homMk _ _
[GOAL]
case refine'_1
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ((map f).obj g).left ⟶ h.left
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ?refine'_1 ≫ h.hom = ((map f).obj g).hom
[PROOFSTEP]
refine' Y.left ≫ pullback.fst
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ (Y.left ≫ pullback.fst) ≫ h.hom = ((map f).obj g).hom
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ (Y.left ≫ pullback.fst) ≫ h.hom = g.hom ≫ f
[PROOFSTEP]
rw [← Over.w Y, Category.assoc, pullback.condition, Category.assoc]
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ Y.left ≫ pullback.snd ≫ f = Y.left ≫ ((pullback f).obj h).hom ≫ f
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
X : (map f).obj g ⟶ h
⊢ (fun Y => homMk (Y.left ≫ pullback.fst))
      ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom))) X) =
    X
[PROOFSTEP]
ext
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
X : (map f).obj g ⟶ h
⊢ ((fun Y => homMk (Y.left ≫ pullback.fst))
        ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom))) X)).left =
    X.left
[PROOFSTEP]
dsimp
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
X : (map f).obj g ⟶ h
⊢ pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom) ≫ pullback.fst = X.left
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ (fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom)))
      ((fun Y => homMk (Y.left ≫ pullback.fst)) Y) =
    Y
[PROOFSTEP]
apply OverMorphism.ext
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom)))
        ((fun Y => homMk (Y.left ≫ pullback.fst)) Y)).left =
    Y.left
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h.h₀
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom)))
          ((fun Y => homMk (Y.left ≫ pullback.fst)) Y)).left ≫
      pullback.fst =
    Y.left ≫ pullback.fst
[PROOFSTEP]
dsimp
[GOAL]
case h.h₀
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ pullback.lift (Y.left ≫ pullback.fst) g.hom (_ : (homMk (Y.left ≫ pullback.fst)).left ≫ h.hom = ((map f).obj g).hom) ≫
      pullback.fst =
    Y.left ≫ pullback.fst
[PROOFSTEP]
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
[GOAL]
case h.h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom)))
          ((fun Y => homMk (Y.left ≫ pullback.fst)) Y)).left ≫
      pullback.snd =
    Y.left ≫ pullback.snd
[PROOFSTEP]
dsimp
[GOAL]
case h.h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ pullback.lift (Y.left ≫ pullback.fst) g.hom (_ : (homMk (Y.left ≫ pullback.fst)).left ≫ h.hom = ((map f).obj g).hom) ≫
      pullback.snd =
    Y.left ≫ pullback.snd
[PROOFSTEP]
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, ← Over.w Y]
[GOAL]
case h.h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ Y.left ≫ ((pullback f).obj h).hom = Y.left ≫ pullback.snd
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPushouts C
X Y : C
f : X ⟶ Y
g h : Under X
k : g ⟶ h
⊢ g.hom ≫ k.right ≫ pushout.inl = f ≫ pushout.inr
[PROOFSTEP]
simp [← pushout.condition]
