[GOAL]
J : Type w
X✝ Y✝ : WalkingParallelFamily J
f : X✝ ⟶ Y✝
⊢ f ≫ 𝟙 Y✝ = f
[PROOFSTEP]
cases f
[GOAL]
case id
J : Type w
X✝ : WalkingParallelFamily J
⊢ Hom.id X✝ ≫ 𝟙 X✝ = Hom.id X✝
[PROOFSTEP]
aesop_cat
[GOAL]
case line
J : Type w
x✝ : J
⊢ line x✝ ≫ 𝟙 one = line x✝
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
W✝ X✝ Y✝ Z✝ : WalkingParallelFamily J
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases f
[GOAL]
case id
J : Type w
W✝ Y✝ Z✝ : WalkingParallelFamily J
h : Y✝ ⟶ Z✝
g : W✝ ⟶ Y✝
⊢ (Hom.id W✝ ≫ g) ≫ h = Hom.id W✝ ≫ g ≫ h
[PROOFSTEP]
cases g
[GOAL]
case line
J : Type w
Y✝ Z✝ : WalkingParallelFamily J
h : Y✝ ⟶ Z✝
x✝ : J
g : one ⟶ Y✝
⊢ (line x✝ ≫ g) ≫ h = line x✝ ≫ g ≫ h
[PROOFSTEP]
cases g
[GOAL]
case id.id
J : Type w
W✝ Z✝ : WalkingParallelFamily J
h : W✝ ⟶ Z✝
⊢ (Hom.id W✝ ≫ Hom.id W✝) ≫ h = Hom.id W✝ ≫ Hom.id W✝ ≫ h
[PROOFSTEP]
cases h
[GOAL]
case id.line
J : Type w
Z✝ : WalkingParallelFamily J
x✝ : J
h : one ⟶ Z✝
⊢ (Hom.id zero ≫ line x✝) ≫ h = Hom.id zero ≫ line x✝ ≫ h
[PROOFSTEP]
cases h
[GOAL]
case line.id
J : Type w
Z✝ : WalkingParallelFamily J
x✝ : J
h : one ⟶ Z✝
⊢ (line x✝ ≫ Hom.id one) ≫ h = line x✝ ≫ Hom.id one ≫ h
[PROOFSTEP]
cases h
[GOAL]
case id.id.id
J : Type w
W✝ : WalkingParallelFamily J
⊢ (Hom.id W✝ ≫ Hom.id W✝) ≫ Hom.id W✝ = Hom.id W✝ ≫ Hom.id W✝ ≫ Hom.id W✝
[PROOFSTEP]
aesop_cat
[GOAL]
case id.id.line
J : Type w
x✝ : J
⊢ (Hom.id zero ≫ Hom.id zero) ≫ line x✝ = Hom.id zero ≫ Hom.id zero ≫ line x✝
[PROOFSTEP]
aesop_cat
[GOAL]
case id.line.id
J : Type w
x✝ : J
⊢ (Hom.id zero ≫ line x✝) ≫ Hom.id one = Hom.id zero ≫ line x✝ ≫ Hom.id one
[PROOFSTEP]
aesop_cat
[GOAL]
case line.id.id
J : Type w
x✝ : J
⊢ (line x✝ ≫ Hom.id one) ≫ Hom.id one = line x✝ ≫ Hom.id one ≫ Hom.id one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ {X_1 Y_1 Z : WalkingParallelFamily J} (f_1 : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    { obj := fun x => WalkingParallelFamily.casesOn x X Y,
            map := fun {x y} h =>
              match x, y, h with
              | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
              | .(zero), .(one), line j => f j }.map
        (f_1 ≫ g) =
      { obj := fun x => WalkingParallelFamily.casesOn x X Y,
              map := fun {x y} h =>
                match x, y, h with
                | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
                | .(zero), .(one), line j => f j }.map
          f_1 ≫
        { obj := fun x => WalkingParallelFamily.casesOn x X Y,
              map := fun {x y} h =>
                match x, y, h with
                | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
                | .(zero), .(one), line j => f j }.map
          g
[PROOFSTEP]
rintro _ _ _ ⟨⟩ ⟨⟩
[GOAL]
case id.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily J
⊢ { obj := fun x => WalkingParallelFamily.casesOn x X Y,
          map := fun {x y} h =>
            match x, y, h with
            | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
            | .(zero), .(one), line j => f j }.map
      (Hom.id X✝ ≫ Hom.id X✝) =
    { obj := fun x => WalkingParallelFamily.casesOn x X Y,
            map := fun {x y} h =>
              match x, y, h with
              | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
              | .(zero), .(one), line j => f j }.map
        (Hom.id X✝) ≫
      { obj := fun x => WalkingParallelFamily.casesOn x X Y,
            map := fun {x y} h =>
              match x, y, h with
              | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
              | .(zero), .(one), line j => f j }.map
        (Hom.id X✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case id.line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
x✝ : J
⊢ { obj := fun x => WalkingParallelFamily.casesOn x X Y,
          map := fun {x y} h =>
            match x, y, h with
            | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
            | .(zero), .(one), line j => f j }.map
      (Hom.id zero ≫ line x✝) =
    { obj := fun x => WalkingParallelFamily.casesOn x X Y,
            map := fun {x y} h =>
              match x, y, h with
              | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
              | .(zero), .(one), line j => f j }.map
        (Hom.id zero) ≫
      { obj := fun x => WalkingParallelFamily.casesOn x X Y,
            map := fun {x y} h =>
              match x, y, h with
              | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
              | .(zero), .(one), line j => f j }.map
        (line x✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case line.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
x✝ : J
⊢ { obj := fun x => WalkingParallelFamily.casesOn x X Y,
          map := fun {x y} h =>
            match x, y, h with
            | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
            | .(zero), .(one), line j => f j }.map
      (line x✝ ≫ Hom.id one) =
    { obj := fun x => WalkingParallelFamily.casesOn x X Y,
            map := fun {x y} h =>
              match x, y, h with
              | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
              | .(zero), .(one), line j => f j }.map
        (line x✝) ≫
      { obj := fun x => WalkingParallelFamily.casesOn x X Y,
            map := fun {x y} h =>
              match x, y, h with
              | x, .(x), Hom.id .(x) => 𝟙 ((fun x => WalkingParallelFamily.casesOn x X Y) x)
              | .(zero), .(one), line j => f j }.map
        (Hom.id one)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j => F.map (line j)).obj j
[PROOFSTEP]
cases j
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ F.obj zero = (parallelFamily fun j => F.map (line j)).obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ F.obj one = (parallelFamily fun j => F.map (line j)).obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ ∀ {X Y : WalkingParallelFamily J} (f : X ⟶ Y),
    F.map f ≫ ((fun j => eqToIso (_ : F.obj j = (parallelFamily fun j => F.map (line j)).obj j)) Y).hom =
      ((fun j => eqToIso (_ : F.obj j = (parallelFamily fun j => F.map (line j)).obj j)) X).hom ≫
        (parallelFamily fun j => F.map (line j)).map f
[PROOFSTEP]
rintro _ _ (_ | _)
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
X✝ : WalkingParallelFamily J
⊢ F.map (Hom.id X✝) ≫ ((fun j => eqToIso (_ : F.obj j = (parallelFamily fun j => F.map (line j)).obj j)) X✝).hom =
    ((fun j => eqToIso (_ : F.obj j = (parallelFamily fun j => F.map (line j)).obj j)) X✝).hom ≫
      (parallelFamily fun j => F.map (line j)).map (Hom.id X✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
x✝ : J
⊢ F.map (line x✝) ≫ ((fun j => eqToIso (_ : F.obj j = (parallelFamily fun j => F.map (line j)).obj j)) one).hom =
    ((fun j => eqToIso (_ : F.obj j = (parallelFamily fun j => F.map (line j)).obj j)) zero).hom ≫
      (parallelFamily fun j => F.map (line j)).map (line x✝)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
X : WalkingParallelFamily (ULift Bool)
⊢ (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
    ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      X
[PROOFSTEP]
cases X
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift Bool))).obj zero =
    ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      zero
[PROOFSTEP]
rfl
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift Bool))).obj one =
    ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      one
