[GOAL]
L R : Type w
fst snd : R → L
⊢ ∀ {X Y : WalkingMulticospan fst snd} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case left.left.id
L R : Type w
fst snd : R → L
a✝ : L
⊢ 𝟙 (left a✝) ≫ Hom.id (left a✝) = Hom.id (left a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.right.fst
L R : Type w
fst snd : R → L
a✝ : R
⊢ 𝟙 (left (fst a✝)) ≫ Hom.fst a✝ = Hom.fst a✝
[PROOFSTEP]
rfl
[GOAL]
case left.right.snd
L R : Type w
fst snd : R → L
a✝ : R
⊢ 𝟙 (left (snd a✝)) ≫ Hom.snd a✝ = Hom.snd a✝
[PROOFSTEP]
rfl
[GOAL]
case right.right.id
L R : Type w
fst snd : R → L
a✝ : R
⊢ 𝟙 (right a✝) ≫ Hom.id (right a✝) = Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
L R : Type w
fst snd : R → L
⊢ ∀ {X Y : WalkingMulticospan fst snd} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case left.left.id
L R : Type w
fst snd : R → L
a✝ : L
⊢ Hom.id (left a✝) ≫ 𝟙 (left a✝) = Hom.id (left a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.right.fst
L R : Type w
fst snd : R → L
a✝ : R
⊢ Hom.fst a✝ ≫ 𝟙 (right a✝) = Hom.fst a✝
[PROOFSTEP]
rfl
[GOAL]
case left.right.snd
L R : Type w
fst snd : R → L
a✝ : R
⊢ Hom.snd a✝ ≫ 𝟙 (right a✝) = Hom.snd a✝
[PROOFSTEP]
rfl
[GOAL]
case right.right.id
L R : Type w
fst snd : R → L
a✝ : R
⊢ Hom.id (right a✝) ≫ 𝟙 (right a✝) = Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
L R : Type w
fst snd : R → L
⊢ ∀ {W X Y Z : WalkingMulticospan fst snd} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _) (_ | _ | _)
[GOAL]
case left.left.left.left.id.id.id
L R : Type w
fst snd : R → L
a✝ : L
⊢ (Hom.id (left a✝) ≫ Hom.id (left a✝)) ≫ Hom.id (left a✝) = Hom.id (left a✝) ≫ Hom.id (left a✝) ≫ Hom.id (left a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.left.left.right.id.id.fst
L R : Type w
fst snd : R → L
a✝ : R
⊢ (Hom.id (left (fst a✝)) ≫ Hom.id (left (fst a✝))) ≫ Hom.fst a✝ =
    Hom.id (left (fst a✝)) ≫ Hom.id (left (fst a✝)) ≫ Hom.fst a✝
[PROOFSTEP]
rfl
[GOAL]
case left.left.left.right.id.id.snd
L R : Type w
fst snd : R → L
a✝ : R
⊢ (Hom.id (left (snd a✝)) ≫ Hom.id (left (snd a✝))) ≫ Hom.snd a✝ =
    Hom.id (left (snd a✝)) ≫ Hom.id (left (snd a✝)) ≫ Hom.snd a✝
[PROOFSTEP]
rfl
[GOAL]
case left.left.right.right.id.fst.id
L R : Type w
fst snd : R → L
a✝ : R
⊢ (Hom.id (left (fst a✝)) ≫ Hom.fst a✝) ≫ Hom.id (right a✝) = Hom.id (left (fst a✝)) ≫ Hom.fst a✝ ≫ Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.left.right.right.id.snd.id
L R : Type w
fst snd : R → L
a✝ : R
⊢ (Hom.id (left (snd a✝)) ≫ Hom.snd a✝) ≫ Hom.id (right a✝) = Hom.id (left (snd a✝)) ≫ Hom.snd a✝ ≫ Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.right.right.right.fst.id.id
L R : Type w
fst snd : R → L
a✝ : R
⊢ (Hom.fst a✝ ≫ Hom.id (right a✝)) ≫ Hom.id (right a✝) = Hom.fst a✝ ≫ Hom.id (right a✝) ≫ Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.right.right.right.snd.id.id
L R : Type w
fst snd : R → L
a✝ : R
⊢ (Hom.snd a✝ ≫ Hom.id (right a✝)) ≫ Hom.id (right a✝) = Hom.snd a✝ ≫ Hom.id (right a✝) ≫ Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
case right.right.right.right.id.id.id
L R : Type w
fst snd : R → L
a✝ : R
⊢ (Hom.id (right a✝) ≫ Hom.id (right a✝)) ≫ Hom.id (right a✝) =
    Hom.id (right a✝) ≫ Hom.id (right a✝) ≫ Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
L R : Type v
fst snd : L → R
⊢ ∀ {X Y : WalkingMultispan fst snd} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case left.left.id
L R : Type v
fst snd : L → R
a✝ : L
⊢ 𝟙 (left a✝) ≫ Hom.id (left a✝) = Hom.id (left a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.right.fst
L R : Type v
fst snd : L → R
a✝ : L
⊢ 𝟙 (left a✝) ≫ Hom.fst a✝ = Hom.fst a✝
[PROOFSTEP]
rfl
[GOAL]
case left.right.snd
L R : Type v
fst snd : L → R
a✝ : L
⊢ 𝟙 (left a✝) ≫ Hom.snd a✝ = Hom.snd a✝
[PROOFSTEP]
rfl
[GOAL]
case right.right.id
L R : Type v
fst snd : L → R
a✝ : R
⊢ 𝟙 (right a✝) ≫ Hom.id (right a✝) = Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
L R : Type v
fst snd : L → R
⊢ ∀ {X Y : WalkingMultispan fst snd} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case left.left.id
L R : Type v
fst snd : L → R
a✝ : L
⊢ Hom.id (left a✝) ≫ 𝟙 (left a✝) = Hom.id (left a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.right.fst
L R : Type v
fst snd : L → R
a✝ : L
⊢ Hom.fst a✝ ≫ 𝟙 (right (fst a✝)) = Hom.fst a✝
[PROOFSTEP]
rfl
[GOAL]
case left.right.snd
L R : Type v
fst snd : L → R
a✝ : L
⊢ Hom.snd a✝ ≫ 𝟙 (right (snd a✝)) = Hom.snd a✝
[PROOFSTEP]
rfl
[GOAL]
case right.right.id
L R : Type v
fst snd : L → R
a✝ : R
⊢ Hom.id (right a✝) ≫ 𝟙 (right a✝) = Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
L R : Type v
fst snd : L → R
⊢ ∀ {W X Y Z : WalkingMultispan fst snd} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _) (_ | _ | _)
[GOAL]
case left.left.left.left.id.id.id
L R : Type v
fst snd : L → R
a✝ : L
⊢ (Hom.id (left a✝) ≫ Hom.id (left a✝)) ≫ Hom.id (left a✝) = Hom.id (left a✝) ≫ Hom.id (left a✝) ≫ Hom.id (left a✝)
[PROOFSTEP]
rfl
[GOAL]
case left.left.left.right.id.id.fst
L R : Type v
fst snd : L → R
a✝ : L
⊢ (Hom.id (left a✝) ≫ Hom.id (left a✝)) ≫ Hom.fst a✝ = Hom.id (left a✝) ≫ Hom.id (left a✝) ≫ Hom.fst a✝
[PROOFSTEP]
rfl
[GOAL]
case left.left.left.right.id.id.snd
L R : Type v
fst snd : L → R
a✝ : L
⊢ (Hom.id (left a✝) ≫ Hom.id (left a✝)) ≫ Hom.snd a✝ = Hom.id (left a✝) ≫ Hom.id (left a✝) ≫ Hom.snd a✝
[PROOFSTEP]
rfl
[GOAL]
case left.left.right.right.id.fst.id
L R : Type v
fst snd : L → R
a✝ : L
⊢ (Hom.id (left a✝) ≫ Hom.fst a✝) ≫ Hom.id (right (fst a✝)) = Hom.id (left a✝) ≫ Hom.fst a✝ ≫ Hom.id (right (fst a✝))
[PROOFSTEP]
rfl
[GOAL]
case left.left.right.right.id.snd.id
L R : Type v
fst snd : L → R
a✝ : L
⊢ (Hom.id (left a✝) ≫ Hom.snd a✝) ≫ Hom.id (right (snd a✝)) = Hom.id (left a✝) ≫ Hom.snd a✝ ≫ Hom.id (right (snd a✝))
[PROOFSTEP]
rfl
[GOAL]
case left.right.right.right.fst.id.id
L R : Type v
fst snd : L → R
a✝ : L
⊢ (Hom.fst a✝ ≫ Hom.id (right (fst a✝))) ≫ Hom.id (right (fst a✝)) =
    Hom.fst a✝ ≫ Hom.id (right (fst a✝)) ≫ Hom.id (right (fst a✝))
[PROOFSTEP]
rfl
[GOAL]
case left.right.right.right.snd.id.id
L R : Type v
fst snd : L → R
a✝ : L
⊢ (Hom.snd a✝ ≫ Hom.id (right (snd a✝))) ≫ Hom.id (right (snd a✝)) =
    Hom.snd a✝ ≫ Hom.id (right (snd a✝)) ≫ Hom.id (right (snd a✝))
[PROOFSTEP]
rfl
[GOAL]
case right.right.right.right.id.id.id
L R : Type v
fst snd : L → R
a✝ : R
⊢ (Hom.id (right a✝) ≫ Hom.id (right a✝)) ≫ Hom.id (right a✝) =
    Hom.id (right a✝) ≫ Hom.id (right a✝) ≫ Hom.id (right a✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
⊢ ∀ (X : WalkingMulticospan I.fstTo I.sndTo),
    {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (𝟙 X) =
      𝟙
        ({
              obj := fun x =>
                match x with
                | WalkingMulticospan.left a => left I a
                | WalkingMulticospan.right b => right I b,
              map := fun {x y} f =>
                match x, y, f with
                | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                  𝟙
                    ((fun x =>
                        match x with
                        | WalkingMulticospan.left a => left I a
                        | WalkingMulticospan.right b => right I b)
                      x)
                | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                  fst I b
                | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                  snd I b }.obj
          X)
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
a✝ : I.L
⊢ {
          obj := fun x =>
            match x with
            | WalkingMulticospan.left a => left I a
            | WalkingMulticospan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMulticospan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMulticospan.left a => left I a
                    | WalkingMulticospan.right b => right I b)
                  x)
            | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
              fst I b
            | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
              snd I b }.map
      (𝟙 (WalkingMulticospan.left a✝)) =
    𝟙
      ({
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.obj
        (WalkingMulticospan.left a✝))
[PROOFSTEP]
rfl
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
a✝ : I.R
⊢ {
          obj := fun x =>
            match x with
            | WalkingMulticospan.left a => left I a
            | WalkingMulticospan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMulticospan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMulticospan.left a => left I a
                    | WalkingMulticospan.right b => right I b)
                  x)
            | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
              fst I b
            | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
              snd I b }.map
      (𝟙 (WalkingMulticospan.right a✝)) =
    𝟙
      ({
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.obj
        (WalkingMulticospan.right a✝))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
⊢ ∀ {X Y Z : WalkingMulticospan I.fstTo I.sndTo} (f : X ⟶ Y) (g : Y ⟶ Z),
    {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (f ≫ g) =
      {
              obj := fun x =>
                match x with
                | WalkingMulticospan.left a => left I a
                | WalkingMulticospan.right b => right I b,
              map := fun {x y} f =>
                match x, y, f with
                | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                  𝟙
                    ((fun x =>
                        match x with
                        | WalkingMulticospan.left a => left I a
                        | WalkingMulticospan.right b => right I b)
                      x)
                | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                  fst I b
                | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                  snd I b }.map
          f ≫
        {
              obj := fun x =>
                match x with
                | WalkingMulticospan.left a => left I a
                | WalkingMulticospan.right b => right I b,
              map := fun {x y} f =>
                match x, y, f with
                | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                  𝟙
                    ((fun x =>
                        match x with
                        | WalkingMulticospan.left a => left I a
                        | WalkingMulticospan.right b => right I b)
                      x)
                | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                  fst I b
                | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                  snd I b }.map
          g
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _)
[GOAL]
case left.left.left.id.id
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
a✝ : I.L
⊢ {
          obj := fun x =>
            match x with
            | WalkingMulticospan.left a => left I a
            | WalkingMulticospan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMulticospan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMulticospan.left a => left I a
                    | WalkingMulticospan.right b => right I b)
                  x)
            | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
              fst I b
            | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
              snd I b }.map
      (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝) ≫
        WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝)) =
    {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝)) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝))
