[GOAL]
C : Type u_1
inst✝² : Category.{?u.6892, u_1} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasPullback f f
inst✝ : Mono f
⊢ IsIso (diagonal f)
[PROOFSTEP]
rw [(IsIso.inv_eq_of_inv_hom_id (diagonal_fst f)).symm]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.6892, u_1} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasPullback f f
inst✝ : Mono f
⊢ IsIso (inv fst)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.9281, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f
[PROOFSTEP]
simp [condition]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.9281, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f
[PROOFSTEP]
simp [condition]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd ≫ fst ≫ i₁ ≫ fst = fst
[PROOFSTEP]
conv_rhs => rw [← Category.comp_id pullback.fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
| fst
[PROOFSTEP]
rw [← Category.comp_id pullback.fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
| fst
[PROOFSTEP]
rw [← Category.comp_id pullback.fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
| fst
[PROOFSTEP]
rw [← Category.comp_id pullback.fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd ≫ fst ≫ i₁ ≫ fst = fst ≫ 𝟙 X
[PROOFSTEP]
rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.280786, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f
[PROOFSTEP]
simp [condition]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.280786, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f
[PROOFSTEP]
simp [condition]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd ≫ snd ≫ i₂ ≫ fst = fst
[PROOFSTEP]
conv_rhs => rw [← Category.comp_id pullback.fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
| fst
[PROOFSTEP]
rw [← Category.comp_id pullback.fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
| fst
[PROOFSTEP]
rw [← Category.comp_id pullback.fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
| fst
[PROOFSTEP]
rw [← Category.comp_id pullback.fst]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd ≫ snd ≫ i₂ ≫ fst = fst ≫ 𝟙 X
[PROOFSTEP]
rw [← diagonal_snd f, pullback.condition_assoc, pullback.lift_snd]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.552978, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f
[PROOFSTEP]
simp only [Category.assoc, condition]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.552978, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f
[PROOFSTEP]
simp only [Category.assoc, condition]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.552978, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (snd ≫ fst) ≫ i₁ = (snd ≫ snd) ≫ i₂
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{?u.552978, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((snd ≫ fst) ≫ i₁) ≫ fst = ((snd ≫ snd) ≫ i₂) ≫ fst
[PROOFSTEP]
simp [Category.assoc, pullback_diagonal_map_snd_fst_fst, pullback_diagonal_map_snd_snd_fst]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.552978, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((snd ≫ fst) ≫ i₁) ≫ snd = ((snd ≫ snd) ≫ i₂) ≫ snd
[PROOFSTEP]
simp [Category.assoc, pullback.condition, pullback.condition_assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.552978, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (fst ≫ i₁ ≫ fst) ≫ diagonal f =
    map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
        (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
      map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
        (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{?u.552978, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst ≫ i₁ ≫ fst) ≫ diagonal f) ≫ fst =
    (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
          (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
        map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
          (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)) ≫
      fst
[PROOFSTEP]
simp only [Category.assoc, diagonal_fst, Category.comp_id, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
  limit.lift_π_assoc, cospan_left]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.552978, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst ≫ i₁ ≫ fst) ≫ diagonal f) ≫ snd =
    (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
          (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
        map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
          (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)) ≫
      snd
[PROOFSTEP]
simp only [condition_assoc, Category.assoc, diagonal_snd, Category.comp_id, limit.lift_π, PullbackCone.mk_pt,
  PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_right]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ fst = snd ≫ fst
[PROOFSTEP]
delta pullbackDiagonalMapIso
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (Iso.mk (lift (snd ≫ fst) (snd ≫ snd) (_ : (snd ≫ fst) ≫ i₁ = (snd ≫ snd) ≫ i₂))
          (lift (fst ≫ i₁ ≫ fst)
            (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
              (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd))
            (_ :
              (fst ≫ i₁ ≫ fst) ≫ diagonal f =
                map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
                    (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
                  map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
                    (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)))).hom ≫
      fst =
    snd ≫ fst
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ snd = snd ≫ snd
[PROOFSTEP]
delta pullbackDiagonalMapIso
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (Iso.mk (lift (snd ≫ fst) (snd ≫ snd) (_ : (snd ≫ fst) ≫ i₁ = (snd ≫ snd) ≫ i₂))
          (lift (fst ≫ i₁ ≫ fst)
            (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
              (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd))
            (_ :
              (fst ≫ i₁ ≫ fst) ≫ diagonal f =
                map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
                    (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
                  map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
                    (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)))).hom ≫
      snd =
    snd ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).inv ≫ fst = fst ≫ i₁ ≫ fst
[PROOFSTEP]
delta pullbackDiagonalMapIso
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (Iso.mk (lift (snd ≫ fst) (snd ≫ snd) (_ : (snd ≫ fst) ≫ i₁ = (snd ≫ snd) ≫ i₂))
          (lift (fst ≫ i₁ ≫ fst)
            (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
              (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd))
            (_ :
              (fst ≫ i₁ ≫ fst) ≫ diagonal f =
                map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
                    (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
                  map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
                    (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)))).inv ≫
      fst =
    fst ≫ i₁ ≫ fst
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).inv ≫ snd ≫ fst = fst
[PROOFSTEP]
delta pullbackDiagonalMapIso
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (Iso.mk (lift (snd ≫ fst) (snd ≫ snd) (_ : (snd ≫ fst) ≫ i₁ = (snd ≫ snd) ≫ i₂))
          (lift (fst ≫ i₁ ≫ fst)
            (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
              (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd))
            (_ :
              (fst ≫ i₁ ≫ fst) ≫ diagonal f =
                map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
                    (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
                  map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
                    (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)))).inv ≫
      snd ≫ fst =
    fst
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).inv ≫ snd ≫ snd = snd
[PROOFSTEP]
delta pullbackDiagonalMapIso
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (Iso.mk (lift (snd ≫ fst) (snd ≫ snd) (_ : (snd ≫ fst) ≫ i₁ = (snd ≫ snd) ≫ i₂))
          (lift (fst ≫ i₁ ≫ fst)
            (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
              (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd))
            (_ :
              (fst ≫ i₁ ≫ fst) ≫ diagonal f =
                map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
                    (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
                  map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
                    (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)))).inv ≫
      snd ≫ snd =
    snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.597947, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f
[PROOFSTEP]
simp [condition]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.597947, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f
[PROOFSTEP]
simp [condition]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (fst ≫ i₁ ≫ fst) ≫ diagonal f =
    map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
        (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
      map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
        (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst ≫ i₁ ≫ fst) ≫ diagonal f) ≫ fst =
    (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
          (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
        map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
          (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)) ≫
      fst
[PROOFSTEP]
simp [condition_assoc]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst ≫ i₁ ≫ fst) ≫ diagonal f) ≫ snd =
    (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd)
          (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd) ≫
        map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i (_ : (i₁ ≫ snd) ≫ i = (i₁ ≫ fst) ≫ f)
          (_ : (i₂ ≫ snd) ≫ i = (i₂ ≫ fst) ≫ f)) ≫
      snd
[PROOFSTEP]
simp [condition_assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).symm.hom ≫ snd =
    map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) (𝟙 V₁) (𝟙 V₂) snd (_ : i₁ ≫ snd = 𝟙 V₁ ≫ i₁ ≫ snd) (_ : i₂ ≫ snd = 𝟙 V₂ ≫ i₂ ≫ snd)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ pullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i)) ≅
    pullback f g
[PROOFSTEP]
refine' _ ≪≫ pullbackDiagonalMapIso i (𝟙 _) (f ≫ inv pullback.fst) (g ≫ inv pullback.fst) ≪≫ _
[GOAL]
case refine'_1
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ pullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i)) ≅
    pullback (diagonal i)
      (map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst) (𝟙 S)
        (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
        (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i))
[PROOFSTEP]
refine' @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 T) ((pullback.congrHom _ _).hom) (𝟙 _) _ _) ?_
[GOAL]
case refine'_1.refine'_1
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ f ≫ i = (f ≫ inv fst) ≫ snd
[PROOFSTEP]
rw [← Category.comp_id pullback.snd, ← condition, Category.assoc, IsIso.inv_hom_id_assoc]
[GOAL]
case refine'_1.refine'_2
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ g ≫ i = (g ≫ inv fst) ≫ snd
[PROOFSTEP]
rw [← Category.comp_id pullback.snd, ← condition, Category.assoc, IsIso.inv_hom_id_assoc]
[GOAL]
case refine'_1.refine'_3
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i
[PROOFSTEP]
rw [Category.comp_id, Category.id_comp]
[GOAL]
case refine'_1.refine'_4
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i) ≫ 𝟙 (diagonalObj i) =
    (congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom ≫
      map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst) (𝟙 S)
        (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
        (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i)
[PROOFSTEP]
ext
[GOAL]
case refine'_1.refine'_4.h₀
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i) ≫ 𝟙 (diagonalObj i)) ≫
      fst =
    ((congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom ≫
        map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst) (𝟙 S)
          (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
          (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i)) ≫
      fst
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_4.h₁
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i) ≫ 𝟙 (diagonalObj i)) ≫
      snd =
    ((congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom ≫
        map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst) (𝟙 S)
          (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
          (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i)) ≫
      snd
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_5
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ IsIso
    (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
      (diagonal i)
      (map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst) (𝟙 S)
        (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
        (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i))
      (𝟙 T) (congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom (𝟙 (diagonalObj i))
      (_ : diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i)
      (_ :
        map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i) ≫ 𝟙 (diagonalObj i) =
          (congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom ≫
            map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst) (𝟙 S)
              (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
              (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i)))
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_2
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ pullback (f ≫ inv fst) (g ≫ inv fst) ≅ pullback f g
[PROOFSTEP]
refine' @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) pullback.fst _ _) ?_
[GOAL]
case refine'_2.refine'_1
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (f ≫ inv fst) ≫ fst = 𝟙 X ≫ f
[PROOFSTEP]
rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
[GOAL]
case refine'_2.refine'_2
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (g ≫ inv fst) ≫ fst = 𝟙 Y ≫ g
[PROOFSTEP]
rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
[GOAL]
case refine'_2.refine'_3
C : Type u_1
inst✝⁵ : Category.{?u.611578, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ IsIso
    (map (f ≫ inv fst) (g ≫ inv fst) f g (𝟙 X) (𝟙 Y) fst (_ : (f ≫ inv fst) ≫ fst = 𝟙 X ≫ f)
      (_ : (g ≫ inv fst) ≫ fst = 𝟙 Y ≫ g))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (pullbackDiagonalMapIdIso f g i).hom ≫ fst = snd ≫ fst
[PROOFSTEP]
delta pullbackDiagonalMapIdIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (asIso
            (map (diagonal i)
              (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i)) (diagonal i)
              (map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst) (𝟙 S)
                (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
                (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i))
              (𝟙 T) (congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom
              (𝟙 (diagonalObj i)) (_ : diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i)
              (_ :
                map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i) ≫
                    𝟙 (diagonalObj i) =
                  (congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom ≫
                    map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst)
                      (𝟙 S) (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
                      (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i))) ≪≫
          pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv fst) (g ≫ inv fst) ≪≫
            asIso
              (map (f ≫ inv fst) (g ≫ inv fst) f g (𝟙 X) (𝟙 Y) fst (_ : (f ≫ inv fst) ≫ fst = 𝟙 X ≫ f)
                (_ : (g ≫ inv fst) ≫ fst = 𝟙 Y ≫ g))).hom ≫
      fst =
    snd ≫ fst
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (pullbackDiagonalMapIdIso f g i).hom ≫ snd = snd ≫ snd
[PROOFSTEP]
delta pullbackDiagonalMapIdIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (asIso
            (map (diagonal i)
              (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i)) (diagonal i)
              (map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst) (𝟙 S)
                (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
                (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i))
              (𝟙 T) (congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom
              (𝟙 (diagonalObj i)) (_ : diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i)
              (_ :
                map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i) ≫
                    𝟙 (diagonalObj i) =
                  (congrHom (_ : f ≫ i = (f ≫ inv fst) ≫ snd) (_ : g ≫ i = (g ≫ inv fst) ≫ snd)).hom ≫
                    map ((f ≫ inv fst) ≫ snd) ((g ≫ inv fst) ≫ snd) i i ((f ≫ inv fst) ≫ fst) ((g ≫ inv fst) ≫ fst)
                      (𝟙 S) (_ : ((f ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((f ≫ inv fst) ≫ fst) ≫ i)
                      (_ : ((g ≫ inv fst) ≫ snd) ≫ 𝟙 S = ((g ≫ inv fst) ≫ fst) ≫ i))) ≪≫
          pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv fst) (g ≫ inv fst) ≪≫
            asIso
              (map (f ≫ inv fst) (g ≫ inv fst) f g (𝟙 X) (𝟙 Y) fst (_ : (f ≫ inv fst) ≫ fst = 𝟙 X ≫ f)
                (_ : (g ≫ inv fst) ≫ fst = 𝟙 Y ≫ g))).hom ≫
      snd =
    snd ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫ fst = fst ≫ f
[PROOFSTEP]
rw [Iso.inv_comp_eq, ← Category.comp_id pullback.fst, ← diagonal_fst i, pullback.condition_assoc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ snd ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i) ≫ fst =
    (pullbackDiagonalMapIdIso f g i).hom ≫ fst ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫ snd ≫ fst = fst
[PROOFSTEP]
rw [Iso.inv_comp_eq]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ snd ≫ fst = (pullbackDiagonalMapIdIso f g i).hom ≫ fst
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (pullbackDiagonalMapIdIso f g i).inv ≫ snd ≫ snd = snd
[PROOFSTEP]
rw [Iso.inv_comp_eq]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ snd ≫ snd = (pullbackDiagonalMapIdIso f g i).hom ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁷ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝⁶ : HasPullback i i
inst✝⁵ : HasPullback f✝ g✝
inst✝⁴ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝³ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasPullback f f
inst✝¹ : HasPullback g g
inst✝ : HasPullback (f ≫ g) (f ≫ g)
⊢ diagonal (f ≫ g) = diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ snd
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u_1
inst✝⁸ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁷ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝⁶ : HasPullback i i
inst✝⁵ : HasPullback f✝ g✝
inst✝⁴ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝³ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasPullback f f
inst✝¹ : HasPullback g g
inst✝ : HasPullback (f ≫ g) (f ≫ g)
⊢ diagonal (f ≫ g) ≫ fst = (diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ snd) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case h₁
C : Type u_1
inst✝⁸ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁷ : HasPullbacks C
S T : C
f✝ : X ⟶ T
g✝ : Y ⟶ T
i : T ⟶ S
inst✝⁶ : HasPullback i i
inst✝⁵ : HasPullback f✝ g✝
inst✝⁴ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝³ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasPullback f f
inst✝¹ : HasPullback g g
inst✝ : HasPullback (f ≫ g) (f ≫ g)
⊢ diagonal (f ≫ g) ≫ snd = (diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ snd) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ IsPullback (fst ≫ f) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i (_ : f ≫ i = 𝟙 X ≫ f ≫ i) (_ : g ≫ i = 𝟙 Y ≫ g ≫ i))
    (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
[PROOFSTEP]
apply IsPullback.of_iso_pullback _ (pullbackDiagonalMapIdIso f g i).symm
[GOAL]
case w₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (pullbackDiagonalMapIdIso f g i).symm.hom ≫ fst = fst ≫ f
[PROOFSTEP]
simp
[GOAL]
case w₂
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i (_ : f ≫ i = 𝟙 X ≫ f ≫ i) (_ : g ≫ i = 𝟙 Y ≫ g ≫ i)
[PROOFSTEP]
ext
[GOAL]
case w₂.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ ((pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd) ≫ fst =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i (_ : f ≫ i = 𝟙 X ≫ f ≫ i) (_ : g ≫ i = 𝟙 Y ≫ g ≫ i) ≫ fst
[PROOFSTEP]
simp
[GOAL]
case w₂.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ ((pullbackDiagonalMapIdIso f g i).symm.hom ≫ snd) ≫ snd =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i (_ : f ≫ i = 𝟙 X ≫ f ≫ i) (_ : g ≫ i = 𝟙 Y ≫ g ≫ i) ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ CommSq (fst ≫ f) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i (_ : f ≫ i = 𝟙 X ≫ f ≫ i) (_ : g ≫ i = 𝟙 Y ≫ g ≫ i))
    (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
[PROOFSTEP]
constructor
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ (fst ≫ f) ≫ diagonal i =
    map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i (_ : f ≫ i = 𝟙 X ≫ f ≫ i) (_ : g ≫ i = 𝟙 Y ≫ g ≫ i) ≫
      map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i)
[PROOFSTEP]
ext
[GOAL]
case w.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ ((fst ≫ f) ≫ diagonal i) ≫ fst =
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i (_ : f ≫ i = 𝟙 X ≫ f ≫ i) (_ : g ≫ i = 𝟙 Y ≫ g ≫ i) ≫
        map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i)) ≫
      fst
[PROOFSTEP]
simp [condition]
[GOAL]
case w.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ :
  HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i))