[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ {X Y : WalkingParallelFamily (ULift Bool)} (f : X ⟶ Y),
    (𝟭 (WalkingParallelFamily (ULift Bool))).map f ≫
        ((fun X =>
              eqToIso
                (_ :
                  (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                    ((parallelFamily fun p =>
                            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                          parallelPair (line { down := true }) (line { down := false })).obj
                      X))
            Y).hom =
      ((fun X =>
              eqToIso
                (_ :
                  (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                    ((parallelFamily fun p =>
                            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                          parallelPair (line { down := true }) (line { down := false })).obj
                      X))
            X).hom ≫
        ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
              parallelPair (line { down := true }) (line { down := false })).map
          f
[PROOFSTEP]
rintro _ _ (_ | ⟨_ | _⟩)
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily (ULift Bool)
⊢ (𝟭 (WalkingParallelFamily (ULift Bool))).map (Hom.id X✝) ≫
      ((fun X =>
            eqToIso
              (_ :
                (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                  ((parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                        parallelPair (line { down := true }) (line { down := false })).obj
                    X))
          X✝).hom =
    ((fun X =>
            eqToIso
              (_ :
                (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                  ((parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                        parallelPair (line { down := true }) (line { down := false })).obj
                    X))
          X✝).hom ≫
      ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (Hom.id X✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case line.up.false
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift Bool))).map (line { down := false }) ≫
      ((fun X =>
            eqToIso
              (_ :
                (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                  ((parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                        parallelPair (line { down := true }) (line { down := false })).obj
                    X))
          one).hom =
    ((fun X =>
            eqToIso
              (_ :
                (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                  ((parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                        parallelPair (line { down := true }) (line { down := false })).obj
                    X))
          zero).hom ≫
      ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (line { down := false })
[PROOFSTEP]
aesop_cat
[GOAL]
case line.up.true
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift Bool))).map (line { down := true }) ≫
      ((fun X =>
            eqToIso
              (_ :
                (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                  ((parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                        parallelPair (line { down := true }) (line { down := false })).obj
                    X))
          one).hom =
    ((fun X =>
            eqToIso
              (_ :
                (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                  ((parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                        parallelPair (line { down := true }) (line { down := false })).obj
                    X))
          zero).hom ≫
      ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (line { down := true })
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
X : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      X =
    (𝟭 WalkingParallelPair).obj X
[PROOFSTEP]
cases X
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.zero =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.zero
[PROOFSTEP]
rfl
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.one =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.one
[PROOFSTEP]
rfl
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    (parallelPair (line { down := true }) (line { down := false }) ⋙
              parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
          f ≫
        ((fun X =>
              eqToIso
                (_ :
                  (parallelPair (line { down := true }) (line { down := false }) ⋙
                          parallelFamily fun p =>
                            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                      X =
                    (𝟭 WalkingParallelPair).obj X))
            Y).hom =
      ((fun X =>
              eqToIso
                (_ :
                  (parallelPair (line { down := true }) (line { down := false }) ⋙
                          parallelFamily fun p =>
                            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                      X =
                    (𝟭 WalkingParallelPair).obj X))
            X).hom ≫
        (𝟭 WalkingParallelPair).map f
[PROOFSTEP]
rintro _ _ (_ | _ | _)
[GOAL]
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.left ≫
      ((fun X =>
            eqToIso
              (_ :
                (parallelPair (line { down := true }) (line { down := false }) ⋙
                        parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                    X =
                  (𝟭 WalkingParallelPair).obj X))
          WalkingParallelPair.one).hom =
    ((fun X =>
            eqToIso
              (_ :
                (parallelPair (line { down := true }) (line { down := false }) ⋙
                        parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                    X =
                  (𝟭 WalkingParallelPair).obj X))
          WalkingParallelPair.zero).hom ≫
      (𝟭 WalkingParallelPair).map WalkingParallelPairHom.left
[PROOFSTEP]
aesop_cat
[GOAL]
case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.right ≫
      ((fun X =>
            eqToIso
              (_ :
                (parallelPair (line { down := true }) (line { down := false }) ⋙
                        parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                    X =
                  (𝟭 WalkingParallelPair).obj X))
          WalkingParallelPair.one).hom =
    ((fun X =>
            eqToIso
              (_ :
                (parallelPair (line { down := true }) (line { down := false }) ⋙
                        parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                    X =
                  (𝟭 WalkingParallelPair).obj X))
          WalkingParallelPair.zero).hom ≫
      (𝟭 WalkingParallelPair).map WalkingParallelPairHom.right
[PROOFSTEP]
aesop_cat
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        (WalkingParallelPairHom.id X✝) ≫
      ((fun X =>
            eqToIso
              (_ :
                (parallelPair (line { down := true }) (line { down := false }) ⋙
                        parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                    X =
                  (𝟭 WalkingParallelPair).obj X))
          X✝).hom =
    ((fun X =>
            eqToIso
              (_ :
                (parallelPair (line { down := true }) (line { down := false }) ⋙
                        parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                    X =
                  (𝟭 WalkingParallelPair).obj X))
          X✝).hom ≫
      (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ (X : WalkingParallelFamily (ULift Bool)),
    (parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
          (NatTrans.app
            (NatIso.ofComponents fun X =>
                eqToIso
                  (_ :
                    (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                      ((parallelFamily fun p =>
                              bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                            parallelPair (line { down := true }) (line { down := false })).obj
                        X)).hom
            X) ≫
        NatTrans.app
          (NatIso.ofComponents fun X =>
              eqToIso
                (_ :
                  (parallelPair (line { down := true }) (line { down := false }) ⋙
                          parallelFamily fun p =>
                            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                      X =
                    (𝟭 WalkingParallelPair).obj X)).hom
          ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
            X) =
      𝟙 ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj X)
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        (NatTrans.app
          (NatIso.ofComponents fun X =>
              eqToIso
                (_ :
                  (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                    ((parallelFamily fun p =>
                            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                          parallelPair (line { down := true }) (line { down := false })).obj
                      X)).hom
          zero) ≫
      NatTrans.app
        (NatIso.ofComponents fun X =>
            eqToIso
              (_ :
                (parallelPair (line { down := true }) (line { down := false }) ⋙
                        parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                    X =
                  (𝟭 WalkingParallelPair).obj X)).hom
        ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          zero) =
    𝟙 ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj zero)
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        (NatTrans.app
          (NatIso.ofComponents fun X =>
              eqToIso
                (_ :
                  (𝟭 (WalkingParallelFamily (ULift Bool))).obj X =
                    ((parallelFamily fun p =>
                            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
                          parallelPair (line { down := true }) (line { down := false })).obj
                      X)).hom
          one) ≫
      NatTrans.app
        (NatIso.ofComponents fun X =>
            eqToIso
              (_ :
                (parallelPair (line { down := true }) (line { down := false }) ⋙
                        parallelFamily fun p =>
                          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
                    X =
                  (𝟭 WalkingParallelPair).obj X)).hom
        ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          one) =
    𝟙 ((parallelFamily fun p => bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj one)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Trident f
j : J
⊢ NatTrans.app s.π zero ≫ f j = NatTrans.app s.π one
[PROOFSTEP]
rw [← s.w (line j), parallelFamily_map_left]
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
⊢ f j ≫ NatTrans.app s.ι one = NatTrans.app s.ι zero
[PROOFSTEP]
rw [← s.w (line j), parallelFamily_map_left]
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f✝ j₁ = ι ≫ f✝ j₂
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map f ≫
      (fun X_1 => WalkingParallelFamily.casesOn X_1 ι (ι ≫ f✝ (Classical.arbitrary J))) j =
    (fun X_1 => WalkingParallelFamily.casesOn X_1 ι (ι ≫ f✝ (Classical.arbitrary J))) i ≫ (parallelFamily f✝).map f
[PROOFSTEP]
dsimp
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f✝ j₁ = ι ≫ f✝ j₂
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ 𝟙 P ≫ WalkingParallelFamily.rec ι (ι ≫ f✝ (Classical.arbitrary J)) j =
    WalkingParallelFamily.rec ι (ι ≫ f✝ (Classical.arbitrary J)) i ≫ (parallelFamily f✝).map f
[PROOFSTEP]
cases' f with _ k
[GOAL]
case id
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂
i : WalkingParallelFamily J
⊢ 𝟙 P ≫ WalkingParallelFamily.rec ι (ι ≫ f (Classical.arbitrary J)) i =
    WalkingParallelFamily.rec ι (ι ≫ f (Classical.arbitrary J)) i ≫ (parallelFamily f).map (Hom.id i)
[PROOFSTEP]
simp
[GOAL]
case line
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂
k : J
⊢ 𝟙 P ≫ WalkingParallelFamily.rec ι (ι ≫ f (Classical.arbitrary J)) one =
    WalkingParallelFamily.rec ι (ι ≫ f (Classical.arbitrary J)) zero ≫ (parallelFamily f).map (line k)
[PROOFSTEP]
simp [w (Classical.arbitrary J) k]
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f✝ j₁ ≫ π = f✝ j₂ ≫ π
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ (parallelFamily f✝).map f ≫ (fun X_1 => WalkingParallelFamily.casesOn X_1 (f✝ (Classical.arbitrary J) ≫ π) π) j =
    (fun X_1 => WalkingParallelFamily.casesOn X_1 (f✝ (Classical.arbitrary J) ≫ π) π) i ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map f
[PROOFSTEP]
dsimp
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f✝ j₁ ≫ π = f✝ j₂ ≫ π
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ (parallelFamily f✝).map f ≫ WalkingParallelFamily.rec (f✝ (Classical.arbitrary J) ≫ π) π j =
    WalkingParallelFamily.rec (f✝ (Classical.arbitrary J) ≫ π) π i ≫ 𝟙 P
[PROOFSTEP]
cases' f with _ k
[GOAL]
case id
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
i : WalkingParallelFamily J
⊢ (parallelFamily f).map (Hom.id i) ≫ WalkingParallelFamily.rec (f (Classical.arbitrary J) ≫ π) π i =
    WalkingParallelFamily.rec (f (Classical.arbitrary J) ≫ π) π i ≫ 𝟙 P
[PROOFSTEP]
simp
[GOAL]
case line
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
k : J
⊢ (parallelFamily f).map (line k) ≫ WalkingParallelFamily.rec (f (Classical.arbitrary J) ≫ π) π one =
    WalkingParallelFamily.rec (f (Classical.arbitrary J) ≫ π) π zero ≫ 𝟙 P
[PROOFSTEP]
simp [w (Classical.arbitrary J) k]
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Trident f
⊢ ι t ≫ f j₁ = ι t ≫ f j₂
[PROOFSTEP]
rw [t.app_zero, t.app_zero]
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Cotrident f
⊢ f j₁ ≫ π t = f j₂ ≫ π t
[PROOFSTEP]
rw [t.app_one, t.app_one]
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ ι s = l ≫ ι s
⊢ k ≫ NatTrans.app s.π one = l ≫ NatTrans.app s.π one
[PROOFSTEP]
rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : π s ≫ k = π s ≫ l
⊢ NatTrans.app s.ι zero ≫ k = NatTrans.app s.ι zero ≫ l
[PROOFSTEP]
rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ ι t = ι s
uniq :
  ∀ (s : Trident f) (m : s.pt ⟶ t.pt),
    (∀ (j : WalkingParallelFamily J), m ≫ NatTrans.app t.π j = NatTrans.app s.π j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
⊢ lift s ≫ NatTrans.app t.π one = NatTrans.app s.π one
[PROOFSTEP]
rw [← t.w (line (Classical.arbitrary J)), reassoc_of% fac, s.w]
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), π t ≫ desc s = π s
uniq :
  ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt),
    (∀ (j : WalkingParallelFamily J), NatTrans.app t.ι j ≫ m = NatTrans.app s.ι j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
⊢ NatTrans.app t.ι zero ≫ desc s = NatTrans.app s.ι zero
[PROOFSTEP]
rw [← t.w_assoc (line (Classical.arbitrary J)), fac, s.w]
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Trident f
ht : IsLimit t
Z : C
k : Z ⟶ t.pt
⊢ ∀ (j₁ j₂ : J), (k ≫ ι t) ≫ f j₁ = (k ≫ ι t) ≫ f j₂
[PROOFSTEP]
simp
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Cotrident f
ht : IsColimit t
Z : C
k : t.pt ⟶ Z
⊢ ∀ (j₁ j₂ : J), f j₁ ≫ π t ≫ k = f j₂ ≫ π t ≫ k
[PROOFSTEP]
simp
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
X : WalkingParallelFamily J
⊢ (parallelFamily fun j => F.map (line j)).obj X = F.obj X
[PROOFSTEP]
cases X
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
⊢ (parallelFamily fun j => F.map (line j)).obj zero = F.obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
⊢ (parallelFamily fun j => F.map (line j)).obj one = F.obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map g ≫
      (fun X => NatTrans.app t.π X ≫ eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X)) j' =
    (fun X => NatTrans.app t.π X ≫ eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X)) j ≫ F.map g
[PROOFSTEP]
cases g
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
j : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j) ≫
      (fun X => NatTrans.app t.π X ≫ eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X)) j =
    (fun X => NatTrans.app t.π X ≫ eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X)) j ≫
      F.map (Hom.id j)
[PROOFSTEP]
aesop_cat
[GOAL]
case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
x✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line x✝) ≫
      (fun X => NatTrans.app t.π X ≫ eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X)) one =
    (fun X => NatTrans.app t.π X ≫ eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X)) zero ≫
      F.map (line x✝)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
X : WalkingParallelFamily J
⊢ F.obj X = (parallelFamily fun j => F.map (line j)).obj X
[PROOFSTEP]
cases X
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
⊢ F.obj zero = (parallelFamily fun j => F.map (line j)).obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
⊢ F.obj one = (parallelFamily fun j => F.map (line j)).obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ F.map g ≫ (fun X => eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X) ≫ NatTrans.app t.ι X) j' =
    (fun X => eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X) ≫ NatTrans.app t.ι X) j ≫
      ((Functor.const (WalkingParallelFamily J)).obj t.pt).map g
[PROOFSTEP]
cases g
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
j : WalkingParallelFamily J
⊢ F.map (Hom.id j) ≫
      (fun X => eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X) ≫ NatTrans.app t.ι X) j =
    (fun X => eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X) ≫ NatTrans.app t.ι X) j ≫
      ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j)
[PROOFSTEP]
dsimp
[GOAL]
case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
x✝ : J
⊢ F.map (line x✝) ≫
      (fun X => eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X) ≫ NatTrans.app t.ι X) one =
    (fun X => eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X) ≫ NatTrans.app t.ι X) zero ≫
      ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line x✝)
[PROOFSTEP]
dsimp
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
j : WalkingParallelFamily J
⊢ F.map (𝟙 j) ≫ eqToHom (_ : F.obj j = (parallelFamily fun j => F.map (line j)).obj j) ≫ NatTrans.app t.ι j =
    (eqToHom (_ : F.obj j = (parallelFamily fun j => F.map (line j)).obj j) ≫ NatTrans.app t.ι j) ≫ 𝟙 t.pt
[PROOFSTEP]
simp [Cotrident.app_one t]
[GOAL]
case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
x✝ : J
⊢ F.map (line x✝) ≫ 𝟙 (F.obj one) ≫ NatTrans.app t.ι one = (𝟙 (F.obj zero) ≫ NatTrans.app t.ι zero) ≫ 𝟙 t.pt
[PROOFSTEP]
simp [Cotrident.app_one t]
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
j : WalkingParallelFamily J
⊢ (parallelFamily fun j => F.map (line j)).obj j = F.obj j
[PROOFSTEP]
cases j
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
⊢ (parallelFamily fun j => F.map (line j)).obj zero = F.obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
⊢ (parallelFamily fun j => F.map (line j)).obj one = F.obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j => F.map (line j)).obj j
[PROOFSTEP]
cases j
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
⊢ F.obj zero = (parallelFamily fun j => F.map (line j)).obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j => F.map (line j)
⊢ F.obj one = (parallelFamily fun j => F.map (line j)).obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
X : WalkingParallelFamily J
⊢ F.obj X = (parallelFamily fun j => F.map (line j)).obj X
[PROOFSTEP]
cases X
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj zero = (parallelFamily fun j => F.map (line j)).obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj one = (parallelFamily fun j => F.map (line j)).obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ ∀ ⦃X Y : WalkingParallelFamily J⦄ (f : X ⟶ Y),
    ((Functor.const (WalkingParallelFamily J)).obj t.pt).map f ≫
        (fun X => NatTrans.app t.π X ≫ eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X)) Y =
      (fun X => NatTrans.app t.π X ≫ eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X)) X ≫
        (parallelFamily fun j => F.map (line j)).map f
[PROOFSTEP]
rintro _ _ (_ | _)
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
X✝ : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id X✝) ≫
      (fun X => NatTrans.app t.π X ≫ eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X)) X✝ =
    (fun X => NatTrans.app t.π X ≫ eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X)) X✝ ≫
      (parallelFamily fun j => F.map (line j)).map (Hom.id X✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
x✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line x✝) ≫
      (fun X => NatTrans.app t.π X ≫ eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X)) one =
    (fun X => NatTrans.app t.π X ≫ eqToHom (_ : F.obj X = (parallelFamily fun j => F.map (line j)).obj X)) zero ≫
      (parallelFamily fun j => F.map (line j)).map (line x✝)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
X : WalkingParallelFamily J
⊢ (parallelFamily fun j => F.map (line j)).obj X = F.obj X
[PROOFSTEP]
cases X
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j => F.map (line j)).obj zero = F.obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j => F.map (line j)).obj one = F.obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ ∀ ⦃X Y : WalkingParallelFamily J⦄ (f : X ⟶ Y),
    (parallelFamily fun j => F.map (line j)).map f ≫
        (fun X => eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X) ≫ NatTrans.app t.ι X) Y =
      (fun X => eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X) ≫ NatTrans.app t.ι X) X ≫
        ((Functor.const (WalkingParallelFamily J)).obj t.pt).map f