[PROOFSTEP]
aesop_cat
[GOAL]
case left.left.right.id.fst
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
a✝ : I.R
⊢ {
          obj := fun x =>
            match x with
            | WalkingMulticospan.left a => left I a
            | WalkingMulticospan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMulticospan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMulticospan.left a => left I a
                    | WalkingMulticospan.right b => right I b)
                  x)
            | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
              fst I b
            | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
              snd I b }.map
      (WalkingMulticospan.Hom.id (WalkingMulticospan.left (fstTo I a✝)) ≫ WalkingMulticospan.Hom.fst a✝) =
    {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left (fstTo I a✝))) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.fst a✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case left.left.right.id.snd
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
a✝ : I.R
⊢ {
          obj := fun x =>
            match x with
            | WalkingMulticospan.left a => left I a
            | WalkingMulticospan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMulticospan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMulticospan.left a => left I a
                    | WalkingMulticospan.right b => right I b)
                  x)
            | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
              fst I b
            | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
              snd I b }.map
      (WalkingMulticospan.Hom.id (WalkingMulticospan.left (sndTo I a✝)) ≫ WalkingMulticospan.Hom.snd a✝) =
    {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left (sndTo I a✝))) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.snd a✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case left.right.right.fst.id
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
a✝ : I.R
⊢ {
          obj := fun x =>
            match x with
            | WalkingMulticospan.left a => left I a
            | WalkingMulticospan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMulticospan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMulticospan.left a => left I a
                    | WalkingMulticospan.right b => right I b)
                  x)
            | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
              fst I b
            | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
              snd I b }.map
      (WalkingMulticospan.Hom.fst a✝ ≫ WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) =
    {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.fst a✝) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))
[PROOFSTEP]
aesop_cat
[GOAL]
case left.right.right.snd.id
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
a✝ : I.R
⊢ {
          obj := fun x =>
            match x with
            | WalkingMulticospan.left a => left I a
            | WalkingMulticospan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMulticospan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMulticospan.left a => left I a
                    | WalkingMulticospan.right b => right I b)
                  x)
            | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
              fst I b
            | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
              snd I b }.map
      (WalkingMulticospan.Hom.snd a✝ ≫ WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) =
    {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.snd a✝) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))
[PROOFSTEP]
aesop_cat
[GOAL]
case right.right.right.id.id
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
a✝ : I.R
⊢ {
          obj := fun x =>
            match x with
            | WalkingMulticospan.left a => left I a
            | WalkingMulticospan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMulticospan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMulticospan.left a => left I a
                    | WalkingMulticospan.right b => right I b)
                  x)
            | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
              fst I b
            | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
              snd I b }.map
      (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) ≫
        WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) =
    {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMulticospan.left a => left I a
              | WalkingMulticospan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMulticospan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMulticospan.left a => left I a
                      | WalkingMulticospan.right b => right I b)
                    x)
              | .(WalkingMulticospan.left (fstTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b =>
                fst I b
              | .(WalkingMulticospan.left (sndTo I b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
                snd I b }.map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
b : I.R
⊢ fstPiMap I ≫ Pi.π I.right b = Pi.π I.left (fstTo I b) ≫ fst I b
[PROOFSTEP]
simp [fstPiMap]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
b : I.R
⊢ sndPiMap I ≫ Pi.π I.right b = Pi.π I.left (sndTo I b) ≫ snd I b
[PROOFSTEP]
simp [sndPiMap]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
⊢ ∀ (X : WalkingMultispan I.fstFrom I.sndFrom),
    {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (𝟙 X) =
      𝟙
        ({
              obj := fun x =>
                match x with
                | WalkingMultispan.left a => left I a
                | WalkingMultispan.right b => right I b,
              map := fun {x y} f =>
                match x, y, f with
                | x, .(x), WalkingMultispan.Hom.id .(x) =>
                  𝟙
                    ((fun x =>
                        match x with
                        | WalkingMultispan.left a => left I a
                        | WalkingMultispan.right b => right I b)
                      x)
                | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                  fst I b
                | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                  snd I b }.obj
          X)
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
a✝ : I.L
⊢ {
          obj := fun x =>
            match x with
            | WalkingMultispan.left a => left I a
            | WalkingMultispan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMultispan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMultispan.left a => left I a
                    | WalkingMultispan.right b => right I b)
                  x)
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b => fst I b
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
              snd I b }.map
      (𝟙 (WalkingMultispan.left a✝)) =
    𝟙
      ({
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.obj
        (WalkingMultispan.left a✝))
[PROOFSTEP]
rfl
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
a✝ : I.R
⊢ {
          obj := fun x =>
            match x with
            | WalkingMultispan.left a => left I a
            | WalkingMultispan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMultispan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMultispan.left a => left I a
                    | WalkingMultispan.right b => right I b)
                  x)
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b => fst I b
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
              snd I b }.map
      (𝟙 (WalkingMultispan.right a✝)) =
    𝟙
      ({
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.obj
        (WalkingMultispan.right a✝))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
⊢ ∀ {X Y Z : WalkingMultispan I.fstFrom I.sndFrom} (f : X ⟶ Y) (g : Y ⟶ Z),
    {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (f ≫ g) =
      {
              obj := fun x =>
                match x with
                | WalkingMultispan.left a => left I a
                | WalkingMultispan.right b => right I b,
              map := fun {x y} f =>
                match x, y, f with
                | x, .(x), WalkingMultispan.Hom.id .(x) =>
                  𝟙
                    ((fun x =>
                        match x with
                        | WalkingMultispan.left a => left I a
                        | WalkingMultispan.right b => right I b)
                      x)
                | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                  fst I b
                | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                  snd I b }.map
          f ≫
        {
              obj := fun x =>
                match x with
                | WalkingMultispan.left a => left I a
                | WalkingMultispan.right b => right I b,
              map := fun {x y} f =>
                match x, y, f with
                | x, .(x), WalkingMultispan.Hom.id .(x) =>
                  𝟙
                    ((fun x =>
                        match x with
                        | WalkingMultispan.left a => left I a
                        | WalkingMultispan.right b => right I b)
                      x)
                | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                  fst I b
                | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                  snd I b }.map
          g
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _)
[GOAL]
case left.left.left.id.id
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
a✝ : I.L
⊢ {
          obj := fun x =>
            match x with
            | WalkingMultispan.left a => left I a
            | WalkingMultispan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMultispan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMultispan.left a => left I a
                    | WalkingMultispan.right b => right I b)
                  x)
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b => fst I b
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
              snd I b }.map
      (WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) =
    {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.id (WalkingMultispan.left a✝))
