[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


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ Subobject X ≃o (Subobject (op X))ᵒᵈ
[PROOFSTEP]
refine' OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) _ _
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ OrderHom.comp ↑(cokernelOrderHom X) ↑(kernelOrderHom X) = OrderHom.id
[PROOFSTEP]
change (cokernelOrderHom X).comp (kernelOrderHom X) = _
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X) = OrderHom.id
[PROOFSTEP]
refine' OrderHom.ext _ _ (funext (Subobject.ind _ _))
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : Cᵒᵖ⦄ (f : A ⟶ op X) [inst : Mono f],
    ↑(OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) (Subobject.mk f) = ↑OrderHom.id (Subobject.mk f)
[PROOFSTEP]
intro A f hf
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ↑(OrderHom.comp (cokernelOrderHom X) (kernelOrderHom X)) (Subobject.mk f) = ↑OrderHom.id (Subobject.mk f)
[PROOFSTEP]
dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk, cokernelOrderHom_coe,
  OrderHom.id_coe, id.def]
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Subobject.mk (cokernel.π (kernel.ι f.unop)).op = Subobject.mk f
[PROOFSTEP]
refine' Subobject.mk_eq_mk_of_comm _ _ ⟨_, _, Quiver.Hom.unop_inj _, Quiver.Hom.unop_inj _⟩ _
[GOAL]
case refine'_1.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ op (cokernel (kernel.ι f.unop)) ⟶ A
[PROOFSTEP]
exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op
[GOAL]
case refine'_1.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ A ⟶ op (cokernel (kernel.ι f.unop))
[PROOFSTEP]
exact (cokernel.desc _ _ (kernel.condition f.unop)).op
[GOAL]
case refine'_1.refine'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op ≫
        (cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op).unop =
    (𝟙 (op (cokernel (kernel.ι f.unop)))).unop
[PROOFSTEP]
rw [← cancel_epi (cokernel.π (kernel.ι f.unop))]
[GOAL]
case refine'_1.refine'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ cokernel.π (kernel.ι f.unop) ≫
      ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op ≫
          (cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op).unop =
    cokernel.π (kernel.ι f.unop) ≫ (𝟙 (op (cokernel (kernel.ι f.unop)))).unop
[PROOFSTEP]
simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc, comp_epiDesc, Category.comp_id]
[GOAL]
case refine'_1.refine'_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op ≫
        (epiDesc f.unop (cokernel.π (kernel.ι f.unop))
            (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op).unop =
    (𝟙 A).unop
[PROOFSTEP]
simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc, cokernel.π_desc,
  Category.comp_id]
[GOAL]
case refine'_1.refine'_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ (Iso.mk (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op
          (cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op).hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op
[PROOFSTEP]
exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc])
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((Iso.mk (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) (_ : kernel.ι f.unop ≫ cokernel.π (kernel.ι f.unop) = 0)).op
            (cokernel.desc (kernel.ι f.unop) f.unop (_ : kernel.ι f.unop ≫ f.unop = 0)).op).hom ≫
        f).unop =
    (cokernel.π (kernel.ι f.unop)).op.unop
[PROOFSTEP]
simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ OrderHom.comp ↑(kernelOrderHom X) ↑(cokernelOrderHom X) = OrderHom.id
[PROOFSTEP]
change (kernelOrderHom X).comp (cokernelOrderHom X) = _
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X) = OrderHom.id
[PROOFSTEP]
refine' OrderHom.ext _ _ (funext (Subobject.ind _ _))
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f],
    ↑(OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) (Subobject.mk f) = ↑OrderHom.id (Subobject.mk f)
[PROOFSTEP]
intro A f hf
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ↑(OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) (Subobject.mk f) = ↑OrderHom.id (Subobject.mk f)
[PROOFSTEP]
dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk, kernelOrderHom_coe,
  OrderHom.id_coe, id.def, unop_op, Quiver.Hom.unop_op]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ Subobject.mk (kernel.ι (cokernel.π f)) = Subobject.mk f
[PROOFSTEP]
refine' Subobject.mk_eq_mk_of_comm _ _ ⟨_, _, _, _⟩ _
[GOAL]
case refine'_2.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel (cokernel.π f) ⟶ A
[PROOFSTEP]
exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))
[GOAL]
case refine'_2.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (cokernel.π f)
[PROOFSTEP]
exact kernel.lift _ _ (cokernel.condition f)
[GOAL]
case refine'_2.refine'_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ monoLift f (kernel.ι (cokernel.π f)) (_ : kernel.ι (cokernel.π f) ≫ cokernel.π f = 0) ≫
      kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0) =
    𝟙 (kernel (cokernel.π f))
[PROOFSTEP]
simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp, Category.id_comp]
[GOAL]
case refine'_2.refine'_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0) ≫
      monoLift f (kernel.ι (cokernel.π f)) (_ : kernel.ι (cokernel.π f) ≫ cokernel.π f = 0) =
    𝟙 A