[PROOFSTEP]
rintro _ _ (_ | _)
[GOAL]
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
X✝ : WalkingParallelFamily J
⊢ (parallelFamily fun j => F.map (line j)).map (Hom.id X✝) ≫
      (fun X => eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X) ≫ NatTrans.app t.ι X) X✝ =
    (fun X => eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X) ≫ NatTrans.app t.ι X) X✝ ≫
      ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id X✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
x✝ : J
⊢ (parallelFamily fun j => F.map (line j)).map (line x✝) ≫
      (fun X => eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X) ≫ NatTrans.app t.ι X) one =
    (fun X => eqToHom (_ : (parallelFamily fun j => F.map (line j)).obj X = F.obj X) ≫ NatTrans.app t.ι X) zero ≫
      ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line x✝)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j => F.map (line j)).obj j
[PROOFSTEP]
cases j
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj zero = (parallelFamily fun j => F.map (line j)).obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj one = (parallelFamily fun j => F.map (line j)).obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
j : WalkingParallelFamily J
⊢ (parallelFamily fun j => F.map (line j)).obj j = F.obj j
[PROOFSTEP]
cases j
[GOAL]
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j => F.map (line j)).obj zero = F.obj zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j => F.map (line j)).obj one = F.obj one
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : autoParam (k ≫ ι t = ι s) _auto✝
⊢ ∀ (j : WalkingParallelFamily J), k ≫ NatTrans.app t.π j = NatTrans.app s.π j
[PROOFSTEP]
rintro ⟨_ | _⟩
[GOAL]
case zero
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : autoParam (k ≫ ι t = ι s) _auto✝
⊢ k ≫ NatTrans.app t.π zero = NatTrans.app s.π zero
[PROOFSTEP]
exact w
[GOAL]
case one
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : autoParam (k ≫ ι t = ι s) _auto✝
⊢ k ≫ NatTrans.app t.π one = NatTrans.app s.π one
[PROOFSTEP]
simpa using w =≫ f (Classical.arbitrary J)
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
i : s.pt ≅ t.pt
w : autoParam (i.hom ≫ ι t = ι s) _auto✝
⊢ i.inv ≫ ι s = ι t
[PROOFSTEP]
rw [← w, Iso.inv_hom_id_assoc]
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : autoParam (π s ≫ k = π t) _auto✝
⊢ ∀ (j : WalkingParallelFamily J), NatTrans.app s.ι j ≫ k = NatTrans.app t.ι j
[PROOFSTEP]
rintro ⟨_ | _⟩
[GOAL]
case zero
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : autoParam (π s ≫ k = π t) _auto✝
⊢ NatTrans.app s.ι zero ≫ k = NatTrans.app t.ι zero
[PROOFSTEP]
simpa using f (Classical.arbitrary J) ≫= w
[GOAL]
case one
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : autoParam (π s ≫ k = π t) _auto✝
⊢ NatTrans.app s.ι one ≫ k = NatTrans.app t.ι one
[PROOFSTEP]
exact w
[GOAL]
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
i : s.pt ≅ t.pt
w : autoParam (π s ≫ i.hom = π t) _auto✝
⊢ π t ≫ i.inv = π s
[PROOFSTEP]
rw [Iso.comp_inv_eq, w]