[PROOFSTEP]
aesop_cat
[GOAL]
case left.left.right.id.fst
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
a✝ : I.L
⊢ {
          obj := fun x =>
            match x with
            | WalkingMultispan.left a => left I a
            | WalkingMultispan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMultispan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMultispan.left a => left I a
                    | WalkingMultispan.right b => right I b)
                  x)
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b => fst I b
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
              snd I b }.map
      (WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.fst a✝) =
    {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.fst a✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case left.left.right.id.snd
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
a✝ : I.L
⊢ {
          obj := fun x =>
            match x with
            | WalkingMultispan.left a => left I a
            | WalkingMultispan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMultispan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMultispan.left a => left I a
                    | WalkingMultispan.right b => right I b)
                  x)
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b => fst I b
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
              snd I b }.map
      (WalkingMultispan.Hom.id (WalkingMultispan.left a✝) ≫ WalkingMultispan.Hom.snd a✝) =
    {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.snd a✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case left.right.right.fst.id
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
a✝ : I.L
⊢ {
          obj := fun x =>
            match x with
            | WalkingMultispan.left a => left I a
            | WalkingMultispan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMultispan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMultispan.left a => left I a
                    | WalkingMultispan.right b => right I b)
                  x)
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b => fst I b
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
              snd I b }.map
      (WalkingMultispan.Hom.fst a✝ ≫ WalkingMultispan.Hom.id (WalkingMultispan.right (fstFrom I a✝))) =
    {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.fst a✝) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.id (WalkingMultispan.right (fstFrom I a✝)))
[PROOFSTEP]
aesop_cat
[GOAL]
case left.right.right.snd.id
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
a✝ : I.L
⊢ {
          obj := fun x =>
            match x with
            | WalkingMultispan.left a => left I a
            | WalkingMultispan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMultispan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMultispan.left a => left I a
                    | WalkingMultispan.right b => right I b)
                  x)
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b => fst I b
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
              snd I b }.map
      (WalkingMultispan.Hom.snd a✝ ≫ WalkingMultispan.Hom.id (WalkingMultispan.right (sndFrom I a✝))) =
    {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.snd a✝) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.id (WalkingMultispan.right (sndFrom I a✝)))
[PROOFSTEP]
aesop_cat
[GOAL]
case right.right.right.id.id
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
a✝ : I.R
⊢ {
          obj := fun x =>
            match x with
            | WalkingMultispan.left a => left I a
            | WalkingMultispan.right b => right I b,
          map := fun {x y} f =>
            match x, y, f with
            | x, .(x), WalkingMultispan.Hom.id .(x) =>
              𝟙
                ((fun x =>
                    match x with
                    | WalkingMultispan.left a => left I a
                    | WalkingMultispan.right b => right I b)
                  x)
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b => fst I b
            | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
              snd I b }.map
      (WalkingMultispan.Hom.id (WalkingMultispan.right a✝) ≫ WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) =
    {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      {
            obj := fun x =>
              match x with
              | WalkingMultispan.left a => left I a
              | WalkingMultispan.right b => right I b,
            map := fun {x y} f =>
              match x, y, f with
              | x, .(x), WalkingMultispan.Hom.id .(x) =>
                𝟙
                  ((fun x =>
                      match x with
                      | WalkingMultispan.left a => left I a
                      | WalkingMultispan.right b => right I b)
                    x)
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (fstFrom I b)), WalkingMultispan.Hom.fst b =>
                fst I b
              | .(WalkingMultispan.left b), .(WalkingMultispan.right (sndFrom I b)), WalkingMultispan.Hom.snd b =>
                snd I b }.map
        (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.L
⊢ Sigma.ι I.left b ≫ fstSigmaMap I = fst I b ≫ Sigma.ι I.right (fstFrom I b)
[PROOFSTEP]
simp [fstSigmaMap]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.L
⊢ Sigma.ι I.left b ≫ sndSigmaMap I = snd I b ≫ Sigma.ι I.right (sndFrom I b)
[PROOFSTEP]
simp [sndSigmaMap]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ NatTrans.app K.π (WalkingMulticospan.right b) = ι K (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b
[PROOFSTEP]
rw [← K.w (WalkingMulticospan.Hom.fst b)]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ NatTrans.app K.π (WalkingMulticospan.left (MulticospanIndex.fstTo I b)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.fst b) =
    ι K (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ NatTrans.app K.π (WalkingMulticospan.right b) = ι K (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
[PROOFSTEP]
rw [← K.w (WalkingMulticospan.Hom.snd b)]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ NatTrans.app K.π (WalkingMulticospan.left (MulticospanIndex.sndTo I b)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.snd b) =
    ι K (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
⊢ ∀ ⦃X Y : WalkingMulticospan I.fstTo I.sndTo⦄ (f : X ⟶ Y),
    ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj P).map f ≫
        (fun x =>
            match x with
            | WalkingMulticospan.left a => ι a
            | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
          Y =
      (fun x =>
            match x with
            | WalkingMulticospan.left a => ι a
            | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
          X ≫
        (MulticospanIndex.multicospan I).map f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.L
⊢ ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj P).map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝)) ≫
      (fun x =>
          match x with
          | WalkingMulticospan.left a => ι a
          | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
        (WalkingMulticospan.left a✝) =
    (fun x =>
          match x with
          | WalkingMulticospan.left a => ι a
          | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
        (WalkingMulticospan.left a✝) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝))
[PROOFSTEP]
dsimp
[GOAL]
case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.R
⊢ ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj P).map (WalkingMulticospan.Hom.fst a✝) ≫
      (fun x =>
          match x with
          | WalkingMulticospan.left a => ι a
          | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
        (WalkingMulticospan.right a✝) =
    (fun x =>
          match x with
          | WalkingMulticospan.left a => ι a
          | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
        (WalkingMulticospan.left (MulticospanIndex.fstTo I a✝)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.fst a✝)
[PROOFSTEP]
dsimp
[GOAL]
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.R
⊢ ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj P).map (WalkingMulticospan.Hom.snd a✝) ≫
      (fun x =>
          match x with
          | WalkingMulticospan.left a => ι a
          | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
        (WalkingMulticospan.right a✝) =
    (fun x =>
          match x with
          | WalkingMulticospan.left a => ι a
          | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
        (WalkingMulticospan.left (MulticospanIndex.sndTo I a✝)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.snd a✝)
[PROOFSTEP]
dsimp
[GOAL]
case right.right.id
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.R
⊢ ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj P).map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      (fun x =>
          match x with
          | WalkingMulticospan.left a => ι a
          | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
        (WalkingMulticospan.right a✝) =
    (fun x =>
          match x with
          | WalkingMulticospan.left a => ι a
          | WalkingMulticospan.right b => ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b)
        (WalkingMulticospan.right a✝) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))
[PROOFSTEP]
dsimp
[GOAL]
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝ ≫ (MulticospanIndex.multicospan I).map (𝟙 (WalkingMulticospan.left a✝))
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id, Functor.map_id, MulticospanIndex.multicospan_obj_left,
  MulticospanIndex.multicospan_obj_right]
[GOAL]
case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.R
⊢ 𝟙 P ≫ ι (MulticospanIndex.fstTo I a✝) ≫ MulticospanIndex.fst I a✝ =
    ι (MulticospanIndex.fstTo I a✝) ≫ MulticospanIndex.fst I a✝
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id, Functor.map_id, MulticospanIndex.multicospan_obj_left,
  MulticospanIndex.multicospan_obj_right]
[GOAL]
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.R
⊢ 𝟙 P ≫ ι (MulticospanIndex.fstTo I a✝) ≫ MulticospanIndex.fst I a✝ =
    ι (MulticospanIndex.sndTo I a✝) ≫ MulticospanIndex.snd I a✝
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id, Functor.map_id, MulticospanIndex.multicospan_obj_left,
  MulticospanIndex.multicospan_obj_right]
[GOAL]
case right.right.id
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.R
⊢ 𝟙 P ≫ ι (MulticospanIndex.fstTo I a✝) ≫ MulticospanIndex.fst I a✝ =
    (ι (MulticospanIndex.fstTo I a✝) ≫ MulticospanIndex.fst I a✝) ≫
      (MulticospanIndex.multicospan I).map (𝟙 (WalkingMulticospan.right a✝))
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id, Functor.map_id, MulticospanIndex.multicospan_obj_left,
  MulticospanIndex.multicospan_obj_right]
