[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ uncurry (𝟙 (A ⟹ X)) = NatTrans.app (exp.ev A) X
[PROOFSTEP]
rw [uncurry_eq, prod.map_id_id, id_comp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ curry (𝟙 (A ⨯ (𝟭 C).obj X)) = NatTrans.app (exp.coev A) X
[PROOFSTEP]
rw [curry_eq, (exp A).map_id (A ⨯ _)]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ NatTrans.app (exp.coev A) ((𝟭 C).obj X) ≫ 𝟙 (A ⟹ A ⨯ (𝟭 C).obj X) = NatTrans.app (exp.coev A) X
[PROOFSTEP]
apply comp_id
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
inst✝ : Exponentiable (⊤_ C)
Z✝ : C
g : Z✝ ⟶ (⊤_ C) ⟹ X
⊢ (fun {Y} f => CartesianClosed.curry ((prod.leftUnitor Y).hom ≫ f))
      ((fun {Y} f => (prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f) g) =
    g
[PROOFSTEP]
rw [curry_eq_iff, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
inst✝ : Exponentiable (⊤_ C)
Z✝ : C
g : Z✝ ⟶ X
⊢ (fun {Y} f => (prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f)
      ((fun {Y} f => CartesianClosed.curry ((prod.leftUnitor Y).hom ≫ f)) g) =
    g
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
inst✝ : Exponentiable (⊤_ C)
Z✝ Z'✝ : C
f : Z'✝ ⟶ Z✝
g : Z✝ ⟶ (⊤_ C) ⟹ X
⊢ (fun {Y} f => (prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f) (f ≫ g) =
    f ≫ (fun {Y} f => (prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f) g
[PROOFSTEP]
dsimp [-prod.leftUnitor_inv]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
inst✝ : Exponentiable (⊤_ C)
Z✝ Z'✝ : C
f : Z'✝ ⟶ Z✝
g : Z✝ ⟶ (⊤_ C) ⟹ X
⊢ (prod.leftUnitor Z'✝).inv ≫ CartesianClosed.uncurry (f ≫ g) = f ≫ (prod.leftUnitor Z✝).inv ≫ CartesianClosed.uncurry g
[PROOFSTEP]
rw [uncurry_natural_left, prod.leftUnitor_inv_naturality_assoc f]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
f : B ⟶ A
inst✝ : Exponentiable B
X : C
⊢ CartesianClosed.uncurry (NatTrans.app (pre f) X) = prod.map f (𝟙 (A ⟹ X)) ≫ NatTrans.app (exp.ev A) X
[PROOFSTEP]
rw [uncurry_eq, prod_map_pre_app_comp_ev]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A✝ B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A : C
inst✝ : Exponentiable A
⊢ pre (𝟙 A) = 𝟙 (exp A)
[PROOFSTEP]
simp [pre]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Exponentiable A
A₁ A₂ A₃ : C
inst✝² : Exponentiable A₁
inst✝¹ : Exponentiable A₂
inst✝ : Exponentiable A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f
[PROOFSTEP]
rw [pre, pre, pre, transferNatTransSelf_comp, prod.functor.map_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
⊢ prod.snd ≫ IsInitial.to t (A ⨯ I) = 𝟙 (A ⨯ I)
[PROOFSTEP]
have : (prod.snd : A ⨯ I ⟶ I) = CartesianClosed.uncurry (t.to _)
[GOAL]
case this
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
⊢ prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
this : prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
⊢ prod.snd ≫ IsInitial.to t (A ⨯ I) = 𝟙 (A ⨯ I)
[PROOFSTEP]
rw [← curry_eq_iff]
[GOAL]
case this
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
⊢ CartesianClosed.curry prod.snd = IsInitial.to t (A ⟹ I)
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
this : prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
⊢ prod.snd ≫ IsInitial.to t (A ⨯ I) = 𝟙 (A ⨯ I)
[PROOFSTEP]
apply t.hom_ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
this : prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
⊢ prod.snd ≫ IsInitial.to t (A ⨯ I) = 𝟙 (A ⨯ I)
[PROOFSTEP]
rw [this, ← uncurry_natural_right, ← eq_curry_iff]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
this : prod.snd = CartesianClosed.uncurry (IsInitial.to t (A ⟹ I))
⊢ IsInitial.to t (A ⟹ I) ≫ (exp A).map (IsInitial.to t (A ⨯ I)) = CartesianClosed.curry (𝟙 (A ⨯ I))
[PROOFSTEP]
apply t.hom_ext
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I : C
t : IsInitial I
inst✝ : CartesianClosed C
⊢ default ≫ CartesianClosed.curry ((mulZero t).hom ≫ IsInitial.to t B) = 𝟙 (I ⟹ B)
[PROOFSTEP]
rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mulZero t).inv]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I : C
t : IsInitial I
inst✝ : CartesianClosed C
⊢ (mulZero t).inv ≫ prod.map (𝟙 I) default ≫ (mulZero t).hom ≫ IsInitial.to t B =
    (mulZero t).inv ≫ CartesianClosed.uncurry (𝟙 (I ⟹ B))
[PROOFSTEP]
apply t.hom_ext
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) ≫
      CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) =
    𝟙 ((Z ⨯ X) ⨿ Z ⨯ Y)
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inl ≫
      coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) ≫
        CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) =
    coprod.inl ≫ 𝟙 ((Z ⨯ X) ⨿ Z ⨯ Y)
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inr ≫
      coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) ≫
        CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) =
    coprod.inr ≫ 𝟙 ((Z ⨯ X) ⨿ Z ⨯ Y)
[PROOFSTEP]
rw [coprod.inl_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inl_desc, uncurry_curry]
[GOAL]
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inr ≫
      coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) ≫
        CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) =
    coprod.inr ≫ 𝟙 ((Z ⨯ X) ⨿ Z ⨯ Y)