[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
⊢ Mono (F.map f)
[PROOFSTEP]
have := isLimitPullbackConeMapOfIsLimit F _ (PullbackCone.isLimitMkIdId f)
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this :
  let_fun this := (_ : F.map (𝟙 X) ≫ F.map f = F.map (𝟙 X) ≫ F.map f);
  IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)
⊢ Mono (F.map f)
[PROOFSTEP]
simp_rw [F.map_id] at this
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) (_ : 𝟙 (F.obj X) ≫ F.map f = 𝟙 (F.obj X) ≫ F.map f))
⊢ Mono (F.map f)
[PROOFSTEP]
apply PullbackCone.mono_of_isLimitMkIdId _ this
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
⊢ Mono f
[PROOFSTEP]
have := PullbackCone.isLimitMkIdId (F.map f)
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) (_ : 𝟙 (F.obj X) ≫ F.map f = 𝟙 (F.obj X) ≫ F.map f))
⊢ Mono f
[PROOFSTEP]
simp_rw [← F.map_id] at this
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) (_ : F.map (𝟙 X) ≫ F.map f = F.map (𝟙 X) ≫ F.map f))
⊢ Mono f
[PROOFSTEP]
apply PullbackCone.mono_of_isLimitMkIdId _ (isLimitOfIsLimitPullbackConeMap F _ this)
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
⊢ Epi (F.map f)
[PROOFSTEP]
have := isColimitPushoutCoconeMapOfIsColimit F _ (PushoutCocone.isColimitMkIdId f)
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) (_ : F.map f ≫ F.map (𝟙 Y) = F.map f ≫ F.map (𝟙 Y)))
⊢ Epi (F.map f)
[PROOFSTEP]
simp_rw [F.map_id] at this
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) (_ : F.map f ≫ 𝟙 (F.obj Y) = F.map f ≫ 𝟙 (F.obj Y)))
⊢ Epi (F.map f)
[PROOFSTEP]
apply PushoutCocone.epi_of_isColimitMkIdId _ this
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
⊢ Epi f
[PROOFSTEP]
have := PushoutCocone.isColimitMkIdId (F.map f)
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) (_ : F.map f ≫ 𝟙 (F.obj Y) = F.map f ≫ 𝟙 (F.obj Y)))
⊢ Epi f
[PROOFSTEP]
simp_rw [← F.map_id] at this
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) (_ : F.map f ≫ F.map (𝟙 Y) = F.map f ≫ F.map (𝟙 Y)))
⊢ Epi f
[PROOFSTEP]
apply PushoutCocone.epi_of_isColimitMkIdId _ (isColimitOfIsColimitPushoutCoconeMap F _ this)