[GOAL]
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
I✝ : MulticospanIndex C
K : Multifork I✝
I : MulticospanIndex C
P : C
ι : (a : I.L) → P ⟶ MulticospanIndex.left I a
w :
  ∀ (b : I.R),
    ι (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
      ι (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
a✝ : I.R
⊢ ι (MulticospanIndex.fstTo I a✝) ≫ MulticospanIndex.fst I a✝ =
    ι (MulticospanIndex.sndTo I a✝) ≫ MulticospanIndex.snd I a✝
[PROOFSTEP]
apply w
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
b : I.R
⊢ ι K (MulticospanIndex.fstTo I b) ≫ MulticospanIndex.fst I b =
    ι K (MulticospanIndex.sndTo I b) ≫ MulticospanIndex.snd I b
[PROOFSTEP]
rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
⊢ ∀ (s : Cone (MulticospanIndex.multicospan I)) (j : WalkingMulticospan I.fstTo I.sndTo),
    lift s ≫ NatTrans.app K.π j = NatTrans.app s.π j
[PROOFSTEP]
rintro E (a | b)
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
E : Cone (MulticospanIndex.multicospan I)
a : I.L
⊢ lift E ≫ NatTrans.app K.π (WalkingMulticospan.left a) = NatTrans.app E.π (WalkingMulticospan.left a)
[PROOFSTEP]
apply fac
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
E : Cone (MulticospanIndex.multicospan I)
b : I.R
⊢ lift E ≫ NatTrans.app K.π (WalkingMulticospan.right b) = NatTrans.app E.π (WalkingMulticospan.right b)
[PROOFSTEP]
rw [← E.w (WalkingMulticospan.Hom.fst b), ← K.w (WalkingMulticospan.Hom.fst b), ← Category.assoc]
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
E : Cone (MulticospanIndex.multicospan I)
b : I.R
⊢ (lift E ≫ NatTrans.app K.π (WalkingMulticospan.left (MulticospanIndex.fstTo I b))) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.fst b) =
    NatTrans.app E.π (WalkingMulticospan.left (MulticospanIndex.fstTo I b)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.fst b)
[PROOFSTEP]
congr 1
[GOAL]
case right.e_a
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
E : Cone (MulticospanIndex.multicospan I)
b : I.R
⊢ lift E ≫ NatTrans.app K.π (WalkingMulticospan.left (MulticospanIndex.fstTo I b)) =
    NatTrans.app E.π (WalkingMulticospan.left (MulticospanIndex.fstTo I b))
[PROOFSTEP]
apply fac
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
⊢ ∀ (s : Cone (MulticospanIndex.multicospan I)) (m : s.pt ⟶ K.pt),
    (∀ (j : WalkingMulticospan I.fstTo I.sndTo), m ≫ NatTrans.app K.π j = NatTrans.app s.π j) → m = lift s
[PROOFSTEP]
rintro E m hm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
E : Cone (MulticospanIndex.multicospan I)
m : E.pt ⟶ K.pt
hm : ∀ (j : WalkingMulticospan I.fstTo I.sndTo), m ≫ NatTrans.app K.π j = NatTrans.app E.π j
⊢ m = lift E
[PROOFSTEP]
apply uniq
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
E : Cone (MulticospanIndex.multicospan I)
m : E.pt ⟶ K.pt
hm : ∀ (j : WalkingMulticospan I.fstTo I.sndTo), m ≫ NatTrans.app K.π j = NatTrans.app E.π j
⊢ ∀ (i : I.L), m ≫ ι K i = ι E i
[PROOFSTEP]
intro i
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : I.L), lift E ≫ ι K i = ι E i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), m ≫ ι K i = ι E i) → m = lift E
E : Cone (MulticospanIndex.multicospan I)
m : E.pt ⟶ K.pt
hm : ∀ (j : WalkingMulticospan I.fstTo I.sndTo), m ≫ NatTrans.app K.π j = NatTrans.app E.π j
i : I.L
⊢ m ≫ ι K i = ι E i
[PROOFSTEP]
apply hm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
⊢ Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I = Pi.lift (ι K) ≫ MulticospanIndex.sndPiMap I
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
b✝ : I.R
⊢ (Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I) ≫ Pi.π I.right b✝ =
    (Pi.lift (ι K) ≫ MulticospanIndex.sndPiMap I) ≫ Pi.π I.right b✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    ((Functor.const WalkingParallelPair).obj K.pt).map f ≫
        (fun x =>
            match x with
            | WalkingParallelPair.zero => Pi.lift (ι K)
            | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
          Y =
      (fun x =>
            match x with
            | WalkingParallelPair.zero => Pi.lift (ι K)
            | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
          X ≫
        (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)).map f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case zero.zero.id
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ ((Functor.const WalkingParallelPair).obj K.pt).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      (fun x =>
          match x with
          | WalkingParallelPair.zero => Pi.lift (ι K)
          | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
        WalkingParallelPair.zero =
    (fun x =>
          match x with
          | WalkingParallelPair.zero => Pi.lift (ι K)
          | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
        WalkingParallelPair.zero ≫
      (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)).map
        (WalkingParallelPairHom.id WalkingParallelPair.zero)
[PROOFSTEP]
dsimp
[GOAL]
case zero.one.left
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ ((Functor.const WalkingParallelPair).obj K.pt).map WalkingParallelPairHom.left ≫
      (fun x =>
          match x with
          | WalkingParallelPair.zero => Pi.lift (ι K)
          | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
        WalkingParallelPair.one =
    (fun x =>
          match x with
          | WalkingParallelPair.zero => Pi.lift (ι K)
          | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
        WalkingParallelPair.zero ≫
      (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)).map WalkingParallelPairHom.left
[PROOFSTEP]
dsimp
[GOAL]
case zero.one.right
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ ((Functor.const WalkingParallelPair).obj K.pt).map WalkingParallelPairHom.right ≫
      (fun x =>
          match x with
          | WalkingParallelPair.zero => Pi.lift (ι K)
          | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
        WalkingParallelPair.one =
    (fun x =>
          match x with
          | WalkingParallelPair.zero => Pi.lift (ι K)
          | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
        WalkingParallelPair.zero ≫
      (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)).map WalkingParallelPairHom.right
[PROOFSTEP]
dsimp
[GOAL]
case one.one.id
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ ((Functor.const WalkingParallelPair).obj K.pt).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (fun x =>
          match x with
          | WalkingParallelPair.zero => Pi.lift (ι K)
          | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
        WalkingParallelPair.one =
    (fun x =>
          match x with
          | WalkingParallelPair.zero => Pi.lift (ι K)
          | WalkingParallelPair.one => Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I)
        WalkingParallelPair.one ≫
      (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)).map
        (WalkingParallelPairHom.id WalkingParallelPair.one)
[PROOFSTEP]
dsimp
[GOAL]
case zero.zero.id
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ 𝟙 K.pt ≫ Pi.lift (ι K) =
    Pi.lift (ι K) ≫
      (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)).map (𝟙 WalkingParallelPair.zero)
[PROOFSTEP]
simp only [Category.id_comp, Functor.map_id, parallelPair_obj_zero, Category.comp_id, pi_condition,
  parallelPair_obj_one]
[GOAL]
case zero.one.left
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ 𝟙 K.pt ≫ Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I = Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I
[PROOFSTEP]
simp only [Category.id_comp, Functor.map_id, parallelPair_obj_zero, Category.comp_id, pi_condition,
  parallelPair_obj_one]
[GOAL]
case zero.one.right
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ 𝟙 K.pt ≫ Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I = Pi.lift (ι K) ≫ MulticospanIndex.sndPiMap I
[PROOFSTEP]
simp only [Category.id_comp, Functor.map_id, parallelPair_obj_zero, Category.comp_id, pi_condition,
  parallelPair_obj_one]
[GOAL]
case one.one.id
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K✝ : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ 𝟙 K.pt ≫ Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I =
    (Pi.lift (ι K) ≫ MulticospanIndex.fstPiMap I) ≫
      (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)).map (𝟙 WalkingParallelPair.one)
[PROOFSTEP]
simp only [Category.id_comp, Functor.map_id, parallelPair_obj_zero, Category.comp_id, pi_condition,
  parallelPair_obj_one]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
c : Fork (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)
⊢ ∀ ⦃X Y : WalkingMulticospan I.fstTo I.sndTo⦄ (f : X ⟶ Y),
    ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj c.pt).map f ≫
        (fun x =>
            match x with
            | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
            | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
          Y =
      (fun x =>
            match x with
            | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
            | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
          X ≫
        (MulticospanIndex.multicospan I).map f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case left.left.id
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
c : Fork (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)
a✝ : I.L
⊢ ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj c.pt).map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝)) ≫
      (fun x =>
          match x with
          | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
          | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
        (WalkingMulticospan.left a✝) =
    (fun x =>
          match x with
          | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
          | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
        (WalkingMulticospan.left a✝) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a✝))