⊢ ((fst ≫ f) ≫ diagonal i) ≫ snd =
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i (_ : f ≫ i = 𝟙 X ≫ f ≫ i) (_ : g ≫ i = 𝟙 Y ≫ g ≫ i) ≫
        map (f ≫ i) (g ≫ i) i i f g (𝟙 S) (_ : (f ≫ i) ≫ 𝟙 S = f ≫ i) (_ : (g ≫ i) ≫ 𝟙 S = g ≫ i)) ≫
      snd
[PROOFSTEP]
simp [condition]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).hom ≫ fst ≫ fst = fst ≫ snd
[PROOFSTEP]
delta diagonalObjPullbackFstIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g fst ≪≫
          congrHom (_ : fst ≫ f = snd ≫ g) (_ : g = g) ≪≫
            pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst ≫ g) ≪≫ congrHom (_ : fst ≫ g = snd ≫ g) (_ : f = f)).hom ≫
      fst ≫ fst =
    fst ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).hom ≫ fst ≫ snd = snd ≫ snd
[PROOFSTEP]
delta diagonalObjPullbackFstIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g fst ≪≫
          congrHom (_ : fst ≫ f = snd ≫ g) (_ : g = g) ≪≫
            pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst ≫ g) ≪≫ congrHom (_ : fst ≫ g = snd ≫ g) (_ : f = f)).hom ≫
      fst ≫ snd =
    snd ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).hom ≫ snd = fst ≫ fst