[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type ?u.69019
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ f j = f j'
[PROOFSTEP]
simp [w]
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom (_ : f j = f j') = π f j'
[PROOFSTEP]
cases w
[GOAL]
case refl
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j : J
⊢ π f j ≫ eqToHom (_ : f j = f j) = π f j
[PROOFSTEP]
simp
  -- The `simpNF` linter incorrectly identifies these as simp lemmas that could never apply.
  -- https://github.com/leanprover-community/mathlib4/issues/5049
  -- They are used by `simp` in `Sigma.whisker_equiv` below.
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type ?u.69987
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ f j = f j'
[PROOFSTEP]
simp [w]
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ eqToHom (_ : f j = f j') ≫ ι f j' = ι f j
[PROOFSTEP]
cases w
[GOAL]
case refl
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j : J
⊢ eqToHom (_ : f j = f j) ≫ ι f j = ι f j
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
f g : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Mono (p i)
⊢ ∀ (j : Discrete β), Mono (NatTrans.app (Discrete.natTrans fun X => p X.as) j)
[PROOFSTEP]
dsimp
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
f g : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Mono (p i)
⊢ ∀ (j : Discrete β), Mono (p j.as)
[PROOFSTEP]
infer_instance
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
f g : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Epi (p i)
⊢ ∀ (j : Discrete β), Epi (NatTrans.app (Discrete.natTrans fun X => p X.as) j)
[PROOFSTEP]
dsimp
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
f g : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Epi (p i)
⊢ ∀ (j : Discrete β), Epi (p j.as)
[PROOFSTEP]
infer_instance
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
J : Type ?u.78866
K : Type ?u.78950
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (↑e j) ≅ f j
inst✝¹ : HasProduct f
inst✝ : HasProduct g
k : K
⊢ g (↑e (↑e.symm k)) = g k
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
J : Type ?u.94443
K : Type ?u.94527
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (↑e j) ≅ f j
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
k : K
⊢ g k = g (↑e (↑e.symm k))
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
⊢ G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j)
[PROOFSTEP]
ext j
[GOAL]
case h
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
j : β
⊢ (G.map (Pi.lift g) ≫ piComparison G f) ≫ Pi.π (fun b => G.obj (f b)) j =
    (Pi.lift fun j => G.map (g j)) ≫ Pi.π (fun b => G.obj (f b)) j
[PROOFSTEP]
simp only [Discrete.functor_obj, Category.assoc, piComparison_comp_π, ← G.map_comp, limit.lift_π, Fan.mk_pt,
  Fan.mk_π_app]
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b => G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
⊢ sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j)
[PROOFSTEP]
ext j
[GOAL]
case h
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b => G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
j : β
⊢ Sigma.ι (fun b => G.obj (f b)) j ≫ sigmaComparison G f ≫ G.map (Sigma.desc g) =
    Sigma.ι (fun b => G.obj (f b)) j ≫ Sigma.desc fun j => G.map (g j)
[PROOFSTEP]
simp only [Discrete.functor_obj, ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc, Cofan.mk_pt,
  Cofan.mk_ι_app]
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ ((Functor.const (Discrete β)).obj (f default)).obj { as := j } = (Discrete.functor f).obj { as := j }
[PROOFSTEP]
dsimp
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ f default = f j
[PROOFSTEP]
congr
[GOAL]
case e_a
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ default = j
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
j : Discrete β
⊢ (fun s => NatTrans.app s.π default) s ≫
      NatTrans.app
        { pt := f default,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                        (Discrete.functor f).obj { as := j }) }.π
        j =
    NatTrans.app s.π j