[PROOFSTEP]
simp
[GOAL]
case left.right.fst
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
c : Fork (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)
a✝ : I.R
⊢ ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj c.pt).map (WalkingMulticospan.Hom.fst a✝) ≫
      (fun x =>
          match x with
          | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
          | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
        (WalkingMulticospan.right a✝) =
    (fun x =>
          match x with
          | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
          | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
        (WalkingMulticospan.left (MulticospanIndex.fstTo I a✝)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.fst a✝)
[PROOFSTEP]
simp
[GOAL]
case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
c : Fork (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)
a✝ : I.R
⊢ ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj c.pt).map (WalkingMulticospan.Hom.snd a✝) ≫
      (fun x =>
          match x with
          | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
          | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
        (WalkingMulticospan.right a✝) =
    (fun x =>
          match x with
          | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
          | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
        (WalkingMulticospan.left (MulticospanIndex.sndTo I a✝)) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.snd a✝)
[PROOFSTEP]
dsimp
[GOAL]
case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
c : Fork (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)
a✝ : I.R
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right a✝ =
    (Fork.ι c ≫ Pi.π I.left (MulticospanIndex.sndTo I a✝)) ≫ MulticospanIndex.snd I a✝
[PROOFSTEP]
rw [c.condition_assoc]
[GOAL]
case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
c : Fork (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)
a✝ : I.R
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ MulticospanIndex.sndPiMap I ≫ Pi.π I.right a✝ =
    (Fork.ι c ≫ Pi.π I.left (MulticospanIndex.sndTo I a✝)) ≫ MulticospanIndex.snd I a✝
[PROOFSTEP]
simp
[GOAL]
case right.right.id
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
K : Multifork I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
c : Fork (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I)
a✝ : I.R
⊢ ((Functor.const (WalkingMulticospan I.fstTo I.sndTo)).obj c.pt).map
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝)) ≫
      (fun x =>
          match x with
          | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
          | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
        (WalkingMulticospan.right a✝) =
    (fun x =>
          match x with
          | WalkingMulticospan.left a => Fork.ι c ≫ Pi.π I.left a
          | WalkingMulticospan.right b => Fork.ι c ≫ MulticospanIndex.fstPiMap I ≫ Pi.π I.right b)
        (WalkingMulticospan.right a✝) ≫
      (MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingParallelPair),
    f.Hom ≫ NatTrans.app (Multifork.toPiFork K₂).π j = NatTrans.app (Multifork.toPiFork K₁).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ f.Hom ≫ NatTrans.app (Multifork.toPiFork K₂).π WalkingParallelPair.zero =
    NatTrans.app (Multifork.toPiFork K₁).π WalkingParallelPair.zero
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case zero.w
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (j : Discrete I.L),
    (f.Hom ≫ NatTrans.app (Multifork.toPiFork K₂).π WalkingParallelPair.zero) ≫ limit.π (Discrete.functor I.left) j =
      NatTrans.app (Multifork.toPiFork K₁).π WalkingParallelPair.zero ≫ limit.π (Discrete.functor I.left) j
[PROOFSTEP]
simp
[GOAL]
case one
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ f.Hom ≫ NatTrans.app (Multifork.toPiFork K₂).π WalkingParallelPair.one =
    NatTrans.app (Multifork.toPiFork K₁).π WalkingParallelPair.one
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case one.w
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (j : Discrete I.R),
    (f.Hom ≫ NatTrans.app (Multifork.toPiFork K₂).π WalkingParallelPair.one) ≫ limit.π (Discrete.functor I.right) j =
      NatTrans.app (Multifork.toPiFork K₁).π WalkingParallelPair.one ≫ limit.π (Discrete.functor I.right) j
[PROOFSTEP]
intros j
[GOAL]
case one.w
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
j : Discrete I.R
⊢ (f.Hom ≫ NatTrans.app (Multifork.toPiFork K₂).π WalkingParallelPair.one) ≫ limit.π (Discrete.functor I.right) j =
    NatTrans.app (Multifork.toPiFork K₁).π WalkingParallelPair.one ≫ limit.π (Discrete.functor I.right) j
[PROOFSTEP]
simp only [Multifork.toPiFork_π_app_one, Multifork.pi_condition, Category.assoc]
[GOAL]
case one.w
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
j : Discrete I.R
⊢ f.Hom ≫ Pi.lift (Multifork.ι K₂) ≫ sndPiMap I ≫ limit.π (Discrete.functor I.right) j =
    Pi.lift (Multifork.ι K₁) ≫ sndPiMap I ≫ limit.π (Discrete.functor I.right) j
[PROOFSTEP]
dsimp [sndPiMap]
[GOAL]
case one.w
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
j : Discrete I.R
⊢ f.Hom ≫
      Pi.lift (Multifork.ι K₂) ≫
        (Pi.lift fun b => Pi.π I.left (sndTo I b) ≫ snd I b) ≫ limit.π (Discrete.functor I.right) j =
    Pi.lift (Multifork.ι K₁) ≫
      (Pi.lift fun b => Pi.π I.left (sndTo I b) ≫ snd I b) ≫ limit.π (Discrete.functor I.right) j
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Fork (fstPiMap I) (sndPiMap I)
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingMulticospan I.fstTo I.sndTo),
    f.Hom ≫ NatTrans.app (Multifork.ofPiFork I K₂).π j = NatTrans.app (Multifork.ofPiFork I K₁).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case left
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Fork (fstPiMap I) (sndPiMap I)
f : K₁ ⟶ K₂
a✝ : I.L
⊢ f.Hom ≫ NatTrans.app (Multifork.ofPiFork I K₂).π (WalkingMulticospan.left a✝) =
    NatTrans.app (Multifork.ofPiFork I K₁).π (WalkingMulticospan.left a✝)
[PROOFSTEP]
simp
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K₁ K₂ : Fork (fstPiMap I) (sndPiMap I)
f : K₁ ⟶ K₂
a✝ : I.R
⊢ f.Hom ≫ NatTrans.app (Multifork.ofPiFork I K₂).π (WalkingMulticospan.right a✝) =
    NatTrans.app (Multifork.ofPiFork I K₁).π (WalkingMulticospan.right a✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
⊢ ∀ (j : WalkingMulticospan I.fstTo I.sndTo),
    NatTrans.app ((𝟭 (Multifork I)).obj K).π j =
      (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫ NatTrans.app ((toPiForkFunctor I ⋙ ofPiForkFunctor I).obj K).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case left
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
a✝ : I.L
⊢ NatTrans.app ((𝟭 (Multifork I)).obj K).π (WalkingMulticospan.left a✝) =
    (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫
      NatTrans.app ((toPiForkFunctor I ⋙ ofPiForkFunctor I).obj K).π (WalkingMulticospan.left a✝)
[PROOFSTEP]
dsimp
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
a✝ : I.R
⊢ NatTrans.app ((𝟭 (Multifork I)).obj K).π (WalkingMulticospan.right a✝) =
    (Iso.refl ((𝟭 (Multifork I)).obj K).pt).hom ≫
      NatTrans.app ((toPiForkFunctor I ⋙ ofPiForkFunctor I).obj K).π (WalkingMulticospan.right a✝)
[PROOFSTEP]
dsimp
[GOAL]
case left
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
a✝ : I.L
⊢ Multifork.ι K a✝ = 𝟙 K.pt ≫ Pi.lift (Multifork.ι K) ≫ Pi.π I.left a✝
[PROOFSTEP]
simp [← Fork.app_one_eq_ι_comp_left, -Fork.app_one_eq_ι_comp_left]
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
I : MulticospanIndex C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
K : Multifork I
a✝ : I.R
⊢ NatTrans.app K.π (WalkingMulticospan.right a✝) = 𝟙 K.pt ≫ Pi.lift (Multifork.ι K) ≫ fstPiMap I ≫ Pi.π I.right a✝
[PROOFSTEP]
simp [← Fork.app_one_eq_ι_comp_left, -Fork.app_one_eq_ι_comp_left]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
a : I.L
⊢ NatTrans.app K.ι (WalkingMultispan.left a) = MultispanIndex.fst I a ≫ π K (MultispanIndex.fstFrom I a)
[PROOFSTEP]
rw [← K.w (WalkingMultispan.Hom.fst a)]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
a : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.fst a) ≫
      NatTrans.app K.ι (WalkingMultispan.right (MultispanIndex.fstFrom I a)) =
    MultispanIndex.fst I a ≫ π K (MultispanIndex.fstFrom I a)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
a : I.L
⊢ NatTrans.app K.ι (WalkingMultispan.left a) = MultispanIndex.snd I a ≫ π K (MultispanIndex.sndFrom I a)
[PROOFSTEP]
rw [← K.w (WalkingMultispan.Hom.snd a)]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
a : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.snd a) ≫
      NatTrans.app K.ι (WalkingMultispan.right (MultispanIndex.sndFrom I a)) =
    MultispanIndex.snd I a ≫ π K (MultispanIndex.sndFrom I a)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
⊢ ∀ ⦃X Y : WalkingMultispan I.fstFrom I.sndFrom⦄ (f : X ⟶ Y),
    (MultispanIndex.multispan I).map f ≫
        (fun x =>
            match x with
            | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
            | WalkingMultispan.right b => π b)
          Y =
      (fun x =>
            match x with
            | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
            | WalkingMultispan.right b => π b)
          X ≫
        ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj P).map f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) ≫
      (fun x =>
          match x with
          | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
          | WalkingMultispan.right b => π b)
        (WalkingMultispan.left a✝) =
    (fun x =>
          match x with
          | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
          | WalkingMultispan.right b => π b)
        (WalkingMultispan.left a✝) ≫
      ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj P).map
        (WalkingMultispan.Hom.id (WalkingMultispan.left a✝))
