[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
[PROOFSTEP]
have eq₁ := D.t_fac i i j
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = pullback.fst ≫ t D i i
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
[PROOFSTEP]
have eq₂ := (IsIso.eq_comp_inv (D.f i i)).mpr (@pullback.condition _ _ _ _ _ _ (D.f i j) _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = pullback.fst ≫ t D i i
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
[PROOFSTEP]
rw [D.t_id, Category.comp_id, eq₂] at eq₁ 
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
[PROOFSTEP]
have eq₃ := (IsIso.eq_comp_inv (D.f i i)).mp eq₁
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₃ : (t' D i i j ≫ pullback.snd) ≫ f D i i = pullback.snd ≫ f D i j
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
[PROOFSTEP]
rw [Category.assoc, ← pullback.condition, ← Category.assoc] at eq₃ 
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₃ : (t' D i i j ≫ pullback.fst) ≫ f D i j = pullback.snd ≫ f D i j
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
[PROOFSTEP]
exact Mono.right_cancellation _ _ ((Mono.right_cancellation _ _ eq₃).trans (pullbackSymmetry_hom_comp_fst _ _).symm)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
⊢ t' D j i i = pullback.fst ≫ t D j i ≫ inv pullback.snd
[PROOFSTEP]
rw [← Category.assoc, ← D.t_fac]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
⊢ t' D j i i = (t' D j i i ≫ pullback.snd) ≫ inv pullback.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
⊢ t' D i j i = pullback.fst ≫ t D i j ≫ inv pullback.snd
[PROOFSTEP]
rw [← Category.assoc, ← D.t_fac]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
⊢ t' D i j i = (t' D i j i ≫ pullback.snd) ≫ inv pullback.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
[PROOFSTEP]
have eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd ≫ inv pullback.fst := by simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
⊢ (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
[PROOFSTEP]
have := D.cocycle i j i
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : t' D i j i ≫ t' D j i i ≫ t' D i i j = 𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
[PROOFSTEP]
rw [D.t'_iij, D.t'_jii, D.t'_iji, fst_eq_snd_of_mono_eq, eq] at this 
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this :
  (pullback.fst ≫ t D i j ≫ inv pullback.snd) ≫
      (pullback.snd ≫ t D j i ≫ inv pullback.snd) ≫ pullback.snd ≫ inv pullback.fst =
    𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
[PROOFSTEP]
simp only [Category.assoc, IsIso.inv_hom_id_assoc] at this 
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : pullback.fst ≫ t D i j ≫ t D j i ≫ inv pullback.fst = 𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
[PROOFSTEP]
rw [← IsIso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq] at this 
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : t D i j ≫ t D j i = (inv pullback.fst ≫ 𝟙 (pullback (f D i j) (f D i i))) ≫ pullback.fst
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j k : D.J
⊢ t' D i j k ≫ (pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom =
    𝟙 (pullback (f D i j) (f D i k))
[PROOFSTEP]
rw [← cancel_mono (pullback.fst : pullback (D.f i j) (D.f i k) ⟶ _)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j k : D.J
⊢ (t' D i j k ≫ (pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom) ≫
      pullback.fst =
    𝟙 (pullback (f D i j) (f D i k)) ≫ pullback.fst
[PROOFSTEP]
simp [t_fac, t_fac_assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j k : D.J
⊢ (t' D j k i ≫ t' D k i j) ≫ t' D i j k = 𝟙 (pullback (f D j k) (f D j i))
[PROOFSTEP]
simpa using D.cocycle _ _ _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j k : D.J
⊢ t' D j k i ≫ t' D k i j =
    (pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom
[PROOFSTEP]
trans inv (D.t' i j k)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j k : D.J
⊢ t' D j k i ≫ t' D k i j = inv (t' D i j k)
[PROOFSTEP]
exact IsIso.eq_inv_of_hom_inv_id (D.cocycle _ _ _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j k : D.J
⊢ inv (t' D i j k) =
    (pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom
[PROOFSTEP]
rw [← cancel_mono (pullback.fst : pullback (D.f i j) (D.f i k) ⟶ _)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
i j k : D.J
⊢ inv (t' D i j k) ≫ pullback.fst =
    ((pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom) ≫
      pullback.fst
[PROOFSTEP]
simp [t_fac, t_fac_assoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
inst✝ : HasMulticoequalizer (diagram D)
i j : D.J
⊢ f D i j ≫ ι D i = (t D i j ≫ f D j i) ≫ ι D j
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
C' : Type u₂
inst✝² : Category.{v, u₂} C'
D : GlueData C
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : HasColimits C
⊢ Epi (π D)
[PROOFSTEP]
unfold π
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
C' : Type u₂
inst✝² : Category.{v, u₂} C'
D : GlueData C
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : HasColimits C
⊢ Epi (Multicoequalizer.sigmaπ (diagram D))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D✝ : GlueData C
D : GlueData (Type u_1)
x : glued D
⊢ ∃ i y, ι D i y = x
[PROOFSTEP]
delta CategoryTheory.GlueData.ι
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D✝ : GlueData C
D : GlueData (Type u_1)
x : glued D
⊢ ∃ i y, Multicoequalizer.π (diagram D) i y = x
[PROOFSTEP]
simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D✝ : GlueData C
D : GlueData (Type u_1)
x : glued D
⊢ ∃ i y, (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y = x
[PROOFSTEP]
rcases D.types_π_surjective x with
  ⟨x', rfl⟩
    --have := colimit.isoColimitCocone (Types.coproductColimitCocone _)
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
⊢ ∃ i y, (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y = π D x'
[PROOFSTEP]
rw [←
  show (colimit.isoColimitCocone (Types.coproductColimitCocone _)).inv _ = x' from
    ConcreteCategory.congr_hom (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
⊢ ∃ i y,
    (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y =
      π D
        ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv
          ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).hom x'))
[PROOFSTEP]
rcases(colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom x' with ⟨i, y⟩
[GOAL]
case intro.mk
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
i : D.J
y : U D i
⊢ ∃ i_1 y_1,
    (Sigma.ι (diagram D).right i_1 ≫ Multicoequalizer.sigmaπ (diagram D)) y_1 =
      π D ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv { fst := i, snd := y })
[PROOFSTEP]
exact
  ⟨i, y, by
    simp [← Multicoequalizer.ι_sigmaπ, -Multicoequalizer.ι_sigmaπ]
    rfl⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
i : D.J
y : U D i
⊢ (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y =
    π D ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv { fst := i, snd := y })
[PROOFSTEP]
simp [← Multicoequalizer.ι_sigmaπ, -Multicoequalizer.ι_sigmaπ]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
i : D.J
y : U D i
⊢ Multicoequalizer.sigmaπ (diagram D) (Sigma.ι D.U i y) =
    π D ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv { fst := i, snd := y })
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
i : D.J
⊢ (fun i j => F.map (t D i j)) i i = 𝟙 ((fun i => F.obj (V D i)) (i, i))
[PROOFSTEP]
simp [D.t_id i]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
i j k : D.J
⊢ (fun i j k =>
          (PreservesPullback.iso F (f D i j) (f D i k)).inv ≫
            F.map (t' D i j k) ≫ (PreservesPullback.iso F (f D j k) (f D j i)).hom)
        i j k ≫
      pullback.snd =
    pullback.fst ≫ (fun i j => F.map (t D i j)) i j
[PROOFSTEP]
simpa [Iso.inv_comp_eq] using congr_arg (fun f => F.map f) (D.t_fac i j k)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
i j k : D.J
⊢ (fun i j k =>
          (PreservesPullback.iso F (f D i j) (f D i k)).inv ≫
            F.map (t' D i j k) ≫ (PreservesPullback.iso F (f D j k) (f D j i)).hom)
        i j k ≫
      (fun i j k =>
            (PreservesPullback.iso F (f D i j) (f D i k)).inv ≫
              F.map (t' D i j k) ≫ (PreservesPullback.iso F (f D j k) (f D j i)).hom)
          j k i ≫
        (fun i j k =>
            (PreservesPullback.iso F (f D i j) (f D i k)).inv ≫
              F.map (t' D i j k) ≫ (PreservesPullback.iso F (f D j k) (f D j i)).hom)
          k i j =
    𝟙 (pullback ((fun i j => F.map (f D i j)) i j) ((fun i j => F.map (f D i j)) i k))
[PROOFSTEP]
simp only [Category.assoc, Iso.hom_inv_id_assoc, ← Functor.map_comp_assoc, D.cocycle, Iso.inv_hom_id,
  CategoryTheory.Functor.map_id, Category.id_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
⊢ ∀ {X Y : WalkingMultispan (diagram D).fstFrom (diagram D).sndFrom} (f : X ⟶ Y),
    (MultispanIndex.multispan (diagram D) ⋙ F).map f ≫
        ((fun x =>
              match x with
              | WalkingMultispan.left a =>
                Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right b =>
                Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
            Y).hom =
      ((fun x =>
              match x with
              | WalkingMultispan.left a =>
                Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right b =>
                Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
            X).hom ≫
        (MultispanIndex.multispan (diagram (mapGlueData D F))).map f
[PROOFSTEP]
rintro (⟨_, _⟩ | _) _ (_ | _ | _)
[GOAL]
case left.mk.id
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
fst✝ snd✝ : D.J
⊢ (MultispanIndex.multispan (diagram D) ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝))) ≫
      ((fun x =>
            match x with
            | WalkingMultispan.left a =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
            | WalkingMultispan.right b =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
          (WalkingMultispan.left (fst✝, snd✝))).hom =
    ((fun x =>
            match x with
            | WalkingMultispan.left a =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
            | WalkingMultispan.right b =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
          (WalkingMultispan.left (fst✝, snd✝))).hom ≫
      (MultispanIndex.multispan (diagram (mapGlueData D F))).map
        (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝)))
[PROOFSTEP]
erw [Category.comp_id, Category.id_comp, Functor.map_id]
[GOAL]
case left.mk.id
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
fst✝ snd✝ : D.J
⊢ 𝟙 ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left (fst✝, snd✝))) =
    (MultispanIndex.multispan (diagram (mapGlueData D F))).map
      (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝)))
[PROOFSTEP]
rfl
[GOAL]
case left.mk.fst
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
fst✝ snd✝ : D.J
⊢ (MultispanIndex.multispan (diagram D) ⋙ F).map (WalkingMultispan.Hom.fst (fst✝, snd✝)) ≫
      ((fun x =>
            match x with
            | WalkingMultispan.left a =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
            | WalkingMultispan.right b =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
          (WalkingMultispan.right (MultispanIndex.fstFrom (diagram D) (fst✝, snd✝)))).hom =
    ((fun x =>
            match x with
            | WalkingMultispan.left a =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
            | WalkingMultispan.right b =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
          (WalkingMultispan.left (fst✝, snd✝))).hom ≫
      (MultispanIndex.multispan (diagram (mapGlueData D F))).map (WalkingMultispan.Hom.fst (fst✝, snd✝))
[PROOFSTEP]
erw [Category.comp_id, Category.id_comp]
[GOAL]
case left.mk.fst
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
fst✝ snd✝ : D.J
⊢ (MultispanIndex.multispan (diagram D) ⋙ F).map (WalkingMultispan.Hom.fst (fst✝, snd✝)) =
    (MultispanIndex.multispan (diagram (mapGlueData D F))).map (WalkingMultispan.Hom.fst (fst✝, snd✝))
[PROOFSTEP]
rfl
[GOAL]
case left.mk.snd
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
fst✝ snd✝ : D.J
⊢ (MultispanIndex.multispan (diagram D) ⋙ F).map (WalkingMultispan.Hom.snd (fst✝, snd✝)) ≫
      ((fun x =>
            match x with
            | WalkingMultispan.left a =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
            | WalkingMultispan.right b =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
          (WalkingMultispan.right (MultispanIndex.sndFrom (diagram D) (fst✝, snd✝)))).hom =
    ((fun x =>
            match x with
            | WalkingMultispan.left a =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
            | WalkingMultispan.right b =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
          (WalkingMultispan.left (fst✝, snd✝))).hom ≫
      (MultispanIndex.multispan (diagram (mapGlueData D F))).map (WalkingMultispan.Hom.snd (fst✝, snd✝))
[PROOFSTEP]
erw [Category.comp_id, Category.id_comp, Functor.map_comp]
[GOAL]
case left.mk.snd
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
fst✝ snd✝ : D.J
⊢ F.map (t D fst✝ snd✝) ≫ F.map (f D snd✝ fst✝) =
    (MultispanIndex.multispan (diagram (mapGlueData D F))).map (WalkingMultispan.Hom.snd (fst✝, snd✝))
[PROOFSTEP]
rfl
[GOAL]
case right.id
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
a✝ : (diagram D).R
⊢ (MultispanIndex.multispan (diagram D) ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      ((fun x =>
            match x with
            | WalkingMultispan.left a =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
            | WalkingMultispan.right b =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
          (WalkingMultispan.right a✝)).hom =
    ((fun x =>
            match x with
            | WalkingMultispan.left a =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.left a))
            | WalkingMultispan.right b =>
              Iso.refl ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right b)))
          (WalkingMultispan.right a✝)).hom ≫
      (MultispanIndex.multispan (diagram (mapGlueData D F))).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))
[PROOFSTEP]
erw [Category.comp_id, Category.id_comp, Functor.map_id]
[GOAL]
case right.id
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
a✝ : (diagram D).R
⊢ 𝟙 ((MultispanIndex.multispan (diagram D) ⋙ F).obj (WalkingMultispan.right a✝)) =
    (MultispanIndex.multispan (diagram (mapGlueData D F))).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
C' : Type u₂
inst✝² : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i : D.J
⊢ F.map (ι D i) ≫ (gluedIso D F).hom = ι (mapGlueData D F) i
[PROOFSTEP]
haveI : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
C' : Type u₂
inst✝² : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i : D.J
this : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F)))
⊢ F.map (ι D i) ≫ (gluedIso D F).hom = ι (mapGlueData D F) i
[PROOFSTEP]
erw [ι_preservesColimitsIso_hom_assoc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
C' : Type u₂
inst✝² : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i : D.J
this : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F)))
⊢ colimit.ι (MultispanIndex.multispan (diagram D) ⋙ F) (WalkingMultispan.right i) ≫
      (HasColimit.isoOfNatIso (diagramIso D F)).hom =
    ι (mapGlueData D F) i
[PROOFSTEP]
rw [HasColimit.isoOfNatIso_ι_hom]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
C' : Type u₂
inst✝² : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i : D.J
this : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F)))
⊢ NatTrans.app (diagramIso D F).hom (WalkingMultispan.right i) ≫
      colimit.ι (MultispanIndex.multispan (diagram (mapGlueData D F))) (WalkingMultispan.right i) =
    ι (mapGlueData D F) i
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
C' : Type u₂
inst✝² : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i : D.J
this : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F)))
⊢ colimit.ι (MultispanIndex.multispan (diagram (mapGlueData D F))) (WalkingMultispan.right i) = ι (mapGlueData D F) i
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
C' : Type u₂
inst✝² : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i : D.J
⊢ ι (mapGlueData D F) i ≫ (gluedIso D F).inv = F.map (ι D i)
[PROOFSTEP]
rw [Iso.comp_inv_eq, ι_gluedIso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ IsLimit (vPullbackCone D i j)
[PROOFSTEP]
apply isLimitOfReflects F
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ IsLimit (F.mapCone (vPullbackCone D i j))
[PROOFSTEP]
apply (isLimitMapConePullbackConeEquiv _ _).symm _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ IsLimit
    (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
      (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))
[PROOFSTEP]
let e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)
[GOAL]
case e
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) := ?e
⊢ IsLimit
    (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
      (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))
[PROOFSTEP]
exact
  NatIso.ofComponents
    (fun x => by
      cases x
      exacts [D.gluedIso F, Iso.refl _])
    (by rintro (_ | _) (_ | _) (_ | _ | _) <;> simp)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
x : WalkingCospan
⊢ (cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅ (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x
[PROOFSTEP]
cases x
[GOAL]
case none
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ (cospan (F.map (ι D i)) (F.map (ι D j))).obj none ≅ (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj none
case some
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
val✝ : WalkingPair
⊢ (cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val✝) ≅
    (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj (some val✝)
[PROOFSTEP]
exacts [D.gluedIso F, Iso.refl _]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ ∀ {X Y : WalkingCospan} (f : X ⟶ Y),
    (cospan (F.map (ι D i)) (F.map (ι D j))).map f ≫
        ((fun x =>
              Option.casesOn (motive := fun t =>
                x = t →
                  ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                    (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
                x (fun h => (_ : none = x) ▸ gluedIso D F)
                (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
                (_ : x = x))
            Y).hom =
      ((fun x =>
              Option.casesOn (motive := fun t =>
                x = t →
                  ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                    (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
                x (fun h => (_ : none = x) ▸ gluedIso D F)
                (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
                (_ : x = x))
            X).hom ≫
        (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).map f
[PROOFSTEP]
rintro (_ | _) (_ | _) (_ | _ | _)
[GOAL]
case none.none.id
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ (cospan (F.map (ι D i)) (F.map (ι D j))).map (WidePullbackShape.Hom.id none) ≫
      ((fun x =>
            Option.casesOn (motive := fun t =>
              x = t →
                ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                  (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
              x (fun h => (_ : none = x) ▸ gluedIso D F)
              (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
              (_ : x = x))
          none).hom =
    ((fun x =>
            Option.casesOn (motive := fun t =>
              x = t →
                ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                  (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
              x (fun h => (_ : none = x) ▸ gluedIso D F)
              (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
              (_ : x = x))
          none).hom ≫
      (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).map (WidePullbackShape.Hom.id none)
[PROOFSTEP]
simp
[GOAL]
case some.none.term.left
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ (cospan (F.map (ι D i)) (F.map (ι D j))).map (WidePullbackShape.Hom.term WalkingPair.left) ≫
      ((fun x =>
            Option.casesOn (motive := fun t =>
              x = t →
                ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                  (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
              x (fun h => (_ : none = x) ▸ gluedIso D F)
              (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
              (_ : x = x))
          none).hom =
    ((fun x =>
            Option.casesOn (motive := fun t =>
              x = t →
                ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                  (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
              x (fun h => (_ : none = x) ▸ gluedIso D F)
              (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
              (_ : x = x))
          (some WalkingPair.left)).hom ≫
      (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).map (WidePullbackShape.Hom.term WalkingPair.left)
[PROOFSTEP]
simp
[GOAL]
case some.none.term.right
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
⊢ (cospan (F.map (ι D i)) (F.map (ι D j))).map (WidePullbackShape.Hom.term WalkingPair.right) ≫
      ((fun x =>
            Option.casesOn (motive := fun t =>
              x = t →
                ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                  (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
              x (fun h => (_ : none = x) ▸ gluedIso D F)
              (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
              (_ : x = x))
          none).hom =
    ((fun x =>
            Option.casesOn (motive := fun t =>
              x = t →
                ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                  (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
              x (fun h => (_ : none = x) ▸ gluedIso D F)
              (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
              (_ : x = x))
          (some WalkingPair.right)).hom ≫
      (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).map (WidePullbackShape.Hom.term WalkingPair.right)
[PROOFSTEP]
simp
[GOAL]
case some.some.id
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
val✝ : WalkingPair
⊢ (cospan (F.map (ι D i)) (F.map (ι D j))).map (WidePullbackShape.Hom.id (some val✝)) ≫
      ((fun x =>
            Option.casesOn (motive := fun t =>
              x = t →
                ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                  (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
              x (fun h => (_ : none = x) ▸ gluedIso D F)
              (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
              (_ : x = x))
          (some val✝)).hom =
    ((fun x =>
            Option.casesOn (motive := fun t =>
              x = t →
                ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
                  (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
              x (fun h => (_ : none = x) ▸ gluedIso D F)
              (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val)))
              (_ : x = x))
          (some val✝)).hom ≫
      (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).map (WidePullbackShape.Hom.id (some val✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ IsLimit
    (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
      (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))
[PROOFSTEP]
apply IsLimit.postcomposeHomEquiv e _ _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ IsLimit
    ((Cones.postcompose e.hom).obj
      (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
        (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j))))
[PROOFSTEP]
apply hc.ofIsoLimit
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ vPullbackCone (mapGlueData D F) i j ≅
    (Cones.postcompose e.hom).obj
      (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
        (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))
[PROOFSTEP]
refine' Cones.ext (Iso.refl _) _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ ∀ (j_1 : WalkingCospan),
    NatTrans.app (vPullbackCone (mapGlueData D F) i j).π j_1 =
      (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
        NatTrans.app
          ((Cones.postcompose e.hom).obj
              (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
                (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))).π
          j_1
[PROOFSTEP]
rintro (_ | _ | _)
[GOAL]
case none
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π none =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      NatTrans.app
        ((Cones.postcompose e.hom).obj
            (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))).π
        none
case some.left
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π (some WalkingPair.left) =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      NatTrans.app
        ((Cones.postcompose e.hom).obj
            (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))).π
        (some WalkingPair.left)
case some.right
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π (some WalkingPair.right) =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      NatTrans.app
        ((Cones.postcompose e.hom).obj
            (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))).π
        (some WalkingPair.right)
[PROOFSTEP]
change _ = _ ≫ (_ ≫ _) ≫ _
[GOAL]
case none
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π none =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      (F.map (f D i j) ≫ F.map (ι D i)) ≫ NatTrans.app e.hom none
case some.left
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π (some WalkingPair.left) =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      NatTrans.app
        ((Cones.postcompose e.hom).obj
            (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))).π
        (some WalkingPair.left)
case some.right
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π (some WalkingPair.right) =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      NatTrans.app
        ((Cones.postcompose e.hom).obj
            (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))).π
        (some WalkingPair.right)
[PROOFSTEP]
all_goals change _ = 𝟙 _ ≫ _ ≫ _; aesop_cat
[GOAL]
case none
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π none =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      (F.map (f D i j) ≫ F.map (ι D i)) ≫ NatTrans.app e.hom none
[PROOFSTEP]
change _ = 𝟙 _ ≫ _ ≫ _
[GOAL]
case none
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π none =
    𝟙 (((Functor.const WalkingCospan).obj (vPullbackCone (mapGlueData D F) i j).pt).obj none) ≫
      (F.map (f D i j) ≫ F.map (ι D i)) ≫ NatTrans.app e.hom none
[PROOFSTEP]
aesop_cat
[GOAL]
case some.left
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π (some WalkingPair.left) =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      NatTrans.app
        ((Cones.postcompose e.hom).obj
            (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))).π
        (some WalkingPair.left)
[PROOFSTEP]
change _ = 𝟙 _ ≫ _ ≫ _
[GOAL]
case some.left
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π (some WalkingPair.left) =
    𝟙 (((Functor.const WalkingCospan).obj (vPullbackCone (mapGlueData D F) i j).pt).obj (some WalkingPair.left)) ≫
      NatTrans.app
          (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j))).π
          (some WalkingPair.left) ≫
        NatTrans.app e.hom (some WalkingPair.left)
[PROOFSTEP]
aesop_cat
[GOAL]
case some.right
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π (some WalkingPair.right) =
    (Iso.refl (vPullbackCone (mapGlueData D F) i j).pt).hom ≫
      NatTrans.app
        ((Cones.postcompose e.hom).obj
            (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j)))).π
        (some WalkingPair.right)
[PROOFSTEP]
change _ = 𝟙 _ ≫ _ ≫ _
[GOAL]
case some.right
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝² : HasMulticoequalizer (diagram D)
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (ι D i) (ι D j)) F
hc : IsLimit (vPullbackCone (mapGlueData D F) i j)
e : cospan (F.map (ι D i)) (F.map (ι D j)) ≅ cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j) :=
  NatIso.ofComponents fun x =>
    Option.casesOn (motive := fun t =>
      x = t →
        ((cospan (F.map (ι D i)) (F.map (ι D j))).obj x ≅
          (cospan (ι (mapGlueData D F) i) (ι (mapGlueData D F) j)).obj x))
      x (fun h => (_ : none = x) ▸ gluedIso D F)
      (fun val h => (_ : some val = x) ▸ Iso.refl ((cospan (F.map (ι D i)) (F.map (ι D j))).obj (some val))) (_ : x = x)
⊢ NatTrans.app (vPullbackCone (mapGlueData D F) i j).π (some WalkingPair.right) =
    𝟙 (((Functor.const WalkingCospan).obj (vPullbackCone (mapGlueData D F) i j).pt).obj (some WalkingPair.right)) ≫
      NatTrans.app
          (PullbackCone.mk (F.map (f D i j)) (F.map (t D i j ≫ f D j i))
              (_ : F.map (f D i j) ≫ F.map (ι D i) = F.map (t D i j ≫ f D j i) ≫ F.map (ι D j))).π
          (some WalkingPair.right) ≫
        NatTrans.app e.hom (some WalkingPair.right)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
⊢ ∃ i y, F.map (ι D i) y = x
[PROOFSTEP]
let e := D.gluedIso F
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
⊢ ∃ i y, F.map (ι D i) y = x
[PROOFSTEP]
obtain ⟨i, y, eq⟩ := (D.mapGlueData F).types_ι_jointly_surjective (e.hom x)
[GOAL]
case intro.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : ι (mapGlueData D F) i y = e.hom x
⊢ ∃ i y, F.map (ι D i) y = x
[PROOFSTEP]
replace eq := congr_arg e.inv eq
[GOAL]
case intro.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : e.inv (ι (mapGlueData D F) i y) = e.inv (e.hom x)
⊢ ∃ i y, F.map (ι D i) y = x
[PROOFSTEP]
change ((D.mapGlueData F).ι i ≫ e.inv) y = (e.hom ≫ e.inv) x at eq 
[GOAL]
case intro.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : (ι (mapGlueData D F) i ≫ e.inv) y = (e.hom ≫ e.inv) x
⊢ ∃ i y, F.map (ι D i) y = x
[PROOFSTEP]
rw [e.hom_inv_id, D.ι_gluedIso_inv] at eq 
[GOAL]
case intro.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : F.map (ι D i) y = 𝟙 (F.obj (glued D)) x
⊢ ∃ i y, F.map (ι D i) y = x
[PROOFSTEP]
exact ⟨i, y, eq⟩