[PROOFSTEP]
rw [coprod.inr_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inr_desc, uncurry_curry]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ CartesianClosed.uncurry (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr)) ≫
      coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr) =
    𝟙 (Z ⨯ X ⨿ Y)
[PROOFSTEP]
rw [← uncurry_natural_right, ← eq_curry_iff]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr) ≫
      (exp Z).map (coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr)) =
    CartesianClosed.curry (𝟙 (Z ⨯ X ⨿ Y))
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inl ≫
      coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr) ≫
        (exp Z).map (coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr)) =
    coprod.inl ≫ CartesianClosed.curry (𝟙 (Z ⨯ X ⨿ Y))
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inr ≫
      coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr) ≫
        (exp Z).map (coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr)) =
    coprod.inr ≫ CartesianClosed.curry (𝟙 (Z ⨯ X ⨿ Y))
[PROOFSTEP]
rw [coprod.inl_desc_assoc, ← curry_natural_right, coprod.inl_desc, ← curry_natural_left, comp_id]
[GOAL]
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
inst✝¹ : HasBinaryCoproducts C
inst✝ : CartesianClosed C
X Y Z : C
⊢ coprod.inr ≫
      coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr) ≫
        (exp Z).map (coprod.desc (prod.map (𝟙 Z) coprod.inl) (prod.map (𝟙 Z) coprod.inr)) =
    coprod.inr ≫ CartesianClosed.curry (𝟙 (Z ⨯ X ⨿ Y))
[PROOFSTEP]
rw [coprod.inr_desc_assoc, ← curry_natural_right, coprod.inr_desc, ← curry_natural_left, comp_id]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
⊢ IsIso f
[PROOFSTEP]
haveI : Mono (prod.lift (𝟙 A) f ≫ (zeroMul t).hom) := mono_comp _ _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono (prod.lift (𝟙 A) f ≫ (zeroMul t).hom)
⊢ IsIso f
[PROOFSTEP]
rw [zeroMul_hom, prod.lift_snd] at this
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono f
⊢ IsIso f
[PROOFSTEP]
haveI : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
A B X X' Y Y' Z : C
inst✝¹ : HasFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this✝ : Mono f
this : IsSplitEpi f
⊢ IsIso f
[PROOFSTEP]
apply isIso_of_mono_of_isSplitEpi
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
⊢ g = h
[PROOFSTEP]
haveI := strict_initial t g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
this : IsIso g
⊢ g = h
[PROOFSTEP]
haveI := strict_initial t h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
A B✝ X X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
I B : C
t : IsInitial I
inst✝ : CartesianClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ IsInitial.to t B = h ≫ IsInitial.to t B
this✝ : IsIso g
this : IsIso h
⊢ g = h
[PROOFSTEP]
exact eq_of_inv_eq_inv (t.hom_ext _ _)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
haveI q : Exponentiable (e.inverse.obj X) := inferInstance
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X)) := q.isAdj
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
[GOAL]
case this
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
⊢ e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
apply NatIso.ofComponents _ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
⊢ (X_1 : C) → (e.functor ⋙ prod.functor.obj X ⋙ e.inverse).obj X_1 ≅ (prod.functor.obj (e.inverse.obj X)).obj X_1
[PROOFSTEP]
intro Y
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
Y : C
⊢ (e.functor ⋙ prod.functor.obj X ⋙ e.inverse).obj Y ≅ (prod.functor.obj (e.inverse.obj X)).obj Y
[PROOFSTEP]
apply asIso (prodComparison e.inverse X (e.functor.obj Y)) ≪≫ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
Y : C
⊢ e.inverse.obj X ⨯ e.inverse.obj (e.functor.obj Y) ≅ (prod.functor.obj (e.inverse.obj X)).obj Y
[PROOFSTEP]
apply prod.mapIso (Iso.refl _) (e.unitIso.app Y).symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
⊢ ∀ {X_1 Y : C} (f : X_1 ⟶ Y),
    (e.functor ⋙ prod.functor.obj X ⋙ e.inverse).map f ≫
        (asIso (prodComparison e.inverse X (e.functor.obj Y)) ≪≫
            prod.mapIso (Iso.refl (e.inverse.obj X)) (e.unitIso.app Y).symm).hom =
      (asIso (prodComparison e.inverse X (e.functor.obj X_1)) ≪≫
            prod.mapIso (Iso.refl (e.inverse.obj X)) (e.unitIso.app X_1).symm).hom ≫
        (prod.functor.obj (e.inverse.obj X)).map f