[PROOFSTEP]
have h := Subsingleton.elim j default
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
j : Discrete β
h : j = default
⊢ (fun s => NatTrans.app s.π default) s ≫
      NatTrans.app
        { pt := f default,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                        (Discrete.functor f).obj { as := j }) }.π
        j =
    NatTrans.app s.π j
[PROOFSTEP]
subst h
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
⊢ (fun s => NatTrans.app s.π default) s ≫
      NatTrans.app
        { pt := f default,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                        (Discrete.functor f).obj { as := j }) }.π
        default =
    NatTrans.app s.π default
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                    (Discrete.functor f).obj { as := j }) }.pt
w :
  ∀ (j : Discrete β),
    m ≫
        NatTrans.app
          { pt := f default,
              π :=
                Discrete.natTrans fun x =>
                  match x with
                  | { as := j } =>
                    eqToHom
                      (_ :
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                          (Discrete.functor f).obj { as := j }) }.π
          j =
      NatTrans.app s.π j
⊢ m = (fun s => NatTrans.app s.π default) s
[PROOFSTEP]
specialize w default
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                    (Discrete.functor f).obj { as := j }) }.pt
w :
  m ≫
      NatTrans.app
        { pt := f default,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                        (Discrete.functor f).obj { as := j }) }.π
        default =
    NatTrans.app s.π default