[PROOFSTEP]
delta diagonalObjPullbackFstIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g fst ≪≫
          congrHom (_ : fst ≫ f = snd ≫ g) (_ : g = g) ≪≫
            pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst ≫ g) ≪≫ congrHom (_ : fst ≫ g = snd ≫ g) (_ : f = f)).hom ≫
      snd =
    fst ≫ fst
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ fst ≫ fst = snd
[PROOFSTEP]
delta diagonalObjPullbackFstIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g fst ≪≫
          congrHom (_ : fst ≫ f = snd ≫ g) (_ : g = g) ≪≫
            pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst ≫ g) ≪≫ congrHom (_ : fst ≫ g = snd ≫ g) (_ : f = f)).inv ≫
      fst ≫ fst =
    snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ fst ≫ snd = fst ≫ fst
[PROOFSTEP]
delta diagonalObjPullbackFstIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g fst ≪≫
          congrHom (_ : fst ≫ f = snd ≫ g) (_ : g = g) ≪≫
            pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst ≫ g) ≪≫ congrHom (_ : fst ≫ g = snd ≫ g) (_ : f = f)).inv ≫
      fst ≫ snd =
    fst ≫ fst
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ snd ≫ fst = snd
[PROOFSTEP]
delta diagonalObjPullbackFstIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g fst ≪≫
          congrHom (_ : fst ≫ f = snd ≫ g) (_ : g = g) ≪≫
            pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst ≫ g) ≪≫ congrHom (_ : fst ≫ g = snd ≫ g) (_ : f = f)).inv ≫
      snd ≫ fst =
    snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ snd ≫ snd = fst ≫ snd