[PROOFSTEP]
intro Y Z g
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
Y Z : C
g : Y ⟶ Z
⊢ (e.functor ⋙ prod.functor.obj X ⋙ e.inverse).map g ≫
      (asIso (prodComparison e.inverse X (e.functor.obj Z)) ≪≫
          prod.mapIso (Iso.refl (e.inverse.obj X)) (e.unitIso.app Z).symm).hom =
    (asIso (prodComparison e.inverse X (e.functor.obj Y)) ≪≫
          prod.mapIso (Iso.refl (e.inverse.obj X)) (e.unitIso.app Y).symm).hom ≫
      (prod.functor.obj (e.inverse.obj X)).map g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
Y Z : C
g : Y ⟶ Z
⊢ e.inverse.map (prod.map (𝟙 X) (e.functor.map g)) ≫
      prodComparison e.inverse X (e.functor.obj Z) ≫ prod.map (𝟙 (e.inverse.obj X)) (NatTrans.app e.unitIso.inv Z) =
    (prodComparison e.inverse X (e.functor.obj Y) ≫ prod.map (𝟙 (e.inverse.obj X)) (NatTrans.app e.unitIso.inv Y)) ≫
      prod.map (𝟙 (e.inverse.obj X)) g
[PROOFSTEP]
simp [prodComparison, prod.comp_lift, ← e.inverse.map_comp, ← e.inverse.map_comp_assoc]
  -- I wonder if it would be a good idea to make `map_comp` a simp lemma the other way round
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse) := Adjunction.leftAdjointOfNatIso this.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝¹ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) :=
  Adjunction.leftAdjointOfComp e.inverse _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝² : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝¹ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
have : (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) ⋙ e.functor ≅ prod.functor.obj X :=
  by
  apply isoWhiskerRight e.counitIso (prod.functor.obj X ⋙ e.inverse ⋙ e.functor) ≪≫ _
  change prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X
  apply isoWhiskerLeft (prod.functor.obj X) e.counitIso
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝² : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝¹ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) ⋙ e.functor ≅ prod.functor.obj X
[PROOFSTEP]
apply isoWhiskerRight e.counitIso (prod.functor.obj X ⋙ e.inverse ⋙ e.functor) ≪≫ _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝² : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝¹ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ 𝟭 D ⋙ prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X
[PROOFSTEP]
change prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝² : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝¹ : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
⊢ prod.functor.obj X ⋙ e.inverse ⋙ e.functor ≅ prod.functor.obj X
[PROOFSTEP]
apply isoWhiskerLeft (prod.functor.obj X) e.counitIso
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝³ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝² : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝¹ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this✝ : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) ⋙ e.functor ≅ prod.functor.obj X
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
skip
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
A B X✝ X' Y Y' Z : C
inst✝³ : HasFiniteProducts C
inst✝² : Exponentiable A
D : Type u₂
inst✝¹ : Category.{v, u₂} D
inst✝ : HasFiniteProducts D
e : C ≌ D
h : CartesianClosed C
X : D
q : Exponentiable (e.inverse.obj X)
this✝³ : IsLeftAdjoint (prod.functor.obj (e.inverse.obj X))
this✝² : e.functor ⋙ prod.functor.obj X ⋙ e.inverse ≅ prod.functor.obj (e.inverse.obj X)
this✝¹ : IsLeftAdjoint (e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this✝ : IsLeftAdjoint (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse)
this : (e.inverse ⋙ e.functor ⋙ prod.functor.obj X ⋙ e.inverse) ⋙ e.functor ≅ prod.functor.obj X
⊢ IsLeftAdjoint (MonoidalCategory.tensorLeft X)
[PROOFSTEP]
apply Adjunction.leftAdjointOfNatIso 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
⊢ 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⟩