⊢ m = (fun s => NatTrans.app s.π default) s
[PROOFSTEP]
simpa using w
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ (Discrete.functor f).obj { as := j } = ((Functor.const (Discrete β)).obj (f default)).obj { as := j }
[PROOFSTEP]
dsimp
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ f j = f default
[PROOFSTEP]
congr
[GOAL]
case e_a
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ j = default
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
j : Discrete β
⊢ NatTrans.app
        { pt := f default,
            ι :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      (Discrete.functor f).obj { as := j } =
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
        j ≫
      (fun s => NatTrans.app s.ι default) s =
    NatTrans.app s.ι j
[PROOFSTEP]
have h := Subsingleton.elim j default
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
j : Discrete β
h : j = default
⊢ NatTrans.app
        { pt := f default,
            ι :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      (Discrete.functor f).obj { as := j } =
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
        j ≫
      (fun s => NatTrans.app s.ι default) s =
    NatTrans.app s.ι j
[PROOFSTEP]
subst h
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
⊢ NatTrans.app
        { pt := f default,
            ι :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      (Discrete.functor f).obj { as := j } =
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
        default ≫
      (fun s => NatTrans.app s.ι default) s =
    NatTrans.app s.ι default
[PROOFSTEP]
apply Category.id_comp
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  (Discrete.functor f).obj { as := j } =
                    ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete β),
    NatTrans.app
          { pt := f default,
              ι :=
                Discrete.natTrans fun x =>
                  match x with
                  | { as := j } =>
                    eqToHom
                      (_ :
                        (Discrete.functor f).obj { as := j } =
                          ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
          j ≫
        m =
      NatTrans.app s.ι j
⊢ m = (fun s => NatTrans.app s.ι default) s
[PROOFSTEP]
specialize w default
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  (Discrete.functor f).obj { as := j } =
                    ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.pt ⟶
    s.pt
w :
  NatTrans.app
        { pt := f default,
            ι :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      (Discrete.functor f).obj { as := j } =
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
        default ≫
      m =
    NatTrans.app s.ι default
⊢ m = (fun s => NatTrans.app s.ι default) s
[PROOFSTEP]
erw [Category.id_comp] at w
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  (Discrete.functor f).obj { as := j } =
                    ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.pt ⟶
    s.pt
w : m = NatTrans.app s.ι default
⊢ m = (fun s => NatTrans.app s.ι default) s
[PROOFSTEP]
exact w
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ↑ε)
b : β
⊢ (reindex ε f).hom ≫ π f (↑ε b) = π (f ∘ ↑ε) b
[PROOFSTEP]
dsimp [Pi.reindex]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ↑ε)
b : β
⊢ (HasLimit.isoOfEquivalence (Discrete.equivalence ε)
          (Discrete.natIso fun x =>
            Iso.refl ((Discrete.functor f).obj ((Discrete.functor (Discrete.mk ∘ ↑ε)).obj x)))).hom ≫
      π f (↑ε b) =
    π (f ∘ ↑ε) b
[PROOFSTEP]
simp only [HasLimit.isoOfEquivalence_hom_π, Discrete.equivalence_inverse, Discrete.functor_obj, Function.comp_apply,
  Functor.id_obj, Discrete.equivalence_functor, Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv,
  Category.id_comp]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ↑ε)
b : β
⊢ limit.π (Discrete.functor (f ∘ ↑ε)) { as := ↑ε.symm (↑ε b) } ≫
      (Discrete.functor f).map (NatTrans.app (Equivalence.counit (Discrete.equivalence ε)) { as := ↑ε b }) =
    π (f ∘ ↑ε) b
[PROOFSTEP]
exact limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ↑ε)
b : β
⊢ (reindex ε f).inv ≫ π (f ∘ ↑ε) b = π f (↑ε b)
[PROOFSTEP]
simp [Iso.inv_comp_eq]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ ι (f ∘ ↑ε) b ≫ (reindex ε f).hom = ι f (↑ε b)
[PROOFSTEP]
dsimp [Sigma.reindex]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ ι (f ∘ ↑ε) b ≫
      (HasColimit.isoOfEquivalence (Discrete.equivalence ε)
          (Discrete.natIso fun x =>
            Iso.refl ((Discrete.functor f).obj ((Discrete.functor (Discrete.mk ∘ ↑ε)).obj x)))).hom =
    ι f (↑ε b)
[PROOFSTEP]
simp only [HasColimit.isoOfEquivalence_hom_π, Functor.id_obj, Discrete.functor_obj, Function.comp_apply,
  Discrete.equivalence_functor, Discrete.equivalence_inverse, Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv,
  Category.id_comp]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ (Discrete.functor (f ∘ ↑ε)).map (NatTrans.app (Equivalence.unit (Discrete.equivalence ε)) { as := b }) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) } =
    ι f (↑ε b)