[PROOFSTEP]
simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]
[GOAL]
case refine'_2.refine'_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ (Iso.mk (monoLift f (kernel.ι (cokernel.π f)) (_ : kernel.ι (cokernel.π f) ≫ cokernel.π f = 0))
          (kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0))).hom ≫
      f =
    kernel.ι (cokernel.π f)
[PROOFSTEP]
simp only [monoLift_comp]


[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ (fun a => η.app a ◁ Γ.app a) b ≫ naturality (η ≫ ι) f =
    naturality (η ≫ θ) f ≫ (fun a => η.app a ◁ Γ.app a) a ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ η.app b ◁ Γ.app b ≫
      (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (ι.app b)).inv ≫
        naturality η f ▷ ι.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            η.app a ◁ naturality ι f ≫ (α_ (η.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv =
    ((α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (θ.app b)).inv ≫
        naturality η f ▷ θ.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b)).hom ≫
            η.app a ◁ naturality θ f ≫ (α_ (η.app a) (θ.app a) ((↑H.toPrelaxFunctor).map f)).inv) ≫
      (η.app a ◁ Γ.app a) ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (θ.app b)).inv ≫
      naturality η f ▷ θ.app b ≫
        (η.app a ≫ (↑G.toPrelaxFunctor).map f) ◁ Γ.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            η.app a ◁ naturality ι f ≫ (α_ (η.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv =
    ((α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (θ.app b)).inv ≫
        naturality η f ▷ θ.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b)).hom ≫
            η.app a ◁ naturality θ f ≫ (α_ (η.app a) (θ.app a) ((↑H.toPrelaxFunctor).map f)).inv) ≫
      (η.app a ◁ Γ.app a) ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
simp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ (fun a => Γ.app a ▷ ι.app a) b ≫ naturality (θ ≫ ι) f =
    naturality (η ≫ ι) f ≫ (fun a => Γ.app a ▷ ι.app a) a ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ Γ.app b ▷ ι.app b ≫
      (α_ ((↑F.toPrelaxFunctor).map f) (θ.app b) (ι.app b)).inv ≫
        naturality θ f ▷ ι.app b ≫
          (α_ (θ.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            θ.app a ◁ naturality ι f ≫ (α_ (θ.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv =
    ((α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (ι.app b)).inv ≫
        naturality η f ▷ ι.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            η.app a ◁ naturality ι f ≫ (α_ (η.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv) ≫
      Γ.app a ▷ ι.app a ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
simp_rw [assoc, ← associator_inv_naturality_left, whisker_exchange_assoc]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ Γ.app b ▷ ι.app b ≫
      (α_ ((↑F.toPrelaxFunctor).map f) (θ.app b) (ι.app b)).inv ≫
        naturality θ f ▷ ι.app b ≫
          (α_ (θ.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            θ.app a ◁ naturality ι f ≫ (α_ (θ.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv =
    (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (ι.app b)).inv ≫
      naturality η f ▷ ι.app b ≫
        (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
          Γ.app a ▷ ((↑G.toPrelaxFunctor).map f ≫ ι.app b) ≫
            θ.app a ◁ naturality ι f ≫ (α_ (θ.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv
[PROOFSTEP]
simp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
⊢ ∀ {a b : B} (f : a ⟶ b),
    (↑F.toPrelaxFunctor).map f ◁ ((fun a => α_ (η.app a) (θ.app a) (ι.app a)) b).hom ≫ naturality (η ≫ θ ≫ ι) f =
      naturality ((η ≫ θ) ≫ ι) f ≫ ((fun a => α_ (η.app a) (θ.app a) (ι.app a)) a).hom ▷ (↑I.toPrelaxFunctor).map f
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
⊢ ∀ {a b : B} (f : a ⟶ b),
    (↑F.toPrelaxFunctor).map f ◁ ((fun a => λ_ (η.app a)) b).hom ≫ naturality η f =
      naturality (𝟙 F ≫ η) f ≫ ((fun a => λ_ (η.app a)) a).hom ▷ (↑G.toPrelaxFunctor).map f
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
⊢ ∀ {a b : B} (f : a ⟶ b),
    (↑F.toPrelaxFunctor).map f ◁ ((fun a => ρ_ (η.app a)) b).hom ≫ naturality η f =
      naturality (η ≫ 𝟙 G) f ≫ ((fun a => ρ_ (η.app a)) a).hom ▷ (↑G.toPrelaxFunctor).map f
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : OplaxFunctor B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ (fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) f h i θ ≫
      (fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η i =
    (fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η h ≫
      (fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) g h i θ
[PROOFSTEP]
ext
[GOAL]
case w
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : OplaxFunctor B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
b✝ : B
⊢ ((fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) f h i θ ≫
          (fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η i).app
      b✝ =
    ((fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η h ≫
          (fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) g h i θ).app
      b✝
[PROOFSTEP]
exact whisker_exchange _ _