[PROOFSTEP]
delta diagonalObjPullbackFstIso
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g fst ≪≫
          congrHom (_ : fst ≫ f = snd ≫ g) (_ : g = g) ≪≫
            pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst ≫ g) ≪≫ congrHom (_ : fst ≫ g = snd ≫ g) (_ : f = f)).inv ≫
      snd ≫ snd =
    fst ≫ snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ diagonal fst =
    (pullbackSymmetry f (Over.mk g).hom).hom ≫
      ((baseChange f).map (Over.homMk (diagonal g))).left ≫ (diagonalObjPullbackFstIso f g).inv
[PROOFSTEP]
ext
[GOAL]
case h₀.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal fst ≫ fst) ≫ fst =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          ((baseChange f).map (Over.homMk (diagonal g))).left ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        fst) ≫
      fst
[PROOFSTEP]
dsimp
[GOAL]
case h₀.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal fst ≫ fst) ≫ snd =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          ((baseChange f).map (Over.homMk (diagonal g))).left ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        fst) ≫
      snd
[PROOFSTEP]
dsimp
[GOAL]
case h₁.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal fst ≫ snd) ≫ fst =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          ((baseChange f).map (Over.homMk (diagonal g))).left ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        snd) ≫
      fst
[PROOFSTEP]
dsimp
[GOAL]
case h₁.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal fst ≫ snd) ≫ snd =
    (((pullbackSymmetry f (Over.mk g).hom).hom ≫
          ((baseChange f).map (Over.homMk (diagonal g))).left ≫ (diagonalObjPullbackFstIso f g).inv) ≫
        snd) ≫
      snd
[PROOFSTEP]
dsimp
[GOAL]
case h₀.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal fst ≫ fst) ≫ fst =
    (((pullbackSymmetry f g).hom ≫
          map g f (snd ≫ g) f (diagonal g) (𝟙 X) (𝟙 Z)
              (_ : (Over.mk g).hom ≫ 𝟙 Z = (Over.homMk (diagonal g)).left ≫ (Over.mk (snd ≫ g)).hom)
              (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) ≫
            (diagonalObjPullbackFstIso f g).inv) ≫
        fst) ≫
      fst
[PROOFSTEP]
simp
[GOAL]
case h₀.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal fst ≫ fst) ≫ snd =
    (((pullbackSymmetry f g).hom ≫
          map g f (snd ≫ g) f (diagonal g) (𝟙 X) (𝟙 Z)
              (_ : (Over.mk g).hom ≫ 𝟙 Z = (Over.homMk (diagonal g)).left ≫ (Over.mk (snd ≫ g)).hom)
              (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) ≫
            (diagonalObjPullbackFstIso f g).inv) ≫
        fst) ≫
      snd