[PROOFSTEP]
have h := colimit.w (Discrete.functor f) (Discrete.eqToHom' (ε.apply_symm_apply (ε b)))
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ (Discrete.functor (f ∘ ↑ε)).map (NatTrans.app (Equivalence.unit (Discrete.equivalence ε)) { as := b }) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) } =
    ι f (↑ε b)
[PROOFSTEP]
simp only [Discrete.functor_obj] at h
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ (Discrete.functor (f ∘ ↑ε)).map (NatTrans.app (Equivalence.unit (Discrete.equivalence ε)) { as := b }) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) } =
    ι f (↑ε b)
[PROOFSTEP]
erw [← h, eqToHom_map, eqToHom_map, eqToHom_trans_assoc]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ eqToHom (_ : f (↑ε b) = f (↑ε b)) ≫ colimit.ι (Discrete.functor f) { as := ↑ε b } = ι f (↑ε b)
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
[PROOFSTEP]
all_goals {simp
}
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ eqToHom (_ : f (↑ε b) = f (↑ε b)) ≫ colimit.ι (Discrete.functor f) { as := ↑ε b } = ι f (↑ε b)
[PROOFSTEP]
{simp
}
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ eqToHom (_ : f (↑ε b) = f (↑ε b)) ≫ colimit.ι (Discrete.functor f) { as := ↑ε b } = ι f (↑ε b)
[PROOFSTEP]
simp
[GOAL]
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
[PROOFSTEP]
{simp
}
[GOAL]
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ ι f (↑ε b) ≫ (reindex ε f).inv = ι (f ∘ ↑ε) b
[PROOFSTEP]
simp [Iso.comp_inv_eq]