[GOAL]
J : Type w
X✝ Y✝ Z✝ : WidePullbackShape J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ X✝ ⟶ Z✝
[PROOFSTEP]
cases f
[GOAL]
case id
J : Type w
X✝ Z✝ : WidePullbackShape J
g : X✝ ⟶ Z✝
⊢ X✝ ⟶ Z✝
case term J : Type w Z✝ : WidePullbackShape J j✝ : J g : none ⟶ Z✝ ⊢ some j✝ ⟶ Z✝
[PROOFSTEP]
exact g
[GOAL]
case term
J : Type w
Z✝ : WidePullbackShape J
j✝ : J
g : none ⟶ Z✝
⊢ some j✝ ⟶ Z✝
[PROOFSTEP]
cases g
[GOAL]
case term.id
J : Type w
j✝ : J
⊢ some j✝ ⟶ none
[PROOFSTEP]
apply Hom.term _
[GOAL]
J : Type w
x✝¹ x✝ : WidePullbackShape J
⊢ Subsingleton (x✝¹ ⟶ x✝)
[PROOFSTEP]
constructor
[GOAL]
case allEq
J : Type w
x✝¹ x✝ : WidePullbackShape J
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b
[PROOFSTEP]
intro a b
[GOAL]
case allEq
J : Type w
x✝¹ x✝ : WidePullbackShape J
a b : x✝¹ ⟶ x✝
⊢ a = b
[PROOFSTEP]
casesm*WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)
[GOAL]
case allEq.none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none
case allEq.some.none.term.term
J : Type w
val✝ : J
⊢ Hom.term val✝ = Hom.term val✝
case allEq.some.some.id.id J : Type w val✝ : J ⊢ Hom.id (some val✝) = Hom.id (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case allEq.some.none.term.term
J : Type w
val✝ : J
⊢ Hom.term val✝ = Hom.term val✝
case allEq.some.some.id.id J : Type w val✝ : J ⊢ Hom.id (some val✝) = Hom.id (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case allEq.some.some.id.id
J : Type w
val✝ : J
⊢ Hom.id (some val✝) = Hom.id (some val✝)
[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
X✝ Y✝ : WidePullbackShape J
f : X✝ ⟶ Y✝
⊢ (fun j => Option.casesOn j B objs) X✝ ⟶ (fun j => Option.casesOn j B objs) Y✝
[PROOFSTEP]
cases' f with _ j
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
X✝ : WidePullbackShape J
⊢ (fun j => Option.casesOn j B objs) X✝ ⟶ (fun j => Option.casesOn j B objs) X✝
[PROOFSTEP]
apply 𝟙 _
[GOAL]
case term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
j : J
⊢ (fun j => Option.casesOn j B objs) (some j) ⟶ (fun j => Option.casesOn j B objs) none
[PROOFSTEP]
exact arrows j
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
j : WidePullbackShape J
⊢ F.obj j = (wideCospan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.term j)).obj j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
j j' : WidePullbackShape J
f : j ⟶ j'
⊢ ((Functor.const (WidePullbackShape J)).obj X).map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        j' =
    (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        j ≫
      F.map f
[PROOFSTEP]
cases j
[GOAL]
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
j' : WidePullbackShape J
f : none ⟶ j'
⊢ ((Functor.const (WidePullbackShape J)).obj X).map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        j' =
    (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        none ≫
      F.map f
[PROOFSTEP]
cases j'
[GOAL]
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
j' : WidePullbackShape J
val✝ : J
f : some val✝ ⟶ j'
⊢ ((Functor.const (WidePullbackShape J)).obj X).map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        j' =
    (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        (some val✝) ≫
      F.map f
[PROOFSTEP]
cases j'
[GOAL]
case none.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
f : none ⟶ none
⊢ ((Functor.const (WidePullbackShape J)).obj X).map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        none =
    (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        none ≫
      F.map f
[PROOFSTEP]
cases f
[GOAL]
case none.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
val✝ : J
f : none ⟶ some val✝
⊢ ((Functor.const (WidePullbackShape J)).obj X).map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        none ≫
      F.map f
[PROOFSTEP]
cases f
[GOAL]
case some.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
val✝ : J
f : some val✝ ⟶ none
⊢ ((Functor.const (WidePullbackShape J)).obj X).map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        none =
    (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        (some val✝) ≫
      F.map f
[PROOFSTEP]
cases f
[GOAL]
case some.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
val✝¹ val✝ : J
f : some val✝¹ ⟶ some val✝
⊢ ((Functor.const (WidePullbackShape J)).obj X).map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f✝
          | some j => π j)
        (some val✝¹) ≫
      F.map f
[PROOFSTEP]
cases f
[GOAL]
case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
⊢ ((Functor.const (WidePullbackShape J)).obj X).map (Hom.id none) ≫
      (fun j =>
          match j with
          | none => f
          | some j => π j)
        none =
    (fun j =>
          match j with
          | none => f
          | some j => π j)
        none ≫
      F.map (Hom.id none)
[PROOFSTEP]
refine id _
[GOAL]
case some.none.term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ ((Functor.const (WidePullbackShape J)).obj X).map (Hom.term val✝) ≫
      (fun j =>
          match j with
          | none => f
          | some j => π j)
        none =
    (fun j =>
          match j with
          | none => f
          | some j => π j)
        (some val✝) ≫
      F.map (Hom.term val✝)
[PROOFSTEP]
refine id _
[GOAL]
case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ ((Functor.const (WidePullbackShape J)).obj X).map (Hom.id (some val✝)) ≫
      (fun j =>
          match j with
          | none => f
          | some j => π j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f
          | some j => π j)
        (some val✝) ≫
      F.map (Hom.id (some val✝))
[PROOFSTEP]
refine id _
[GOAL]
case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
⊢ ((Functor.const (WidePullbackShape J)).obj X).map (Hom.id none) ≫
      (fun j =>
          match j with
          | none => f
          | some j => π j)
        none =
    (fun j =>
          match j with
          | none => f
          | some j => π j)
        none ≫
      F.map (Hom.id none)
[PROOFSTEP]
dsimp
[GOAL]
case some.none.term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ ((Functor.const (WidePullbackShape J)).obj X).map (Hom.term val✝) ≫
      (fun j =>
          match j with
          | none => f
          | some j => π j)
        none =
    (fun j =>
          match j with
          | none => f
          | some j => π j)
        (some val✝) ≫
      F.map (Hom.term val✝)
[PROOFSTEP]
dsimp
[GOAL]
case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ ((Functor.const (WidePullbackShape J)).obj X).map (Hom.id (some val✝)) ≫
      (fun j =>
          match j with
          | none => f
          | some j => π j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f
          | some j => π j)
        (some val✝) ≫
      F.map (Hom.id (some val✝))
[PROOFSTEP]
dsimp
[GOAL]
case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
⊢ 𝟙 X ≫ f = f ≫ F.map (𝟙 none)
[PROOFSTEP]
simp [w]
[GOAL]
case some.none.term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ 𝟙 X ≫ f = π val✝ ≫ F.map (Hom.term val✝)
[PROOFSTEP]
simp [w]
[GOAL]
case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ 𝟙 X ≫ π val✝ = π val✝ ≫ F.map (𝟙 (some val✝))
[PROOFSTEP]
simp [w]
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePullbackShape J
⊢ (𝟭 (WidePullbackShape J)).obj j ≅
    ((wideCospan none (fun j => some (↑h j)) fun j => Hom.term (↑h j)) ⋙
          wideCospan none (fun j => some (Equiv.invFun h j)) fun j => Hom.term (Equiv.invFun h j)).obj
      j
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case none
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ none ≅ none
case some J : Type w C : Type u inst : Category.{v, u} C J' : Type w' h : J ≃ J' val✝ : J ⊢ some val✝ ≅ some val✝
[PROOFSTEP]
repeat rfl
[GOAL]
case none
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ none ≅ none
case some J : Type w C : Type u inst : Category.{v, u} C J' : Type w' h : J ≃ J' val✝ : J ⊢ some val✝ ≅ some val✝
[PROOFSTEP]
rfl
[GOAL]
case some
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ some val✝ ≅ some val✝
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
X✝ Y✝ : WidePullbackShape J
f : X✝ ⟶ Y✝
⊢ (𝟭 (WidePullbackShape J)).map f ≫
      ((fun j =>
            id
              (Option.casesOn j (id (Iso.refl none)) fun val =>
                Eq.mpr
                  (_ :
                    (some val ≅
                        Option.rec none (fun val => some (↑h.symm val))
                          (Option.rec none (fun val => some (↑h val)) (some val))) =
                      (some val ≅ some val))
                  (Iso.refl (some val))))
          Y✝).hom =
    ((fun j =>
            id
              (Option.casesOn j (id (Iso.refl none)) fun val =>
                Eq.mpr
                  (_ :
                    (some val ≅
                        Option.rec none (fun val => some (↑h.symm val))
                          (Option.rec none (fun val => some (↑h val)) (some val))) =
                      (some val ≅ some val))
                  (Iso.refl (some val))))
          X✝).hom ≫
      ((wideCospan none (fun j => some (↑h j)) fun j => Hom.term (↑h j)) ⋙
            wideCospan none (fun j => some (Equiv.invFun h j)) fun j => Hom.term (Equiv.invFun h j)).map
        f
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePullbackShape J'
⊢ ((wideCospan none (fun j => some (Equiv.invFun h j)) fun j => Hom.term (Equiv.invFun h j)) ⋙
          wideCospan none (fun j => some (↑h j)) fun j => Hom.term (↑h j)).obj
      j ≅
    (𝟭 (WidePullbackShape J')).obj j
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case none
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ none ≅ none
case some J : Type w C : Type u inst : Category.{v, u} C J' : Type w' h : J ≃ J' val✝ : J' ⊢ some val✝ ≅ some val✝
[PROOFSTEP]
repeat rfl
[GOAL]
case none
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ none ≅ none
case some J : Type w C : Type u inst : Category.{v, u} C J' : Type w' h : J ≃ J' val✝ : J' ⊢ some val✝ ≅ some val✝
[PROOFSTEP]
rfl
[GOAL]
case some
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ some val✝ ≅ some val✝
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
X✝ Y✝ : WidePullbackShape J'
f : X✝ ⟶ Y✝
⊢ ((wideCospan none (fun j => some (Equiv.invFun h j)) fun j => Hom.term (Equiv.invFun h j)) ⋙
            wideCospan none (fun j => some (↑h j)) fun j => Hom.term (↑h j)).map
        f ≫
      ((fun j =>
            id
              (Option.casesOn j (id (Iso.refl none)) fun val =>
                Eq.mpr
                  (_ :
                    (Option.rec none (fun val => some (↑h val))
                          (Option.rec none (fun val => some (↑h.symm val)) (some val)) ≅
                        some val) =
                      (some val ≅ some val))
                  (Iso.refl (some val))))
          Y✝).hom =
    ((fun j =>
            id
              (Option.casesOn j (id (Iso.refl none)) fun val =>
                Eq.mpr
                  (_ :
                    (Option.rec none (fun val => some (↑h val))
                          (Option.rec none (fun val => some (↑h.symm val)) (some val)) ≅
                        some val) =
                      (some val ≅ some val))
                  (Iso.refl (some val))))
          X✝).hom ≫
      (𝟭 (WidePullbackShape J')).map f
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
J : Type w
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ X✝ ⟶ Z✝
[PROOFSTEP]
cases f
[GOAL]
case id
J : Type w
X✝ Z✝ : WidePushoutShape J
g : X✝ ⟶ Z✝
⊢ X✝ ⟶ Z✝
case init J : Type w Z✝ : WidePushoutShape J j✝ : J g : some j✝ ⟶ Z✝ ⊢ none ⟶ Z✝
[PROOFSTEP]
exact g
[GOAL]
case init
J : Type w
Z✝ : WidePushoutShape J
j✝ : J
g : some j✝ ⟶ Z✝
⊢ none ⟶ Z✝
[PROOFSTEP]
cases g
[GOAL]
case init.id
J : Type w
j✝ : J
⊢ none ⟶ some j✝
[PROOFSTEP]
apply Hom.init _
[GOAL]
J : Type w
x✝¹ x✝ : WidePushoutShape J
⊢ Subsingleton (x✝¹ ⟶ x✝)
[PROOFSTEP]
constructor
[GOAL]
case allEq
J : Type w
x✝¹ x✝ : WidePushoutShape J
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b
[PROOFSTEP]
intro a b
[GOAL]
case allEq
J : Type w
x✝¹ x✝ : WidePushoutShape J
a b : x✝¹ ⟶ x✝
⊢ a = b
[PROOFSTEP]
casesm*WidePushoutShape _, (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _)
[GOAL]
case allEq.none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none
case allEq.none.some.init.init
J : Type w
val✝ : J
⊢ Hom.init val✝ = Hom.init val✝
case allEq.some.some.id.id J : Type w val✝ : J ⊢ Hom.id (some val✝) = Hom.id (some val✝)
[PROOFSTEP]
repeat rfl
[GOAL]
case allEq.none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none
case allEq.none.some.init.init
J : Type w
val✝ : J
⊢ Hom.init val✝ = Hom.init val✝
case allEq.some.some.id.id J : Type w val✝ : J ⊢ Hom.id (some val✝) = Hom.id (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case allEq.none.some.init.init
J : Type w
val✝ : J
⊢ Hom.init val✝ = Hom.init val✝
case allEq.some.some.id.id J : Type w val✝ : J ⊢ Hom.id (some val✝) = Hom.id (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case allEq.some.some.id.id
J : Type w
val✝ : J
⊢ Hom.id (some val✝) = Hom.id (some val✝)
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Y✝ : WidePushoutShape J
f : X✝ ⟶ Y✝
⊢ (fun j => Option.casesOn j B objs) X✝ ⟶ (fun j => Option.casesOn j B objs) Y✝
[PROOFSTEP]
cases' f with _ j
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ : WidePushoutShape J
⊢ (fun j => Option.casesOn j B objs) X✝ ⟶ (fun j => Option.casesOn j B objs) X✝
[PROOFSTEP]
apply 𝟙 _
[GOAL]
case init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j : J
⊢ (fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) (some j)
[PROOFSTEP]
exact arrows j
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun j => Option.casesOn j B objs,
          map := fun {X Y} f =>
            Hom.casesOn (motive := fun a a_1 t =>
              X = a → Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
              f
              (fun X_1 h =>
                Eq.ndrec (motive := fun X_2 =>
                  Y = X_2 →
                    HEq f (Hom.id X_2) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                  (fun h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : X ⟶ Y) →
                        HEq f (Hom.id X) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                      (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                  h)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = some j →
                      HEq f (Hom.init j) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : none ⟶ Y) →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                      (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                  (_ : none = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (f ≫ g) =
    { obj := fun j => Option.casesOn j B objs,
            map := fun {X Y} f =>
              Hom.casesOn (motive := fun a a_1 t =>
                X = a →
                  Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                f
                (fun X_1 h =>
                  Eq.ndrec (motive := fun X_2 =>
                    Y = X_2 →
                      HEq f (Hom.id X_2) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : X ⟶ Y) →
                          HEq f (Hom.id X) →
                            ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                    h)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = some j →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : none ⟶ Y) →
                          HEq f (Hom.init j) →
                            ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                    (_ : none = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        f ≫
      { obj := fun j => Option.casesOn j B objs,
            map := fun {X Y} f =>
              Hom.casesOn (motive := fun a a_1 t =>
                X = a →
                  Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                f
                (fun X_1 h =>
                  Eq.ndrec (motive := fun X_2 =>
                    Y = X_2 →
                      HEq f (Hom.id X_2) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : X ⟶ Y) →
                          HEq f (Hom.id X) →
                            ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                    h)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = some j →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : none ⟶ Y) →
                          HEq f (Hom.init j) →
                            ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                    (_ : none = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
cases f
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Z✝ : WidePushoutShape J
g : X✝ ⟶ Z✝
⊢ { obj := fun j => Option.casesOn j B objs,
          map := fun {X Y} f =>
            Hom.casesOn (motive := fun a a_1 t =>
              X = a → Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
              f
              (fun X_1 h =>
                Eq.ndrec (motive := fun X_2 =>
                  Y = X_2 →
                    HEq f (Hom.id X_2) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                  (fun h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : X ⟶ Y) →
                        HEq f (Hom.id X) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                      (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                  h)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = some j →
                      HEq f (Hom.init j) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : none ⟶ Y) →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                      (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                  (_ : none = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (Hom.id X✝ ≫ g) =
    { obj := fun j => Option.casesOn j B objs,
            map := fun {X Y} f =>
              Hom.casesOn (motive := fun a a_1 t =>
                X = a →
                  Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                f
                (fun X_1 h =>
                  Eq.ndrec (motive := fun X_2 =>
                    Y = X_2 →
                      HEq f (Hom.id X_2) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : X ⟶ Y) →
                          HEq f (Hom.id X) →
                            ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                    h)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = some j →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : none ⟶ Y) →
                          HEq f (Hom.init j) →
                            ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                    (_ : none = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (Hom.id X✝) ≫
      { obj := fun j => Option.casesOn j B objs,
            map := fun {X Y} f =>
              Hom.casesOn (motive := fun a a_1 t =>
                X = a →
                  Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                f
                (fun X_1 h =>
                  Eq.ndrec (motive := fun X_2 =>
                    Y = X_2 →
                      HEq f (Hom.id X_2) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : X ⟶ Y) →
                          HEq f (Hom.id X) →
                            ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                    h)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = some j →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : none ⟶ Y) →
                          HEq f (Hom.init j) →
                            ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                    (_ : none = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.id_comp]
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Z✝ : WidePushoutShape J
g : X✝ ⟶ Z✝
⊢ Hom.rec (motive := fun a a_1 t =>
      X✝ = a →
        Z✝ = a_1 → HEq (𝟙 X✝ ≫ g) t → (Option.rec B (fun val => objs val) X✝ ⟶ Option.rec B (fun val => objs val) Z✝))
      (fun X h =>
        Eq.rec (motive := fun x x_1 =>
          Z✝ = x →
            HEq (𝟙 X✝ ≫ g) (𝟙 x) → (Option.rec B (fun val => objs val) X✝ ⟶ Option.rec B (fun val => objs val) Z✝))
          (fun h =>
            Eq.rec (motive := fun x x_1 =>
              (f : X✝ ⟶ x) →
                HEq f (𝟙 X✝) → (Option.rec B (fun val => objs val) X✝ ⟶ Option.rec B (fun val => objs val) x))
              (fun f h => 𝟙 (Option.rec B (fun val => objs val) X✝)) (_ : X✝ = Z✝) (𝟙 X✝ ≫ g))
          h)
      (fun j h =>
        Eq.rec (motive := fun x x_1 =>
          (f : x ⟶ Z✝) →
            Z✝ = some j →
              HEq f (Hom.init j) → (Option.rec B (fun val => objs val) x ⟶ Option.rec B (fun val => objs val) Z✝))
          (fun f h =>
            Eq.rec (motive := fun x x_1 =>
              (f : none ⟶ x) → HEq f (Hom.init j) → (B ⟶ Option.rec B (fun val => objs val) x)) (fun f h => arrows j)
              (_ : some j = Z✝) f)
          (_ : none = X✝) (𝟙 X✝ ≫ g))
      (𝟙 X✝ ≫ g) (_ : X✝ = X✝) (_ : Z✝ = Z✝) (_ : HEq (Hom.id X✝ ≫ g) (Hom.id X✝ ≫ g)) =
    Hom.rec (motive := fun a a_1 t =>
      X✝ = a → Z✝ = a_1 → HEq g t → (Option.rec B (fun val => objs val) X✝ ⟶ Option.rec B (fun val => objs val) Z✝))
      (fun X h =>
        Eq.rec (motive := fun x x_1 =>
          Z✝ = x → HEq g (𝟙 x) → (Option.rec B (fun val => objs val) X✝ ⟶ Option.rec B (fun val => objs val) Z✝))
          (fun h =>
            Eq.rec (motive := fun x x_1 =>
              (f : X✝ ⟶ x) →
                HEq f (𝟙 X✝) → (Option.rec B (fun val => objs val) X✝ ⟶ Option.rec B (fun val => objs val) x))
              (fun f h => 𝟙 (Option.rec B (fun val => objs val) X✝)) (_ : X✝ = Z✝) g)
          h)
      (fun j h =>
        Eq.rec (motive := fun x x_1 =>
          (f : x ⟶ Z✝) →
            Z✝ = some j →
              HEq f (Hom.init j) → (Option.rec B (fun val => objs val) x ⟶ Option.rec B (fun val => objs val) Z✝))
          (fun f h =>
            Eq.rec (motive := fun x x_1 =>
              (f : none ⟶ x) → HEq f (Hom.init j) → (B ⟶ Option.rec B (fun val => objs val) x)) (fun f h => arrows j)
              (_ : some j = Z✝) f)
          (_ : none = X✝) g)
      g (_ : X✝ = X✝) (_ : Z✝ = Z✝) (_ : HEq g g)
[PROOFSTEP]
congr
[GOAL]
case init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
Z✝ : WidePushoutShape J
j✝ : J
g : some j✝ ⟶ Z✝
⊢ { obj := fun j => Option.casesOn j B objs,
          map := fun {X Y} f =>
            Hom.casesOn (motive := fun a a_1 t =>
              X = a → Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
              f
              (fun X_1 h =>
                Eq.ndrec (motive := fun X_2 =>
                  Y = X_2 →
                    HEq f (Hom.id X_2) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                  (fun h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : X ⟶ Y) →
                        HEq f (Hom.id X) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                      (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                  h)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = some j →
                      HEq f (Hom.init j) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : none ⟶ Y) →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                      (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                  (_ : none = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (Hom.init j✝ ≫ g) =
    { obj := fun j => Option.casesOn j B objs,
            map := fun {X Y} f =>
              Hom.casesOn (motive := fun a a_1 t =>
                X = a →
                  Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                f
                (fun X_1 h =>
                  Eq.ndrec (motive := fun X_2 =>
                    Y = X_2 →
                      HEq f (Hom.id X_2) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : X ⟶ Y) →
                          HEq f (Hom.id X) →
                            ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                    h)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = some j →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : none ⟶ Y) →
                          HEq f (Hom.init j) →
                            ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                    (_ : none = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (Hom.init j✝) ≫
      { obj := fun j => Option.casesOn j B objs,
            map := fun {X Y} f =>
              Hom.casesOn (motive := fun a a_1 t =>
                X = a →
                  Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                f
                (fun X_1 h =>
                  Eq.ndrec (motive := fun X_2 =>
                    Y = X_2 →
                      HEq f (Hom.id X_2) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : X ⟶ Y) →
                          HEq f (Hom.id X) →
                            ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                    h)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = some j →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : none ⟶ Y) →
                          HEq f (Hom.init j) →
                            ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                    (_ : none = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        g
[PROOFSTEP]
cases g
[GOAL]
case init.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j✝ : J
⊢ { obj := fun j => Option.casesOn j B objs,
          map := fun {X Y} f =>
            Hom.casesOn (motive := fun a a_1 t =>
              X = a → Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
              f
              (fun X_1 h =>
                Eq.ndrec (motive := fun X_2 =>
                  Y = X_2 →
                    HEq f (Hom.id X_2) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                  (fun h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : X ⟶ Y) →
                        HEq f (Hom.id X) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                      (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                  h)
              (fun j h =>
                Eq.ndrec (motive := fun {X} =>
                  (f : X ⟶ Y) →
                    Y = some j →
                      HEq f (Hom.init j) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                  (fun f h =>
                    Eq.ndrec (motive := fun {Y} =>
                      (f : none ⟶ Y) →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                      (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                  (_ : none = X) f)
              (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
      (Hom.init j✝ ≫ Hom.id (some j✝)) =
    { obj := fun j => Option.casesOn j B objs,
            map := fun {X Y} f =>
              Hom.casesOn (motive := fun a a_1 t =>
                X = a →
                  Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                f
                (fun X_1 h =>
                  Eq.ndrec (motive := fun X_2 =>
                    Y = X_2 →
                      HEq f (Hom.id X_2) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : X ⟶ Y) →
                          HEq f (Hom.id X) →
                            ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                    h)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = some j →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : none ⟶ Y) →
                          HEq f (Hom.init j) →
                            ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                    (_ : none = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (Hom.init j✝) ≫
      { obj := fun j => Option.casesOn j B objs,
            map := fun {X Y} f =>
              Hom.casesOn (motive := fun a a_1 t =>
                X = a →
                  Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                f
                (fun X_1 h =>
                  Eq.ndrec (motive := fun X_2 =>
                    Y = X_2 →
                      HEq f (Hom.id X_2) →
                        ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : X ⟶ Y) →
                          HEq f (Hom.id X) →
                            ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.id X = f) ▸ 𝟙 ((fun j => Option.casesOn j B objs) X)) (_ : X = Y) f)
                    h)
                (fun j h =>
                  Eq.ndrec (motive := fun {X} =>
                    (f : X ⟶ Y) →
                      Y = some j →
                        HEq f (Hom.init j) →
                          ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y))
                    (fun f h =>
                      Eq.ndrec (motive := fun {Y} =>
                        (f : none ⟶ Y) →
                          HEq f (Hom.init j) →
                            ((fun j => Option.casesOn j B objs) none ⟶ (fun j => Option.casesOn j B objs) Y))
                        (fun f h => (_ : Hom.init j = f) ▸ arrows j) (_ : some j = Y) f)
                    (_ : none = X) f)
                (_ : X = X) (_ : Y = Y) (_ : HEq f f) }.map
        (Hom.id (some j✝))
[PROOFSTEP]
simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.comp_id]
[GOAL]
case init.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j✝ : J
⊢ Hom.rec (motive := fun a a_1 t => none = a → some j✝ = a_1 → HEq (Hom.init j✝ ≫ 𝟙 (some j✝)) t → (B ⟶ objs j✝))
      (fun X h =>
        Eq.rec (motive := fun x x_1 => some j✝ = x → HEq (Hom.init j✝ ≫ 𝟙 (some j✝)) (𝟙 x) → (B ⟶ objs j✝))
          (fun h =>
            Eq.rec (motive := fun x x_1 => (f : none ⟶ x) → HEq f (𝟙 none) → (B ⟶ Option.rec B (fun val => objs val) x))
              (fun f h => 𝟙 B) (_ : none = some j✝) (Hom.init j✝ ≫ 𝟙 (some j✝)))
          h)
      (fun j h h =>
        Eq.rec (motive := fun x x_1 => (f : none ⟶ x) → HEq f (Hom.init j) → (B ⟶ Option.rec B (fun val => objs val) x))
          (fun f h => arrows j) (_ : some j = some j✝) (Hom.init j✝ ≫ 𝟙 (some j✝)))
      (Hom.init j✝ ≫ 𝟙 (some j✝)) (_ : none = none) (_ : some j✝ = some j✝)
      (_ : HEq (Hom.init j✝ ≫ Hom.id (some j✝)) (Hom.init j✝ ≫ Hom.id (some j✝))) =
    arrows j✝
[PROOFSTEP]
congr
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
j : WidePushoutShape J
⊢ F.obj j = (wideSpan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.init j)).obj j
[PROOFSTEP]
cases j
[GOAL]
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
⊢ F.obj none = (wideSpan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.init j)).obj none
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
val✝ : J
⊢ F.obj (some val✝) = (wideSpan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.init j)).obj (some val✝)
[PROOFSTEP]
repeat rfl
[GOAL]
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
⊢ F.obj none = (wideSpan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.init j)).obj none
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
val✝ : J
⊢ F.obj (some val✝) = (wideSpan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.init j)).obj (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
val✝ : J
⊢ F.obj (some val✝) = (wideSpan (F.obj none) (fun j => F.obj (some j)) fun j => F.map (Hom.init j)).obj (some val✝)
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
j j' : WidePushoutShape J
f : j ⟶ j'
⊢ F.map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        j' =
    (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        j ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
[PROOFSTEP]
cases j
[GOAL]
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
j' : WidePushoutShape J
f : none ⟶ j'
⊢ F.map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        j' =
    (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        none ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
[PROOFSTEP]
cases j'
[GOAL]
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
j' : WidePushoutShape J
val✝ : J
f : some val✝ ⟶ j'
⊢ F.map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        j' =
    (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        (some val✝) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
[PROOFSTEP]
cases j'
[GOAL]
case none.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
f : none ⟶ none
⊢ F.map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        none =
    (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        none ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
[PROOFSTEP]
cases f
[GOAL]
case none.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝ : J
f : none ⟶ some val✝
⊢ F.map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        none ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
[PROOFSTEP]
cases f
[GOAL]
case some.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝ : J
f : some val✝ ⟶ none
⊢ F.map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        none =
    (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        (some val✝) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
[PROOFSTEP]
cases f
[GOAL]
case some.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
val✝¹ val✝ : J
f : some val✝¹ ⟶ some val✝
⊢ F.map f ≫
      (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f✝
          | some j => ι j)
        (some val✝¹) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
[PROOFSTEP]
cases f
[GOAL]
case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
⊢ F.map (Hom.id none) ≫
      (fun j =>
          match j with
          | none => f
          | some j => ι j)
        none =
    (fun j =>
          match j with
          | none => f
          | some j => ι j)
        none ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id none)
[PROOFSTEP]
refine id _
[GOAL]
case none.some.init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ F.map (Hom.init val✝) ≫
      (fun j =>
          match j with
          | none => f
          | some j => ι j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f
          | some j => ι j)
        none ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.init val✝)
[PROOFSTEP]
refine id _
[GOAL]
case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ F.map (Hom.id (some val✝)) ≫
      (fun j =>
          match j with
          | none => f
          | some j => ι j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f
          | some j => ι j)
        (some val✝) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id (some val✝))
[PROOFSTEP]
refine id _
[GOAL]
case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
⊢ F.map (Hom.id none) ≫
      (fun j =>
          match j with
          | none => f
          | some j => ι j)
        none =
    (fun j =>
          match j with
          | none => f
          | some j => ι j)
        none ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id none)
[PROOFSTEP]
dsimp
[GOAL]
case none.some.init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ F.map (Hom.init val✝) ≫
      (fun j =>
          match j with
          | none => f
          | some j => ι j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f
          | some j => ι j)
        none ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.init val✝)
[PROOFSTEP]
dsimp
[GOAL]
case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ F.map (Hom.id (some val✝)) ≫
      (fun j =>
          match j with
          | none => f
          | some j => ι j)
        (some val✝) =
    (fun j =>
          match j with
          | none => f
          | some j => ι j)
        (some val✝) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id (some val✝))
[PROOFSTEP]
dsimp
[GOAL]
case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
⊢ F.map (𝟙 none) ≫ f = f ≫ 𝟙 X
[PROOFSTEP]
simp [w]
[GOAL]
case none.some.init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ F.map (Hom.init val✝) ≫ ι val✝ = f ≫ 𝟙 X
[PROOFSTEP]
simp [w]
[GOAL]
case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ F.map (𝟙 (some val✝)) ≫ ι val✝ = ι val✝ ≫ 𝟙 X
[PROOFSTEP]
simp [w]
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J
⊢ (𝟭 (WidePushoutShape J)).obj j ≅
    ((wideSpan none (fun j => some (↑h j)) fun j => Hom.init (↑h j)) ⋙
          wideSpan none (fun j => some (Equiv.invFun h j)) fun j => Hom.init (Equiv.invFun h j)).obj
      j
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case none
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ none ≅ none
case some J : Type w C : Type u inst : Category.{v, u} C J' : Type w' h : J ≃ J' val✝ : J ⊢ some val✝ ≅ some val✝
[PROOFSTEP]
repeat rfl
[GOAL]
case none
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ none ≅ none
case some J : Type w C : Type u inst : Category.{v, u} C J' : Type w' h : J ≃ J' val✝ : J ⊢ some val✝ ≅ some val✝
[PROOFSTEP]
rfl
[GOAL]
case some
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ some val✝ ≅ some val✝
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
X✝ Y✝ : WidePushoutShape J
f : X✝ ⟶ Y✝
⊢ (𝟭 (WidePushoutShape J)).map f ≫
      ((fun j =>
            id
              (Option.casesOn j (id (Iso.refl none)) fun val =>
                Eq.mpr
                  (_ :
                    (some val ≅
                        Option.rec none (fun val => some (↑h.symm val))
                          (Option.rec none (fun val => some (↑h val)) (some val))) =
                      (some val ≅ some val))
                  (Iso.refl (some val))))
          Y✝).hom =
    ((fun j =>
            id
              (Option.casesOn j (id (Iso.refl none)) fun val =>
                Eq.mpr
                  (_ :
                    (some val ≅
                        Option.rec none (fun val => some (↑h.symm val))
                          (Option.rec none (fun val => some (↑h val)) (some val))) =
                      (some val ≅ some val))
                  (Iso.refl (some val))))
          X✝).hom ≫
      ((wideSpan none (fun j => some (↑h j)) fun j => Hom.init (↑h j)) ⋙
            wideSpan none (fun j => some (Equiv.invFun h j)) fun j => Hom.init (Equiv.invFun h j)).map
        f
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J'
⊢ ((wideSpan none (fun j => some (Equiv.invFun h j)) fun j => Hom.init (Equiv.invFun h j)) ⋙
          wideSpan none (fun j => some (↑h j)) fun j => Hom.init (↑h j)).obj
      j ≅
    (𝟭 (WidePushoutShape J')).obj j
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case none
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ none ≅ none
case some J : Type w C : Type u inst : Category.{v, u} C J' : Type w' h : J ≃ J' val✝ : J' ⊢ some val✝ ≅ some val✝
[PROOFSTEP]
repeat rfl
[GOAL]
case none
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ none ≅ none
case some J : Type w C : Type u inst : Category.{v, u} C J' : Type w' h : J ≃ J' val✝ : J' ⊢ some val✝ ≅ some val✝
[PROOFSTEP]
rfl
[GOAL]
case some
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ some val✝ ≅ some val✝
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
X✝ Y✝ : WidePushoutShape J'
f : X✝ ⟶ Y✝
⊢ ((wideSpan none (fun j => some (Equiv.invFun h j)) fun j => Hom.init (Equiv.invFun h j)) ⋙
            wideSpan none (fun j => some (↑h j)) fun j => Hom.init (↑h j)).map
        f ≫
      ((fun j =>
            id
              (Option.casesOn j (id (Iso.refl none)) fun val =>
                Eq.mpr
                  (_ :
                    (Option.rec none (fun val => some (↑h val))
                          (Option.rec none (fun val => some (↑h.symm val)) (some val)) ≅
                        some val) =
                      (some val ≅ some val))
                  (Iso.refl (some val))))
          Y✝).hom =
    ((fun j =>
            id
              (Option.casesOn j (id (Iso.refl none)) fun val =>
                Eq.mpr
                  (_ :
                    (Option.rec none (fun val => some (↑h val))
                          (Option.rec none (fun val => some (↑h.symm val)) (some val)) ≅
                        some val) =
                      (some val ≅ some val))
                  (Iso.refl (some val))))
          X✝).hom ≫
      (𝟭 (WidePushoutShape J')).map f
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
j : J
⊢ π arrows j ≫ arrows j = base arrows
[PROOFSTEP]
apply limit.w (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.Hom.term j)
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
j : J
⊢ lift f fs w ≫ π arrows j = fs j
[PROOFSTEP]
simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
⊢ lift f fs w ≫ base arrows = f
[PROOFSTEP]
simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ (∀ (j : J), g ≫ π arrows j = fs j) → g ≫ base arrows = f → g = lift f fs w
[PROOFSTEP]
intro h1 h2
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ g = lift f fs w
[PROOFSTEP]
apply (limit.isLimit (WidePullbackShape.wideCospan B objs arrows)).uniq (WidePullbackShape.mkCone f fs <| w)
[GOAL]
case x
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ ∀ (j : WidePullbackShape J),
    g ≫ NatTrans.app (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π j =
      NatTrans.app (WidePullbackShape.mkCone f fs w).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case x.none
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ g ≫ NatTrans.app (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π none =
    NatTrans.app (WidePullbackShape.mkCone f fs w).π none
[PROOFSTEP]
apply h2
[GOAL]
case x.some
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
val✝ : J
⊢ g ≫ NatTrans.app (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π (some val✝) =
    NatTrans.app (WidePullbackShape.mkCone f fs w).π (some val✝)
[PROOFSTEP]
apply h1
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type ?u.192408
inst✝¹ : Category.{v₂, ?u.192408} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ ∀ (j : J), (fun j => g ≫ π arrows j) j ≫ arrows j = g ≫ base arrows
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ g = lift (g ≫ base arrows) (fun j => g ≫ π arrows j) (_ : ∀ (j : J), (g ≫ π arrows j) ≫ arrows j = g ≫ base arrows)
[PROOFSTEP]
apply eq_lift_of_comp_eq
[GOAL]
case a
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ ∀ (j : J), g ≫ π arrows j = g ≫ π arrows j
case a
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ g ≫ base arrows = g ≫ base arrows
[PROOFSTEP]
aesop_cat
[GOAL]
case a
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ g ≫ base arrows = g ≫ base arrows
[PROOFSTEP]
rfl
  -- Porting note: quite a few missing refl's in aesop_cat now
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g1 g2 : X ⟶ widePullback B (fun j => objs j) arrows
⊢ (∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j) → g1 ≫ base arrows = g2 ≫ base arrows → g1 = g2
[PROOFSTEP]
intro h1 h2
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g1 g2 : X ⟶ widePullback B (fun j => objs j) arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ g1 = g2
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case w
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g1 g2 : X ⟶ widePullback B (fun j => objs j) arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ ∀ (j : WidePullbackShape J),
    g1 ≫ limit.π (WidePullbackShape.wideCospan B (fun j => objs j) arrows) j =
      g2 ≫ limit.π (WidePullbackShape.wideCospan B (fun j => objs j) arrows) j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case w.none
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g1 g2 : X ⟶ widePullback B (fun j => objs j) arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B (fun j => objs j) arrows) none =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B (fun j => objs j) arrows) none
[PROOFSTEP]
apply h2
[GOAL]
case w.some
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g1 g2 : X ⟶ widePullback B (fun j => objs j) arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
val✝ : J
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B (fun j => objs j) arrows) (some val✝) =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B (fun j => objs j) arrows) (some val✝)
[PROOFSTEP]
apply h1
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
j : J
⊢ arrows j ≫ ι arrows j = head arrows
[PROOFSTEP]
apply colimit.w (WidePushoutShape.wideSpan _ _ _) (WidePushoutShape.Hom.init j)
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
j : J
⊢ ι arrows j ≫ desc f fs w = fs j
[PROOFSTEP]
simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
⊢ head arrows ≫ desc f fs w = f
[PROOFSTEP]
simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g = fs j) → head arrows ≫ g = f → g = desc f fs w
[PROOFSTEP]
intro h1 h2
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ g = desc f fs w
[PROOFSTEP]
apply (colimit.isColimit (WidePushoutShape.wideSpan B objs arrows)).uniq (WidePushoutShape.mkCocone f fs <| w)
[GOAL]
case x
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ ∀ (j : WidePushoutShape J),
    NatTrans.app (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι j ≫ g =
      NatTrans.app (WidePushoutShape.mkCocone f fs w).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case x.none
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ NatTrans.app (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι none ≫ g =
    NatTrans.app (WidePushoutShape.mkCocone f fs w).ι none
[PROOFSTEP]
apply h2
[GOAL]
case x.some
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
val✝ : J
⊢ NatTrans.app (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι (some val✝) ≫ g =
    NatTrans.app (WidePushoutShape.mkCocone f fs w).ι (some val✝)
[PROOFSTEP]
apply h1
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type ?u.203710
inst✝¹ : Category.{v₂, ?u.203710} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
j : J
⊢ arrows j ≫ (fun j => ι arrows j ≫ g) j = head arrows ≫ g
[PROOFSTEP]
rw [← Category.assoc]
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type ?u.203710
inst✝¹ : Category.{v₂, ?u.203710} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g
[PROOFSTEP]
simp
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ g =
    desc (head arrows ≫ g) (fun j => ι arrows j ≫ g)
      (_ : ∀ (j : J), arrows j ≫ (fun j => ι arrows j ≫ g) j = head arrows ≫ g)
[PROOFSTEP]
apply eq_desc_of_comp_eq
[GOAL]
case a
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ ∀ (j : J), ι arrows j ≫ g = ι arrows j ≫ g
case a
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ head arrows ≫ g = head arrows ≫ g
[PROOFSTEP]
aesop_cat
[GOAL]
case a
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B (fun j => objs j) arrows ⟶ X
⊢ head arrows ≫ g = head arrows ≫ g
[PROOFSTEP]
rfl
  -- Porting note: another missing rfl
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2) → head arrows ≫ g1 = head arrows ≫ g2 → g1 = g2
[PROOFSTEP]
intro h1 h2
[GOAL]
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ g1 = g2
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ ∀ (j : WidePushoutShape J),
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) j ≫ g1 =
      colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) j ≫ g2
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case w.none
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) none ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) none ≫ g2
[PROOFSTEP]
apply h2
[GOAL]
case w.some
J : Type w
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v₂, u_1} D
B : D
objs : J → D
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : D
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g1 g2 : widePushout B (fun j => objs j) arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
val✝ : J
⊢ colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) (some val✝) ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B (fun j => objs j) arrows) (some val✝) ≫ g2
[PROOFSTEP]
apply h1