[PROOFSTEP]
dsimp
[GOAL]
case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.fst a✝) ≫
      (fun x =>
          match x with
          | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
          | WalkingMultispan.right b => π b)
        (WalkingMultispan.right (MultispanIndex.fstFrom I a✝)) =
    (fun x =>
          match x with
          | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
          | WalkingMultispan.right b => π b)
        (WalkingMultispan.left a✝) ≫
      ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj P).map (WalkingMultispan.Hom.fst a✝)
[PROOFSTEP]
dsimp
[GOAL]
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.snd a✝) ≫
      (fun x =>
          match x with
          | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
          | WalkingMultispan.right b => π b)
        (WalkingMultispan.right (MultispanIndex.sndFrom I a✝)) =
    (fun x =>
          match x with
          | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
          | WalkingMultispan.right b => π b)
        (WalkingMultispan.left a✝) ≫
      ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj P).map (WalkingMultispan.Hom.snd a✝)
[PROOFSTEP]
dsimp
[GOAL]
case right.right.id
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.R
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      (fun x =>
          match x with
          | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
          | WalkingMultispan.right b => π b)
        (WalkingMultispan.right a✝) =
    (fun x =>
          match x with
          | WalkingMultispan.left a => MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a)
          | WalkingMultispan.right b => π b)
        (WalkingMultispan.right a✝) ≫
      ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj P).map
        (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))
[PROOFSTEP]
dsimp
[GOAL]
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.L
⊢ (MultispanIndex.multispan I).map (𝟙 (WalkingMultispan.left a✝)) ≫
      MultispanIndex.fst I a✝ ≫ π (MultispanIndex.fstFrom I a✝) =
    (MultispanIndex.fst I a✝ ≫ π (MultispanIndex.fstFrom I a✝)) ≫ 𝟙 P
[PROOFSTEP]
simp only [Functor.map_id, MultispanIndex.multispan_obj_left, Category.id_comp, Category.comp_id,
  MultispanIndex.multispan_obj_right]
[GOAL]
case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.L
⊢ MultispanIndex.fst I a✝ ≫ π (MultispanIndex.fstFrom I a✝) =
    (MultispanIndex.fst I a✝ ≫ π (MultispanIndex.fstFrom I a✝)) ≫ 𝟙 P
[PROOFSTEP]
simp only [Functor.map_id, MultispanIndex.multispan_obj_left, Category.id_comp, Category.comp_id,
  MultispanIndex.multispan_obj_right]
[GOAL]
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.L
⊢ MultispanIndex.snd I a✝ ≫ π (MultispanIndex.sndFrom I a✝) =
    (MultispanIndex.fst I a✝ ≫ π (MultispanIndex.fstFrom I a✝)) ≫ 𝟙 P
[PROOFSTEP]
simp only [Functor.map_id, MultispanIndex.multispan_obj_left, Category.id_comp, Category.comp_id,
  MultispanIndex.multispan_obj_right]
[GOAL]
case right.right.id
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.R
⊢ (MultispanIndex.multispan I).map (𝟙 (WalkingMultispan.right a✝)) ≫ π a✝ = π a✝ ≫ 𝟙 P
[PROOFSTEP]
simp only [Functor.map_id, MultispanIndex.multispan_obj_left, Category.id_comp, Category.comp_id,
  MultispanIndex.multispan_obj_right]
[GOAL]
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.L
⊢ MultispanIndex.snd I a✝ ≫ π (MultispanIndex.sndFrom I a✝) = MultispanIndex.fst I a✝ ≫ π (MultispanIndex.fstFrom I a✝)
[PROOFSTEP]
symm
[GOAL]
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
I✝ : MultispanIndex C
K : Multicofork I✝
I : MultispanIndex C
P : C
π : (b : I.R) → MultispanIndex.right I b ⟶ P
w :
  ∀ (a : I.L),
    MultispanIndex.fst I a ≫ π (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π (MultispanIndex.sndFrom I a)
a✝ : I.L
⊢ MultispanIndex.fst I a✝ ≫ π (MultispanIndex.fstFrom I a✝) = MultispanIndex.snd I a✝ ≫ π (MultispanIndex.sndFrom I a✝)
[PROOFSTEP]
apply w
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
a : I.L
⊢ MultispanIndex.fst I a ≫ π K (MultispanIndex.fstFrom I a) = MultispanIndex.snd I a ≫ π K (MultispanIndex.sndFrom I a)
[PROOFSTEP]
rw [← K.snd_app_right, ← K.fst_app_right]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
⊢ ∀ (s : Cocone (MultispanIndex.multispan I)) (j : WalkingMultispan I.fstFrom I.sndFrom),
    NatTrans.app K.ι j ≫ desc s = NatTrans.app s.ι j
[PROOFSTEP]
rintro S (a | b)
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
S : Cocone (MultispanIndex.multispan I)
a : I.L
⊢ NatTrans.app K.ι (WalkingMultispan.left a) ≫ desc S = NatTrans.app S.ι (WalkingMultispan.left a)
[PROOFSTEP]
rw [← K.w (WalkingMultispan.Hom.fst a), ← S.w (WalkingMultispan.Hom.fst a), Category.assoc]
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
S : Cocone (MultispanIndex.multispan I)
a : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.fst a) ≫
      NatTrans.app K.ι (WalkingMultispan.right (MultispanIndex.fstFrom I a)) ≫ desc S =
    (MultispanIndex.multispan I).map (WalkingMultispan.Hom.fst a) ≫
      NatTrans.app S.ι (WalkingMultispan.right (MultispanIndex.fstFrom I a))
[PROOFSTEP]
congr 1
[GOAL]
case left.e_a
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
S : Cocone (MultispanIndex.multispan I)
a : I.L
⊢ NatTrans.app K.ι (WalkingMultispan.right (MultispanIndex.fstFrom I a)) ≫ desc S =
    NatTrans.app S.ι (WalkingMultispan.right (MultispanIndex.fstFrom I a))
[PROOFSTEP]
apply fac
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
S : Cocone (MultispanIndex.multispan I)
b : I.R
⊢ NatTrans.app K.ι (WalkingMultispan.right b) ≫ desc S = NatTrans.app S.ι (WalkingMultispan.right b)
[PROOFSTEP]
apply fac
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
⊢ ∀ (s : Cocone (MultispanIndex.multispan I)) (m : K.pt ⟶ s.pt),
    (∀ (j : WalkingMultispan I.fstFrom I.sndFrom), NatTrans.app K.ι j ≫ m = NatTrans.app s.ι j) → m = desc s
[PROOFSTEP]
intro S m hm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
S : Cocone (MultispanIndex.multispan I)
m : K.pt ⟶ S.pt
hm : ∀ (j : WalkingMultispan I.fstFrom I.sndFrom), NatTrans.app K.ι j ≫ m = NatTrans.app S.ι j
⊢ m = desc S
[PROOFSTEP]
apply uniq
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
S : Cocone (MultispanIndex.multispan I)
m : K.pt ⟶ S.pt
hm : ∀ (j : WalkingMultispan I.fstFrom I.sndFrom), NatTrans.app K.ι j ≫ m = NatTrans.app S.ι j
⊢ ∀ (i : I.R), π K i ≫ m = π S i
[PROOFSTEP]
intro i
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : I.R), π K i ≫ desc E = π E i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), π K i ≫ m = π E i) → m = desc E
S : Cocone (MultispanIndex.multispan I)
m : K.pt ⟶ S.pt
hm : ∀ (j : WalkingMultispan I.fstFrom I.sndFrom), NatTrans.app K.ι j ≫ m = NatTrans.app S.ι j
i : I.R
⊢ π K i ≫ m = π S i
[PROOFSTEP]
apply hm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
⊢ MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K) = MultispanIndex.sndSigmaMap I ≫ Sigma.desc (π K)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b✝ : I.L
⊢ Sigma.ι I.left b✝ ≫ MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K) =
    Sigma.ι I.left b✝ ≫ MultispanIndex.sndSigmaMap I ≫ Sigma.desc (π K)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)).map f ≫
        (fun x =>
            match x with
            | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
            | WalkingParallelPair.one => Sigma.desc (π K))
          Y =
      (fun x =>
            match x with
            | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
            | WalkingParallelPair.one => Sigma.desc (π K))
          X ≫
        ((Functor.const WalkingParallelPair).obj K.pt).map f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case zero.zero.id
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)).map
        (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      (fun x =>
          match x with
          | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
          | WalkingParallelPair.one => Sigma.desc (π K))
        WalkingParallelPair.zero =
    (fun x =>
          match x with
          | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
          | WalkingParallelPair.one => Sigma.desc (π K))
        WalkingParallelPair.zero ≫
      ((Functor.const WalkingParallelPair).obj K.pt).map (WalkingParallelPairHom.id WalkingParallelPair.zero)
[PROOFSTEP]
dsimp
[GOAL]
case zero.one.left
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)).map WalkingParallelPairHom.left ≫
      (fun x =>
          match x with
          | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
          | WalkingParallelPair.one => Sigma.desc (π K))
        WalkingParallelPair.one =
    (fun x =>
          match x with
          | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
          | WalkingParallelPair.one => Sigma.desc (π K))
        WalkingParallelPair.zero ≫
      ((Functor.const WalkingParallelPair).obj K.pt).map WalkingParallelPairHom.left