[PROOFSTEP]
simp
[GOAL]
case h₁.h₀
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal fst ≫ snd) ≫ fst =
    (((pullbackSymmetry f g).hom ≫
          map g f (snd ≫ g) f (diagonal g) (𝟙 X) (𝟙 Z)
              (_ : (Over.mk g).hom ≫ 𝟙 Z = (Over.homMk (diagonal g)).left ≫ (Over.mk (snd ≫ g)).hom)
              (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) ≫
            (diagonalObjPullbackFstIso f g).inv) ≫
        snd) ≫
      fst
[PROOFSTEP]
simp
[GOAL]
case h₁.h₁
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonal fst ≫ snd) ≫ snd =
    (((pullbackSymmetry f g).hom ≫
          map g f (snd ≫ g) f (diagonal g) (𝟙 X) (𝟙 Z)
              (_ : (Over.mk g).hom ≫ 𝟙 Z = (Over.homMk (diagonal g)).left ≫ (Over.mk (snd ≫ g)).hom)
              (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) ≫
            (diagonalObjPullbackFstIso f g).inv) ≫
        snd) ≫
      snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g
[PROOFSTEP]
rw [← cancel_mono i₃, Category.assoc, Category.assoc, Category.assoc, Category.assoc, e₁, e₂, ←
  pullback.condition_assoc, pullback.condition_assoc, pullback.condition, pullback.condition_assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
        (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
      fst =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
        (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
      fst
[PROOFSTEP]
rw [pullback.lift_fst, pullback.lift_fst]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
      lift
        (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
          (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
        (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
          (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
        (_ :
          lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
              fst =
            lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
              fst) =
    𝟙 (pullback fst fst)
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
        lift
          (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
            (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
          (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
            (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
          (_ :
            lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                  (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                fst =
              lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                  (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                fst)) ≫
      fst =
    𝟙 (pullback fst fst) ≫ fst
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h₀.h₀
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
          lift
            (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
              (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
            (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
              (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
            (_ :
              lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                    (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                  fst =
                lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                    (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                  fst)) ≫
        fst) ≫
      fst =
    (𝟙 (pullback fst fst) ≫ fst) ≫ fst
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h₀.h₀.h₀
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (((lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
            lift
              (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
              (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
              (_ :
                lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                    fst =
                  lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                    fst)) ≫
          fst) ≫
        fst) ≫
      fst =
    ((𝟙 (pullback fst fst) ≫ fst) ≫ fst) ≫ fst
[PROOFSTEP]
simp only [Category.assoc, lift_fst, lift_fst_assoc, Category.id_comp]
[GOAL]
case h₀.h₀.h₀
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ fst ≫ snd ≫ i₁ = fst ≫ fst ≫ fst
[PROOFSTEP]
rw [condition]
[GOAL]
case h₀.h₀.h₁
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (((lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
            lift
              (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
              (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
              (_ :
                lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                    fst =
                  lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                    fst)) ≫
          fst) ≫
        fst) ≫
      snd =
    ((𝟙 (pullback fst fst) ≫ fst) ≫ fst) ≫ snd
[PROOFSTEP]
simp [Category.assoc, lift_snd]
[GOAL]
case h₀.h₀.h₁
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ snd ≫ snd ≫ i₂ = fst ≫ fst ≫ snd
[PROOFSTEP]
rw [condition_assoc, condition]
[GOAL]
case h₀.h₁
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
          lift
            (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
              (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
            (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
              (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
            (_ :
              lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                    (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                  fst =
                lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                    (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                  fst)) ≫
        fst) ≫
      snd =
    (𝟙 (pullback fst fst) ≫ fst) ≫ snd
[PROOFSTEP]
simp only [Category.assoc, lift_fst_assoc, lift_snd, lift_fst, Category.id_comp]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
        lift
          (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
            (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
          (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
            (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
          (_ :
            lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                  (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                fst =
              lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                  (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                fst)) ≫
      snd =
    𝟙 (pullback fst fst) ≫ snd
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h₁.h₀
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
          lift
            (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
              (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
            (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
              (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
            (_ :
              lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                    (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                  fst =
                lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                    (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                  fst)) ≫
        snd) ≫
      fst =
    (𝟙 (pullback fst fst) ≫ snd) ≫ fst
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h₁.h₀.h₀
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (((lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
            lift
              (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
              (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
              (_ :
                lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                    fst =
                  lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                    fst)) ≫
          snd) ≫
        fst) ≫
      fst =
    ((𝟙 (pullback fst fst) ≫ snd) ≫ fst) ≫ fst
[PROOFSTEP]
simp only [Category.assoc, lift_snd_assoc, lift_fst_assoc, lift_fst, Category.id_comp]
[GOAL]
case h₁.h₀.h₀
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ fst ≫ snd ≫ i₁ = snd ≫ fst ≫ fst
[PROOFSTEP]
rw [← condition_assoc, condition]
[GOAL]
case h₁.h₀.h₁
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (((lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
            lift
              (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
              (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
              (_ :
                lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                    fst =
                  lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                    fst)) ≫
          snd) ≫
        fst) ≫
      snd =
    ((𝟙 (pullback fst fst) ≫ snd) ≫ fst) ≫ snd
[PROOFSTEP]
simp only [Category.assoc, lift_snd, lift_fst_assoc, lift_snd_assoc, Category.id_comp]
[GOAL]
case h₁.h₀.h₁
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ snd ≫ snd ≫ i₂ = snd ≫ fst ≫ snd
[PROOFSTEP]
rw [condition]
[GOAL]
case h₁.h₁
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) ≫
          lift
            (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
              (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
            (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
              (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
            (_ :
              lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                    (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                  fst =
                lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                    (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                  fst)) ≫
        snd) ≫
      snd =
    (𝟙 (pullback fst fst) ≫ snd) ≫ snd
[PROOFSTEP]
simp only [Category.assoc, lift_snd_assoc, lift_snd, Category.id_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift
        (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
          (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
        (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
          (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
        (_ :
          lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
              fst =
            lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
              fst) ≫
      lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g) =
    𝟙 (pullback f g)
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (lift
          (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
            (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
          (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
            (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
          (_ :
            lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                  (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                fst =
              lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                  (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                fst) ≫
        lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g)) ≫
      fst =
    𝟙 (pullback f g) ≫ fst
[PROOFSTEP]
simp only [Category.assoc, lift_fst, lift_fst_assoc, lift_snd, Category.id_comp]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.748423, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (lift
          (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
            (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁))
          (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
            (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂))
          (_ :
            lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
                  (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
                fst =
              lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
                  (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
                fst) ≫
        lift (fst ≫ snd) (snd ≫ snd) (_ : (fst ≫ snd) ≫ f = (snd ≫ snd) ≫ g)) ≫
      snd =
    𝟙 (pullback f g) ≫ snd
[PROOFSTEP]
simp only [Category.assoc, lift_snd, lift_snd_assoc, Category.id_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ map f g f' g' i₁ i₂ i₃ e₁ e₂ = (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫ snd ≫ fst
[PROOFSTEP]
simp only [pullbackFstFstIso_inv, lift_snd_assoc, lift_fst]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
        (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
      fst =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
        (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
      fst
[PROOFSTEP]
rw [lift_fst, lift_fst]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ fst =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ snd =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂)
[PROOFSTEP]
simp


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
⊢ ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
    ((Functor.mk src✝.toPrefunctor).map f ⊗ (Functor.mk src✝.toPrefunctor).map g) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) Y Y' =
      (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X X' ≫ (Functor.mk src✝.toPrefunctor).map (f ⊗ g)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
⊢ ((fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
      (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) (X ⊗ Y) Z ≫ (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom =
    (α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
          ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
      (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) Y Z) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (Y ⊗ Z)
[PROOFSTEP]
ext ⟨⟨f, g⟩, h⟩
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : (Functor.mk src✝.toPrefunctor).obj Z
f : (Functor.mk src✝.toPrefunctor).obj X
g : (Functor.mk src✝.toPrefunctor).obj Y
⊢ (((fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) (X ⊗ Y) Z ≫ (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom)
      ((f, g), h) =
    ((α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
            ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
        (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) Y Z) ≫
          (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (Y ⊗ Z))
      ((f, g), h)
[PROOFSTEP]
dsimp at f g h
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ (((fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) (X ⊗ Y) Z ≫ (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom)
      ((f, g), h) =
    ((α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
            ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
        (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) Y Z) ≫
          (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (Y ⊗ Z))
      ((f, g), h)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h)) ≫ (α_ X Y Z).hom =
    (λ_ (𝟙_ C)).inv ≫ (f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h))
[PROOFSTEP]
simp only [Iso.cancel_iso_inv_left, Category.assoc]
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h) ≫ (α_ X Y Z).hom = f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
conv_lhs =>
  rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal,
    triangle_assoc_comp_right_inv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h) ≫ (α_ X Y Z).hom
[PROOFSTEP]
rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal,
    triangle_assoc_comp_right_inv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h) ≫ (α_ X Y Z).hom
[PROOFSTEP]
rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal,
    triangle_assoc_comp_right_inv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ g) ⊗ h) ≫ (α_ X Y Z).hom
[PROOFSTEP]
rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal,
  triangle_assoc_comp_right_inv]
[GOAL]
case h.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ (𝟙 tensorUnit' ⊗ (λ_ (𝟙_ C)).inv) ≫ (f ⊗ g ⊗ h) = f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
conv_rhs => rw [← Category.id_comp f, tensor_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
rw [← Category.id_comp f, tensor_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
rw [← Category.id_comp f, tensor_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| f ⊗ (λ_ (𝟙_ C)).inv ≫ (g ⊗ h)
[PROOFSTEP]
rw [← Category.id_comp f, tensor_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
⊢ ∀ (X : C),
    (λ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom =
      ((fun _p => 𝟙 (op (𝟙_ C)).unop) ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj X)) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) (𝟙_ C) X ≫ (Functor.mk src✝.toPrefunctor).map (λ_ X).hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
⊢ (ρ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom =
    (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ fun _p => 𝟙 (op (𝟙_ C)).unop) ≫
      (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (𝟙_ C) ≫ (Functor.mk src✝.toPrefunctor).map (ρ_ X).hom
[PROOFSTEP]
ext ⟨f, ⟨⟩⟩
[GOAL]
case h.mk.unit
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
f : (Functor.mk src✝.toPrefunctor).obj X
⊢ (ρ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom (f, PUnit.unit) =
    ((𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ fun _p => 𝟙 (op (𝟙_ C)).unop) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (𝟙_ C) ≫ (Functor.mk src✝.toPrefunctor).map (ρ_ X).hom)
      (f, PUnit.unit)
[PROOFSTEP]
dsimp at f
[GOAL]
case h.mk.unit
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
f : 𝟙_ C ⟶ X
⊢ (ρ_ ((Functor.mk src✝.toPrefunctor).obj X)).hom (f, PUnit.unit) =
    ((𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ fun _p => 𝟙 (op (𝟙_ C)).unop) ≫
        (fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd)) X (𝟙_ C) ≫ (Functor.mk src✝.toPrefunctor).map (ρ_ X).hom)
      (f, PUnit.unit)
[PROOFSTEP]
dsimp
[GOAL]
case h.mk.unit
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
f : 𝟙_ C ⟶ X
⊢ f = ((λ_ (𝟙_ C)).inv ≫ (f ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ X).hom
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
case h.mk.unit
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ Type v := coyoneda.obj (op (𝟙_ C))
X : C
f : 𝟙_ C ⟶ X
⊢ f = (λ_ (𝟙_ C)).inv ≫ (f ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ X).hom
[PROOFSTEP]
rw [rightUnitor_naturality, unitors_inv_equal, Iso.inv_hom_id_assoc]


[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
X Y : FullSubcategory P
⊢ LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor X Y ≫
      (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.map
        ((fun X Y => Iso.mk (β_ X.obj Y.obj).hom (β_ X.obj Y.obj).inv) X Y).hom =
    (β_ ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj X)
          ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
      LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor Y X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
X Y : FullSubcategory P
⊢ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.map (β_ X Y).hom =
    inv (LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor X Y) ≫
      (β_ ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj X)
            ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
        LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor Y X
[PROOFSTEP]
rw [IsIso.eq_inv_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
X Y : FullSubcategory P
⊢ LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor X Y ≫
      (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.map (β_ X Y).hom =
    (β_ ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj X)
          ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
      LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor Y X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
h : ∀ ⦃X : C⦄, P X → P' X
X Y : FullSubcategory P
⊢ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.map (β_ X Y).hom =
    inv (LaxMonoidalFunctor.μ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor X Y) ≫
      (β_ ((fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.obj X)
            ((fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
        LaxMonoidalFunctor.μ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor Y X
[PROOFSTEP]
rw [IsIso.eq_inv_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
h : ∀ ⦃X : C⦄, P X → P' X
X Y : FullSubcategory P
⊢ LaxMonoidalFunctor.μ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor X Y ≫
      (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.map (β_ X Y).hom =
    (β_ ((fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.obj X)
          ((fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
      LaxMonoidalFunctor.μ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor Y X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X : FullSubcategory P
⊢ CategoryTheory.whiskerRight (NatTrans.mk fun Y => NatTrans.app (ihom.coev X.obj) Y.obj) (tensorLeft X) ≫
      (Functor.associator (tensorLeft X)
            (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
              (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
            (tensorLeft X)).hom ≫
        CategoryTheory.whiskerLeft (tensorLeft X) (NatTrans.mk fun Y => NatTrans.app (ihom.ev X.obj) Y.obj) =
    NatTrans.id (𝟭 (FullSubcategory P) ⋙ tensorLeft X)
[PROOFSTEP]
ext Y
[GOAL]
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X Y : FullSubcategory P
⊢ NatTrans.app
      (CategoryTheory.whiskerRight (NatTrans.mk fun Y => NatTrans.app (ihom.coev X.obj) Y.obj) (tensorLeft X) ≫
        (Functor.associator (tensorLeft X)
              (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
                (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
              (tensorLeft X)).hom ≫
          CategoryTheory.whiskerLeft (tensorLeft X) (NatTrans.mk fun Y => NatTrans.app (ihom.ev X.obj) Y.obj))
      Y =
    NatTrans.app (NatTrans.id (𝟭 (FullSubcategory P) ⋙ tensorLeft X)) Y
[PROOFSTEP]
simp
[GOAL]
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X Y : FullSubcategory P
⊢ (𝟙 X ⊗ NatTrans.app (ihom.coev X.obj) Y.obj) ≫ NatTrans.app (ihom.ev X.obj) (X ⊗ Y).obj = 𝟙 (X ⊗ Y)
[PROOFSTEP]
exact ihom.ev_coev X.1 Y.1
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X : FullSubcategory P
⊢ CategoryTheory.whiskerLeft
        (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
          (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
        (NatTrans.mk fun Y => NatTrans.app (ihom.coev X.obj) Y.obj) ≫
      (Functor.associator
            (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
              (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
            (tensorLeft X)
            (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
              (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))).inv ≫
        CategoryTheory.whiskerRight (NatTrans.mk fun Y => NatTrans.app (ihom.ev X.obj) Y.obj)
          (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
            (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y)))) =
    NatTrans.id
      (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
          (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))) ⋙
        𝟭 (FullSubcategory P))
[PROOFSTEP]
ext Y
[GOAL]
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X Y : FullSubcategory P
⊢ NatTrans.app
      (CategoryTheory.whiskerLeft
          (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
            (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
          (NatTrans.mk fun Y => NatTrans.app (ihom.coev X.obj) Y.obj) ≫
        (Functor.associator
              (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
                (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
              (tensorLeft X)
              (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
                (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))).inv ≫
          CategoryTheory.whiskerRight (NatTrans.mk fun Y => NatTrans.app (ihom.ev X.obj) Y.obj)
            (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
              (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y)))))
      Y =
    NatTrans.app
      (NatTrans.id
        (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
            (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))) ⋙
          𝟭 (FullSubcategory P)))
      Y
[PROOFSTEP]
simp
[GOAL]
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X Y : FullSubcategory P
⊢ NatTrans.app (ihom.coev X.obj) ((ihom X.obj).obj Y.obj) ≫ (ihom X.obj).map (NatTrans.app (ihom.ev X.obj) Y.obj) =
    𝟙
      ((FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
            (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj Y.obj))).obj
        Y)
[PROOFSTEP]
exact ihom.coev_ev X.1 Y.1


[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (fun X => NatTrans.app α X ⊗ NatTrans.app β X) Y =
    (fun X => NatTrans.app α X ⊗ NatTrans.app β X) X ≫ (tensorObj G G').map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (F.map f ⊗ F'.map f) ≫ (NatTrans.app α Y ⊗ NatTrans.app β Y) =
    (NatTrans.app α X ⊗ NatTrans.app β X) ≫ (G.map f ⊗ G'.map f)
[PROOFSTEP]
rw [← tensor_comp, α.naturality, β.naturality, tensor_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F✝ G F' G' : C ⥤ D
α : F✝ ⟶ G
β✝ : F' ⟶ G'
F : C ⥤ D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (fun X => F.obj X ◁ NatTrans.app β X) Y =
    (fun X => F.obj X ◁ NatTrans.app β X) X ≫ (tensorObj F G').map f
[PROOFSTEP]
simp only [← id_tensorHom]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F✝ G F' G' : C ⥤ D
α : F✝ ⟶ G
β✝ : F' ⟶ G'
F : C ⥤ D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (𝟙 (F.obj Y) ⊗ NatTrans.app β Y) = (𝟙 (F.obj X) ⊗ NatTrans.app β X) ≫ (tensorObj F G').map f
[PROOFSTEP]
apply (tensorHom (𝟙 F) β).naturality
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F'✝ G' : C ⥤ D
α : F ⟶ G
β : F'✝ ⟶ G'
F' : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (fun X => NatTrans.app α X ▷ F'.obj X) Y =
    (fun X => NatTrans.app α X ▷ F'.obj X) X ≫ (tensorObj G F').map f
[PROOFSTEP]
simp only [← tensorHom_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F'✝ G' : C ⥤ D
α : F ⟶ G
β : F'✝ ⟶ G'
F' : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (NatTrans.app α Y ⊗ 𝟙 (F'.obj Y)) =
    (NatTrans.app α X ⊗ 𝟙 (F'.obj X)) ≫ (tensorObj G F').map f
[PROOFSTEP]
apply (tensorHom α (𝟙 F')).naturality
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
⊢ ∀ {X₁ Y₁ X₂ Y₂ : C ⥤ D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) f g =
      (fun {X₁ X₂} α F => FunctorCategory.whiskerRight α F) f X₂ ≫
        (fun F x x_1 α => FunctorCategory.whiskerLeft F α) Y₁ X₂ Y₂ g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X₁✝ Y₁✝ X₂✝ Y₂✝ : C ⥤ D
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) f✝ g✝ =
    (fun {X₁ X₂} α F => FunctorCategory.whiskerRight α F) f✝ X₂✝ ≫
      (fun F x x_1 α => FunctorCategory.whiskerLeft F α) Y₁✝ X₂✝ Y₂✝ g✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X₁✝ Y₁✝ X₂✝ Y₂✝ : C ⥤ D
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
x✝ : C
⊢ NatTrans.app ((fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) f✝ g✝) x✝ =
    NatTrans.app
      ((fun {X₁ X₂} α F => FunctorCategory.whiskerRight α F) f✝ X₂✝ ≫
        (fun F x x_1 α => FunctorCategory.whiskerLeft F α) Y₁✝ X₂✝ Y₂✝ g✝)
      x✝
[PROOFSTEP]
simp [tensorHom_def]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
⊢ (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β)
        ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F G H).hom (𝟙 K) ≫
      ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F
            ((fun F G => FunctorCategory.tensorObj F G) G H) K).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) (𝟙 F)
          ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) G H K).hom =
    ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X))
          ((fun F G => FunctorCategory.tensorObj F G) F G) H K).hom ≫
      ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F G
          ((fun F G => FunctorCategory.tensorObj F G) H K)).hom
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ NatTrans.app
      ((fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β)
          ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F G H).hom (𝟙 K) ≫
        ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F
              ((fun F G => FunctorCategory.tensorObj F G) G H) K).hom ≫
          (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) (𝟙 F)
            ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) G H K).hom)
      X =
    NatTrans.app
      (((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X))
            ((fun F G => FunctorCategory.tensorObj F G) F G) H K).hom ≫
        ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F G
            ((fun F G => FunctorCategory.tensorObj F G) H K)).hom)
      X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ ((α_ (F.obj X) (G.obj X) (H.obj X)).hom ⊗ 𝟙 (K.obj X)) ≫
      (α_ (F.obj X) (G.obj X ⊗ H.obj X) (K.obj X)).hom ≫ (𝟙 (F.obj X) ⊗ (α_ (G.obj X) (H.obj X) (K.obj X)).hom) =
    (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom
[PROOFSTEP]
rw [pentagon]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).hom ≫ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F (G ⊗ H)).hom ≫ (α_ G H F).hom =
    (((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F G).hom ⊗ 𝟙 H) ≫
      (α_ G F H).hom ≫ (𝟙 G ⊗ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F H).hom)
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ NatTrans.app
      ((α_ F G H).hom ≫
        ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F (G ⊗ H)).hom ≫ (α_ G H F).hom)
      X =
    NatTrans.app
      ((((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F G).hom ⊗ 𝟙 H) ≫
        (α_ G F H).hom ≫ (𝟙 G ⊗ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F H).hom))
      X
[PROOFSTEP]
apply hexagon_forward
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).inv ≫ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) (F ⊗ G) H).hom ≫ (α_ H F G).inv =
    (𝟙 F ⊗ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) G H).hom) ≫
      (α_ F H G).inv ≫ (((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F H).hom ⊗ 𝟙 G)
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ NatTrans.app
      ((α_ F G H).inv ≫
        ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) (F ⊗ G) H).hom ≫ (α_ H F G).inv)
      X =
    NatTrans.app
      ((𝟙 F ⊗ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) G H).hom) ≫
        (α_ F H G).inv ≫ (((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F H).hom ⊗ 𝟙 G))
      X
[PROOFSTEP]
apply hexagon_reverse
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : SymmetricCategory D
F G : C ⥤ D
⊢ (β_ F G).hom ≫ (β_ G F).hom = 𝟙 (F ⊗ G)
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : SymmetricCategory D
F G : C ⥤ D
X : C
⊢ NatTrans.app ((β_ F G).hom ≫ (β_ G F).hom) X = NatTrans.app (𝟙 (F ⊗ G)) X
[PROOFSTEP]
apply symmetry