[PROOFSTEP]
dsimp
[GOAL]
case zero.one.right
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)).map WalkingParallelPairHom.right ≫
      (fun x =>
          match x with
          | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
          | WalkingParallelPair.one => Sigma.desc (π K))
        WalkingParallelPair.one =
    (fun x =>
          match x with
          | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
          | WalkingParallelPair.one => Sigma.desc (π K))
        WalkingParallelPair.zero ≫
      ((Functor.const WalkingParallelPair).obj K.pt).map WalkingParallelPairHom.right
[PROOFSTEP]
dsimp
[GOAL]
case one.one.id
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)).map
        (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (fun x =>
          match x with
          | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
          | WalkingParallelPair.one => Sigma.desc (π K))
        WalkingParallelPair.one =
    (fun x =>
          match x with
          | WalkingParallelPair.zero => MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)
          | WalkingParallelPair.one => Sigma.desc (π K))
        WalkingParallelPair.one ≫
      ((Functor.const WalkingParallelPair).obj K.pt).map (WalkingParallelPairHom.id WalkingParallelPair.one)
[PROOFSTEP]
dsimp
[GOAL]
case zero.zero.id
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)).map (𝟙 WalkingParallelPair.zero) ≫
      MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K) =
    (MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)) ≫ 𝟙 K.pt
[PROOFSTEP]
simp only [Functor.map_id, parallelPair_obj_zero, parallelPair_obj_one, sigma_condition, Category.id_comp,
  Category.comp_id]
[GOAL]
case zero.one.left
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K) = (MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)) ≫ 𝟙 K.pt
[PROOFSTEP]
simp only [Functor.map_id, parallelPair_obj_zero, parallelPair_obj_one, sigma_condition, Category.id_comp,
  Category.comp_id]
[GOAL]
case zero.one.right
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ MultispanIndex.sndSigmaMap I ≫ Sigma.desc (π K) = (MultispanIndex.fstSigmaMap I ≫ Sigma.desc (π K)) ≫ 𝟙 K.pt
[PROOFSTEP]
simp only [Functor.map_id, parallelPair_obj_zero, parallelPair_obj_one, sigma_condition, Category.id_comp,
  Category.comp_id]
[GOAL]
case one.one.id
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K✝ : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)).map (𝟙 WalkingParallelPair.one) ≫
      Sigma.desc (π K) =
    Sigma.desc (π K) ≫ 𝟙 K.pt
[PROOFSTEP]
simp only [Functor.map_id, parallelPair_obj_zero, parallelPair_obj_one, sigma_condition, Category.id_comp,
  Category.comp_id]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
c : Cofork (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)
⊢ ∀ ⦃X Y : WalkingMultispan I.fstFrom I.sndFrom⦄ (f : X ⟶ Y),
    (MultispanIndex.multispan I).map f ≫
        (fun x =>
            match x with
            | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
            | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
          Y =
      (fun x =>
            match x with
            | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
            | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
          X ≫
        ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj c.pt).map f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case left.left.id
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
c : Cofork (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)
a✝ : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.id (WalkingMultispan.left a✝)) ≫
      (fun x =>
          match x with
          | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
          | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
        (WalkingMultispan.left a✝) =
    (fun x =>
          match x with
          | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
          | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
        (WalkingMultispan.left a✝) ≫
      ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj c.pt).map
        (WalkingMultispan.Hom.id (WalkingMultispan.left a✝))
[PROOFSTEP]
simp
[GOAL]
case left.right.fst
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
c : Cofork (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)
a✝ : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.fst a✝) ≫
      (fun x =>
          match x with
          | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
          | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
        (WalkingMultispan.right (MultispanIndex.fstFrom I a✝)) =
    (fun x =>
          match x with
          | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
          | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
        (WalkingMultispan.left a✝) ≫
      ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj c.pt).map (WalkingMultispan.Hom.fst a✝)
[PROOFSTEP]
simp
[GOAL]
case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
c : Cofork (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)
a✝ : I.L
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.snd a✝) ≫
      (fun x =>
          match x with
          | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
          | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
        (WalkingMultispan.right (MultispanIndex.sndFrom I a✝)) =
    (fun x =>
          match x with
          | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
          | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
        (WalkingMultispan.left a✝) ≫
      ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj c.pt).map (WalkingMultispan.Hom.snd a✝)
[PROOFSTEP]
simp [c.condition]
[GOAL]
case right.right.id
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
K : Multicofork I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
c : Cofork (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I)
a✝ : I.R
⊢ (MultispanIndex.multispan I).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      (fun x =>
          match x with
          | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
          | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
        (WalkingMultispan.right a✝) =
    (fun x =>
          match x with
          | WalkingMultispan.left a => Sigma.ι I.left a ≫ MultispanIndex.fstSigmaMap I ≫ Cofork.π c
          | WalkingMultispan.right b => Sigma.ι I.right b ≫ Cofork.π c)
        (WalkingMultispan.right a✝) ≫
      ((Functor.const (WalkingMultispan I.fstFrom I.sndFrom)).obj c.pt).map
        (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app (Multicofork.toSigmaCofork K₁).ι j ≫ f.Hom = NatTrans.app (Multicofork.toSigmaCofork K₂).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.zero ≫ f.Hom =
    NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.zero
case one
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.one ≫ f.Hom =
    NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.one
[PROOFSTEP]
all_goals {
  apply colimit.hom_ext
  rintro ⟨j⟩
  simp
}
[GOAL]
case zero
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.zero ≫ f.Hom =
    NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.zero
[PROOFSTEP]
{ apply colimit.hom_ext
  rintro ⟨j⟩
  simp
}
[GOAL]
case zero
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.zero ≫ f.Hom =
    NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.zero
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case zero.w
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ ∀ (j : Discrete I.L),
    colimit.ι (Discrete.functor I.left) j ≫
        NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.zero ≫ f.Hom =
      colimit.ι (Discrete.functor I.left) j ≫ NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.zero
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case zero.w.mk
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
j : I.L
⊢ colimit.ι (Discrete.functor I.left) { as := j } ≫
      NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.zero ≫ f.Hom =
    colimit.ι (Discrete.functor I.left) { as := j } ≫
      NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case one
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.one ≫ f.Hom =
    NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.one
[PROOFSTEP]
{ apply colimit.hom_ext
  rintro ⟨j⟩
  simp
}
[GOAL]
case one
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.one ≫ f.Hom =
    NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.one
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case one.w
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ ∀ (j : Discrete I.R),
    colimit.ι (Discrete.functor I.right) j ≫
        NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.one ≫ f.Hom =
      colimit.ι (Discrete.functor I.right) j ≫ NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.one
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case one.w.mk
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
j : I.R
⊢ colimit.ι (Discrete.functor I.right) { as := j } ≫
      NatTrans.app (Multicofork.toSigmaCofork K₁).ι WalkingParallelPair.one ≫ f.Hom =
    colimit.ι (Discrete.functor I.right) { as := j } ≫
      NatTrans.app (Multicofork.toSigmaCofork K₂).ι WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Cofork (fstSigmaMap I) (sndSigmaMap I)
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingMultispan I.fstFrom I.sndFrom),
    NatTrans.app (Multicofork.ofSigmaCofork I K₁).ι j ≫ f.Hom = NatTrans.app (Multicofork.ofSigmaCofork I K₂).ι j
[PROOFSTEP]
rintro
  (_ | _)
      -- porting note; in mathlib3, `simp` worked. What seems to be happening is that
              -- the `simp` set is not confluent, and mathlib3 found
              -- `Multicofork.ofSigmaCofork_ι_app_left` before `Multicofork.fst_app_right`,
              -- but mathlib4 finds `Multicofork.fst_app_right` first.
[GOAL]
case left
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Cofork (fstSigmaMap I) (sndSigmaMap I)
f : K₁ ⟶ K₂
a✝ : I.L
⊢ NatTrans.app (Multicofork.ofSigmaCofork I K₁).ι (WalkingMultispan.left a✝) ≫ f.Hom =
    NatTrans.app (Multicofork.ofSigmaCofork I K₂).ι (WalkingMultispan.left a✝)
case right
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Cofork (fstSigmaMap I) (sndSigmaMap I)
f : K₁ ⟶ K₂
a✝ : I.R
⊢ NatTrans.app (Multicofork.ofSigmaCofork I K₁).ι (WalkingMultispan.right a✝) ≫ f.Hom =
    NatTrans.app (Multicofork.ofSigmaCofork I K₂).ι (WalkingMultispan.right a✝)
[PROOFSTEP]
{simp [-Multicofork.fst_app_right]
}
-- porting note: similarly here, the `simp` set seems to be non-confluent
[GOAL]
case left
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Cofork (fstSigmaMap I) (sndSigmaMap I)
f : K₁ ⟶ K₂
a✝ : I.L
⊢ NatTrans.app (Multicofork.ofSigmaCofork I K₁).ι (WalkingMultispan.left a✝) ≫ f.Hom =
    NatTrans.app (Multicofork.ofSigmaCofork I K₂).ι (WalkingMultispan.left a✝)
[PROOFSTEP]
simp [-Multicofork.fst_app_right]
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Cofork (fstSigmaMap I) (sndSigmaMap I)
f : K₁ ⟶ K₂
a✝ : I.R
⊢ NatTrans.app (Multicofork.ofSigmaCofork I K₁).ι (WalkingMultispan.right a✝) ≫ f.Hom =
    NatTrans.app (Multicofork.ofSigmaCofork I K₂).ι (WalkingMultispan.right a✝)
[PROOFSTEP]
{simp [-Multicofork.ofSigmaCofork_pt]
}
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K₁ K₂ : Cofork (fstSigmaMap I) (sndSigmaMap I)
f : K₁ ⟶ K₂
a✝ : I.R
⊢ NatTrans.app (Multicofork.ofSigmaCofork I K₁).ι (WalkingMultispan.right a✝) ≫ f.Hom =
    NatTrans.app (Multicofork.ofSigmaCofork I K₂).ι (WalkingMultispan.right a✝)
[PROOFSTEP]
simp [-Multicofork.ofSigmaCofork_pt]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
⊢ ∀ (j : WalkingMultispan I.fstFrom I.sndFrom),
    NatTrans.app ((𝟭 (Multicofork I)).obj K).ι j ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
      NatTrans.app ((toSigmaCoforkFunctor I ⋙ ofSigmaCoforkFunctor I).obj K).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case left
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
a✝ : I.L
⊢ NatTrans.app ((𝟭 (Multicofork I)).obj K).ι (WalkingMultispan.left a✝) ≫
      (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
    NatTrans.app ((toSigmaCoforkFunctor I ⋙ ofSigmaCoforkFunctor I).obj K).ι (WalkingMultispan.left a✝)
[PROOFSTEP]
simp
[GOAL]
case right
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Multicofork I
a✝ : I.R
⊢ NatTrans.app ((𝟭 (Multicofork I)).obj K).ι (WalkingMultispan.right a✝) ≫
      (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
    NatTrans.app ((toSigmaCoforkFunctor I ⋙ ofSigmaCoforkFunctor I).obj K).ι (WalkingMultispan.right a✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Cofork (fstSigmaMap I) (sndSigmaMap I)
⊢ Cofork.π ((ofSigmaCoforkFunctor I ⋙ toSigmaCoforkFunctor I).obj K) ≫
      (Iso.refl ((ofSigmaCoforkFunctor I ⋙ toSigmaCoforkFunctor I).obj K).pt).hom =
    Cofork.π ((𝟭 (Cofork (fstSigmaMap I) (sndSigmaMap I))).obj K)
[PROOFSTEP]
apply Limits.colimit.hom_ext
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Cofork (fstSigmaMap I) (sndSigmaMap I)
⊢ ∀ (j : Discrete I.R),
    colimit.ι (Discrete.functor I.right) j ≫
        Cofork.π ((ofSigmaCoforkFunctor I ⋙ toSigmaCoforkFunctor I).obj K) ≫
          (Iso.refl ((ofSigmaCoforkFunctor I ⋙ toSigmaCoforkFunctor I).obj K).pt).hom =
      colimit.ι (Discrete.functor I.right) j ≫ Cofork.π ((𝟭 (Cofork (fstSigmaMap I) (sndSigmaMap I))).obj K)
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case w.mk
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Cofork (fstSigmaMap I) (sndSigmaMap I)
j : I.R
⊢ colimit.ι (Discrete.functor I.right) { as := j } ≫
      Cofork.π ((ofSigmaCoforkFunctor I ⋙ toSigmaCoforkFunctor I).obj K) ≫
        (Iso.refl ((ofSigmaCoforkFunctor I ⋙ toSigmaCoforkFunctor I).obj K).pt).hom =
    colimit.ι (Discrete.functor I.right) { as := j } ≫ Cofork.π ((𝟭 (Cofork (fstSigmaMap I) (sndSigmaMap I))).obj K)
[PROOFSTEP]
dsimp
[GOAL]
case w.mk
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Cofork (fstSigmaMap I) (sndSigmaMap I)
j : I.R
⊢ colimit.ι (Discrete.functor I.right) { as := j } ≫
      Sigma.desc (Multicofork.π (Multicofork.ofSigmaCofork I K)) ≫ 𝟙 K.pt =
    colimit.ι (Discrete.functor I.right) { as := j } ≫ Cofork.π K
[PROOFSTEP]
simp only [Category.comp_id, colimit.ι_desc, Cofan.mk_ι_app]
[GOAL]
case w.mk
C : Type u
inst✝² : Category.{v, u} C
I : MultispanIndex C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
K : Cofork (fstSigmaMap I) (sndSigmaMap I)
j : I.R
⊢ Multicofork.π (Multicofork.ofSigmaCofork I K) j = colimit.ι (Discrete.functor I.right) { as := j } ≫ Cofork.π K
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
I : MulticospanIndex C
inst✝ : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : I.L), i ≫ ι I a = j ≫ ι I a
⊢ ∀ (j_1 : WalkingMulticospan I.fstTo I.sndTo),
    i ≫ limit.π (MulticospanIndex.multicospan I) j_1 = j ≫ limit.π (MulticospanIndex.multicospan I) j_1
[PROOFSTEP]
rintro (a | b)
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
I : MulticospanIndex C
inst✝ : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : I.L), i ≫ ι I a = j ≫ ι I a
a : I.L
⊢ i ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a) =
    j ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)
[PROOFSTEP]
apply h
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
I : MulticospanIndex C
inst✝ : HasMultiequalizer I
W : C
i j : W ⟶ multiequalizer I
h : ∀ (a : I.L), i ≫ ι I a = j ≫ ι I a
b : I.R
⊢ i ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b) =
    j ≫ limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)
[PROOFSTEP]
simp_rw [← limit.w I.multicospan (WalkingMulticospan.Hom.fst b), ← Category.assoc, h]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
I : MulticospanIndex C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : I.L
⊢ ιPi I ≫ Pi.π I.left a = ι I a
[PROOFSTEP]
rw [ιPi, Category.assoc, ← Iso.eq_inv_comp, isoEqualizer]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
I : MulticospanIndex C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : I.L
⊢ equalizer.ι (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I) ≫ Pi.π I.left a =
    (limit.isoLimitCone
          {
            cone :=
              (MulticospanIndex.multiforkEquivPiFork I).inverse.obj
                (limit.cone (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I))),
            isLimit :=
              IsLimit.ofPreservesConeTerminal (MulticospanIndex.multiforkEquivPiFork I).inverse
                (limit.isLimit (parallelPair (MulticospanIndex.fstPiMap I) (MulticospanIndex.sndPiMap I))) }).inv ≫
      ι I a
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
I : MultispanIndex C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : I.R), π I b ≫ i = π I b ≫ j
⊢ ∀ (j_1 : WalkingMultispan I.fstFrom I.sndFrom),
    colimit.ι (MultispanIndex.multispan I) j_1 ≫ i = colimit.ι (MultispanIndex.multispan I) j_1 ≫ j
[PROOFSTEP]
rintro (a | b)
[GOAL]
case left
C : Type u
inst✝¹ : Category.{v, u} C
I : MultispanIndex C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : I.R), π I b ≫ i = π I b ≫ j
a : I.L
⊢ colimit.ι (MultispanIndex.multispan I) (WalkingMultispan.left a) ≫ i =
    colimit.ι (MultispanIndex.multispan I) (WalkingMultispan.left a) ≫ j
[PROOFSTEP]
simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]
[GOAL]
case right
C : Type u
inst✝¹ : Category.{v, u} C
I : MultispanIndex C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : I.R), π I b ≫ i = π I b ≫ j
b : I.R
⊢ colimit.ι (MultispanIndex.multispan I) (WalkingMultispan.right b) ≫ i =
    colimit.ι (MultispanIndex.multispan I) (WalkingMultispan.right b) ≫ j
[PROOFSTEP]
apply h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
I : MultispanIndex C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.R
⊢ Sigma.ι I.right b ≫ sigmaπ I = π I b
[PROOFSTEP]
rw [sigmaπ, ← Category.assoc, Iso.comp_inv_eq, isoCoequalizer]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
I : MultispanIndex C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.R
⊢ Sigma.ι I.right b ≫ coequalizer.π (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I) =
    π I b ≫
      (colimit.isoColimitCocone
          {
            cocone :=
              (MultispanIndex.multicoforkEquivSigmaCofork I).inverse.obj
                (colimit.cocone (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))),
            isColimit :=
              IsColimit.ofPreservesCoconeInitial (MultispanIndex.multicoforkEquivSigmaCofork I).inverse
                (colimit.isColimit (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))) }).hom
[PROOFSTEP]
simp only [MultispanIndex.multicoforkEquivSigmaCofork_inverse, MultispanIndex.ofSigmaCoforkFunctor_obj,
  colimit.isoColimitCocone_ι_hom, Multicofork.ofSigmaCofork_pt, colimit.cocone_x, Multicofork.π_eq_app_right]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
I : MultispanIndex C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : I.R
⊢ Sigma.ι I.right b ≫ coequalizer.π (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I) =
    Multicofork.π
      (Multicofork.ofSigmaCofork I
        (colimit.cocone (parallelPair (MultispanIndex.fstSigmaMap I) (MultispanIndex.sndSigmaMap I))))
      b
[PROOFSTEP]
rfl
