[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
A B : StructuredArrow S T
f : A ⟶ B
⊢ A.hom ≫ T.map f.right = B.hom
[PROOFSTEP]
have := f.w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
A B : StructuredArrow S T
f : A ⟶ B
this : (Functor.fromPUnit S).map f.left ≫ B.hom = A.hom ≫ T.map f.right
⊢ A.hom ≫ T.map f.right = B.hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f f' : StructuredArrow S T
g : f.right ⟶ f'.right
w : autoParam (f.hom ≫ T.map g = f'.hom) _auto✝
⊢ f.left = f'.left
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f f' : StructuredArrow S T
g : f.right ⟶ f'.right
w : autoParam (f.hom ≫ T.map g = f'.hom) _auto✝
⊢ (Functor.fromPUnit S).map (eqToHom (_ : f.left = f'.left)) ≫ f'.hom = f.hom ≫ T.map g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f f' : StructuredArrow S T
g : f.right ⟶ f'.right
w : autoParam (f.hom ≫ T.map g = f'.hom) _auto✝
⊢ 𝟙 S ≫ f'.hom = f.hom ≫ T.map g
[PROOFSTEP]
simpa using w.symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f : StructuredArrow S T
g : f.right ⟶ Y'
⊢ f.left = (mk (f.hom ≫ T.map g)).left
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f f' : StructuredArrow S T
g : f.right ≅ f'.right
w : autoParam (f.hom ≫ T.map g.hom = f'.hom) _auto✝
⊢ f.left = f'.left
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f f' : StructuredArrow S T
g : f.right ≅ f'.right
w : autoParam (f.hom ≫ T.map g.hom = f'.hom) _auto✝
⊢ (Functor.fromPUnit S).map (eqToIso (_ : f.left = f'.left)).hom ≫ f'.hom = f.hom ≫ T.map g.hom
[PROOFSTEP]
simpa [eqToHom_map] using w.symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f : StructuredArrow S T
⊢ (map (𝟙 S)).obj f = f
[PROOFSTEP]
rw [eq_mk f]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f : StructuredArrow S T
⊢ (map (𝟙 S)).obj (mk f.hom) = mk f.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj h = (map f).obj ((map f').obj h)
[PROOFSTEP]
rw [eq_mk h]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f).obj ((map f').obj (mk h.hom))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ Z.hom ≫ T.map (inv ((proj S T).map f)) = Y.hom
[PROOFSTEP]
rw [Functor.map_inv, IsIso.comp_inv_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ Z.hom = Y.hom ≫ T.map ((proj S T).map f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) = 𝟙 Y ∧ homMk (inv ((proj S T).map f)) ≫ f = 𝟙 Z
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) = 𝟙 Y
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ homMk (inv ((proj S T).map f)) ≫ f = 𝟙 Z
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ (f ≫ homMk (inv ((proj S T).map f))).left = (𝟙 Y).left
[PROOFSTEP]
dsimp at t ⊢
[GOAL]
case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ (f ≫ homMk (inv ((proj S T).map f))).right = (𝟙 Y).right
[PROOFSTEP]
dsimp at t ⊢
[GOAL]
case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ (homMk (inv ((proj S T).map f)) ≫ f).left = (𝟙 Z).left
[PROOFSTEP]
dsimp at t ⊢
[GOAL]
case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ (homMk (inv ((proj S T).map f)) ≫ f).right = (𝟙 Z).right
[PROOFSTEP]
dsimp at t ⊢
[GOAL]
case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso f.right
⊢ f.right ≫ inv f.right = 𝟙 Y.right
[PROOFSTEP]
simp
[GOAL]
case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' : C
T T' : C ⥤ D
Y Z : StructuredArrow S T
f : Y ⟶ Z
t : IsIso f.right
⊢ inv f.right ≫ f.right = 𝟙 Z.right
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
inst✝¹ : Full T
inst✝ : Faithful T
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι j ≫ m = NatTrans.app c.ι j
⊢ m = (fun c => homMk (T.preimage c.pt.hom)) c
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
inst✝¹ : Full T
inst✝ : Faithful T
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι j ≫ m = NatTrans.app c.ι j
⊢ m.left = ((fun c => homMk (T.preimage c.pt.hom)) c).left
[PROOFSTEP]
aesop_cat
[GOAL]
case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
inst✝¹ : Full T
inst✝ : Faithful T
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι j ≫ m = NatTrans.app c.ι j
⊢ m.right = ((fun c => homMk (T.preimage c.pt.hom)) c).right
[PROOFSTEP]
apply T.map_injective
[GOAL]
case right.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
inst✝¹ : Full T
inst✝ : Faithful T
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι j ≫ m = NatTrans.app c.ι j
⊢ T.map m.right = T.map ((fun c => homMk (T.preimage c.pt.hom)) c).right
[PROOFSTEP]
simpa only [homMk_right, T.image_preimage, ← w m] using (Category.id_comp _).symm
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S✝ S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
X✝ Y✝ : StructuredArrow S F
f : X✝ ⟶ Y✝
⊢ ((fun X => mk (G.map X.hom)) X✝).hom ≫ (F ⋙ G).map f.right = ((fun X => mk (G.map X.hom)) Y✝).hom
[PROOFSTEP]
simp [Functor.comp_map, ← G.map_comp, ← f.w]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S✝ S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
x✝³ x✝² : StructuredArrow S F
x✝¹ x✝ : x✝³ ⟶ x✝²
h : (post S F G).map x✝¹ = (post S F G).map x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa [ext_iff] using h
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
S✝ S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
inst✝ : Faithful G
x✝¹ x✝ : StructuredArrow S F
f : (post S F G).obj x✝¹ ⟶ (post S F G).obj x✝
⊢ G.map (x✝¹.hom ≫ F.map f.right) = G.map x✝.hom
[PROOFSTEP]
simpa using f.w.symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
S✝ S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
inst✝ : Full G
h : StructuredArrow (G.obj S) (F ⋙ G)
⊢ ((post S F G).obj (mk (G.preimage h.hom))).hom ≫
      (F ⋙ G).map (Iso.refl ((post S F G).obj (mk (G.preimage h.hom))).right).hom =
    h.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
⊢ Small.{v₁, max u₁ v₂} ↑((proj S T).toPrefunctor.obj ⁻¹' 𝒢)
[PROOFSTEP]
suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S ⟶ T.obj G => mk f.2
  by
  rw [this]
  infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
this : (proj S T).toPrefunctor.obj ⁻¹' 𝒢 = Set.range fun f => mk f.snd
⊢ Small.{v₁, max u₁ v₂} ↑((proj S T).toPrefunctor.obj ⁻¹' 𝒢)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
this : (proj S T).toPrefunctor.obj ⁻¹' 𝒢 = Set.range fun f => mk f.snd
⊢ Small.{v₁, max u₁ v₂} ↑(Set.range fun f => mk f.snd)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
⊢ (proj S T).toPrefunctor.obj ⁻¹' 𝒢 = Set.range fun f => mk f.snd
[PROOFSTEP]
exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by aesop_cat⟩
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' : C
T T' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
X : StructuredArrow S T
⊢ (X ∈ Set.range fun f => mk f.snd) → X ∈ (proj S T).toPrefunctor.obj ⁻¹' 𝒢
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
A B : CostructuredArrow S T
f : A ⟶ B
⊢ S.map f.left ≫ B.hom = A.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ X.left = Y.left
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ (eqToHom h).left = eqToHom (_ : X.left = Y.left)
[PROOFSTEP]
subst h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
X : CostructuredArrow S T
⊢ (eqToHom (_ : X = X)).left = eqToHom (_ : X.left = X.left)
[PROOFSTEP]
simp only [eqToHom_refl, id_left]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f f' : CostructuredArrow S T
g : f.left ⟶ f'.left
w : autoParam (S.map g ≫ f'.hom = f.hom) _auto✝
⊢ f.right = f'.right
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f f' : CostructuredArrow S T
g : f.left ⟶ f'.left
w : autoParam (S.map g ≫ f'.hom = f.hom) _auto✝
⊢ S.map g ≫ f'.hom = f.hom ≫ (Functor.fromPUnit T).map (eqToHom (_ : f.right = f'.right))
[PROOFSTEP]
simpa [eqToHom_map] using w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f : CostructuredArrow S T
g : Y' ⟶ f.left
⊢ (mk (S.map g ≫ f.hom)).right = f.right
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : autoParam (S.map g.hom ≫ f'.hom = f.hom) _auto✝
⊢ f.right = f'.right
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : autoParam (S.map g.hom ≫ f'.hom = f.hom) _auto✝
⊢ S.map g.hom ≫ f'.hom = f.hom ≫ (Functor.fromPUnit T).map (eqToIso (_ : f.right = f'.right)).hom
[PROOFSTEP]
simpa [eqToHom_map] using w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj f = f
[PROOFSTEP]
rw [eq_mk f]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj (mk f.hom) = mk f.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj h = (map f').obj ((map f).obj h)
[PROOFSTEP]
rw [eq_mk h]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f').obj ((map f).obj (mk h.hom))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ S.map (inv ((proj S T).map f)) ≫ Y.hom = Z.hom
[PROOFSTEP]
rw [Functor.map_inv, IsIso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ Y.hom = S.map ((proj S T).map f) ≫ Z.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) = 𝟙 Y ∧ homMk (inv ((proj S T).map f)) ≫ f = 𝟙 Z
[PROOFSTEP]
constructor
[GOAL]
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ f ≫ homMk (inv ((proj S T).map f)) = 𝟙 Y
[PROOFSTEP]
ext
[GOAL]
case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ homMk (inv ((proj S T).map f)) ≫ f = 𝟙 Z
[PROOFSTEP]
ext
[GOAL]
case left.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ (f ≫ homMk (inv ((proj S T).map f))).left = (𝟙 Y).left
[PROOFSTEP]
dsimp at t ⊢
[GOAL]
case right.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso ((proj S T).map f)
⊢ (homMk (inv ((proj S T).map f)) ≫ f).left = (𝟙 Z).left
[PROOFSTEP]
dsimp at t ⊢
[GOAL]
case left.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso f.left
⊢ f.left ≫ inv f.left = 𝟙 Y.left
[PROOFSTEP]
simp
[GOAL]
case right.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' : C
S S' : C ⥤ D
Y Z : CostructuredArrow S T
f : Y ⟶ Z
t : IsIso f.left
⊢ inv f.left ≫ f.left = 𝟙 Z.left
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
inst✝¹ : Full S
inst✝ : Faithful S
⊢ ∀ (s : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))) (m : s.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt),
    (∀ (j : Discrete PEmpty), m ≫ NatTrans.app (asEmptyCone (mk (𝟙 (S.obj Y)))).π j = NatTrans.app s.π j) →
      m = (fun c => homMk (S.preimage c.pt.hom)) s
[PROOFSTEP]
rintro c m -
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
inst✝¹ : Full S
inst✝ : Faithful S
c : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))
m : c.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt
⊢ m = (fun c => homMk (S.preimage c.pt.hom)) c
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
inst✝¹ : Full S
inst✝ : Faithful S
c : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))
m : c.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt
⊢ m.left = ((fun c => homMk (S.preimage c.pt.hom)) c).left
[PROOFSTEP]
apply S.map_injective
[GOAL]
case h.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
inst✝¹ : Full S
inst✝ : Faithful S
c : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))
m : c.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt
⊢ S.map m.left = S.map ((fun c => homMk (S.preimage c.pt.hom)) c).left
[PROOFSTEP]
simpa only [homMk_left, S.image_preimage, ← w m] using (Category.comp_id _).symm
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
X✝ Y✝ : CostructuredArrow F S
f : X✝ ⟶ Y✝
⊢ (F ⋙ G).map f.left ≫ ((fun X => mk (G.map X.hom)) Y✝).hom = ((fun X => mk (G.map X.hom)) X✝).hom
[PROOFSTEP]
simp [Functor.comp_map, ← G.map_comp, ← f.w]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
x✝³ x✝² : CostructuredArrow F S
x✝¹ x✝ : x✝³ ⟶ x✝²
h : (post F G S).map x✝¹ = (post F G S).map x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa [ext_iff] using h
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
inst✝ : Faithful G
x✝¹ x✝ : CostructuredArrow F S
f : (post F G S).obj x✝¹ ⟶ (post F G S).obj x✝
⊢ G.map (F.map f.left ≫ x✝.hom) = G.map x✝¹.hom
[PROOFSTEP]
simpa using f.w
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
inst✝ : Full G
h : CostructuredArrow (F ⋙ G) (G.obj S)
⊢ (F ⋙ G).map (Iso.refl ((post F G S).obj (mk (G.preimage h.hom))).left).hom ≫ h.hom =
    ((post F G S).obj (mk (G.preimage h.hom))).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
⊢ Small.{v₁, max u₁ v₂} ↑((proj S T).toPrefunctor.obj ⁻¹' 𝒢)
[PROOFSTEP]
suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S.obj G ⟶ T => mk f.2
  by
  rw [this]
  infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
this : (proj S T).toPrefunctor.obj ⁻¹' 𝒢 = Set.range fun f => mk f.snd
⊢ Small.{v₁, max u₁ v₂} ↑((proj S T).toPrefunctor.obj ⁻¹' 𝒢)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
this : (proj S T).toPrefunctor.obj ⁻¹' 𝒢 = Set.range fun f => mk f.snd
⊢ Small.{v₁, max u₁ v₂} ↑(Set.range fun f => mk f.snd)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
⊢ (proj S T).toPrefunctor.obj ⁻¹' 𝒢 = Set.range fun f => mk f.snd
[PROOFSTEP]
exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by aesop_cat⟩
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' : C
S S' : C ⥤ D
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
B : Type u₄
inst✝² : Category.{v₄, u₄} B
𝒢 : Set C
inst✝¹ : Small.{v₁, u₁} ↑𝒢
inst✝ : LocallySmall D
X : CostructuredArrow S T
⊢ (X ∈ Set.range fun f => mk f.snd) → X ∈ (proj S T).toPrefunctor.obj ⁻¹' 𝒢
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (StructuredArrow d F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ F.op.map f.unop.right.op ≫ ((fun X => CostructuredArrow.mk X.unop.hom.op) Y✝).hom =
    ((fun X => CostructuredArrow.mk X.unop.hom.op) X✝).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (StructuredArrow d F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (F.map f.unop.right).op ≫ Y✝.unop.hom.op = X✝.unop.hom.op
[PROOFSTEP]
rw [← op_comp, ← f.unop.w, Functor.const_obj_map]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (StructuredArrow d F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟙 d ≫ X✝.unop.hom).op = X✝.unop.hom.op
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (StructuredArrow (op d) F.op)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ F.map f.unop.right.unop ≫ ((fun X => CostructuredArrow.mk X.unop.hom.unop) Y✝).hom =
    ((fun X => CostructuredArrow.mk X.unop.hom.unop) X✝).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (StructuredArrow (op d) F.op)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ F.map f.unop.right.unop ≫ Y✝.unop.hom.unop = X✝.unop.hom.unop
[PROOFSTEP]
rw [← Quiver.Hom.unop_op (F.map (Quiver.Hom.unop f.unop.right)), ← unop_comp, ← F.op_map, ← f.unop.w,
  Functor.const_obj_map]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (StructuredArrow (op d) F.op)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟙 (op d) ≫ X✝.unop.hom).unop = X✝.unop.hom.unop
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (CostructuredArrow F d)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((fun X => StructuredArrow.mk X.unop.hom.op) X✝).hom ≫ F.op.map f.unop.left.op =
    ((fun X => StructuredArrow.mk X.unop.hom.op) Y✝).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (CostructuredArrow F d)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ X✝.unop.hom.op ≫ (F.map f.unop.left).op = Y✝.unop.hom.op
[PROOFSTEP]
rw [← op_comp, f.unop.w, Functor.const_obj_map]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (CostructuredArrow F d)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (Y✝.unop.hom ≫ 𝟙 d).op = Y✝.unop.hom.op
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (CostructuredArrow F.op (op d))ᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((fun X => StructuredArrow.mk X.unop.hom.unop) X✝).hom ≫ F.map f.unop.left.unop =
    ((fun X => StructuredArrow.mk X.unop.hom.unop) Y✝).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (CostructuredArrow F.op (op d))ᵒᵖ
f : X✝ ⟶ Y✝
⊢ X✝.unop.hom.unop ≫ F.map f.unop.left.unop = Y✝.unop.hom.unop
[PROOFSTEP]
rw [← Quiver.Hom.unop_op (F.map f.unop.left.unop), ← unop_comp, ← F.op_map, f.unop.w, Functor.const_obj_map]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X✝ Y✝ : (CostructuredArrow F.op (op d))ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (Y✝.unop.hom ≫ 𝟙 (op d)).unop = Y✝.unop.hom.unop
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : (StructuredArrow d F)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫ ((fun X => Iso.op (StructuredArrow.isoMk (Iso.refl X.unop.right))) Y).hom).unop =
    (((fun X => Iso.op (StructuredArrow.isoMk (Iso.refl X.unop.right))) X).hom ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f).unop
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : (StructuredArrow d F)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
          ((fun X => Iso.op (StructuredArrow.isoMk (Iso.refl X.unop.right))) Y).hom).unop.left =
    (((fun X => Iso.op (StructuredArrow.isoMk (Iso.refl X.unop.right))) X).hom ≫
          (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map
            f).unop.left
[PROOFSTEP]
dsimp [StructuredArrow.isoMk, Comma.isoMk, StructuredArrow.homMk]
[GOAL]
case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : (StructuredArrow d F)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
          ((fun X => Iso.op (StructuredArrow.isoMk (Iso.refl X.unop.right))) Y).hom).unop.right =
    (((fun X => Iso.op (StructuredArrow.isoMk (Iso.refl X.unop.right))) X).hom ≫
          (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map
            f).unop.right
[PROOFSTEP]
dsimp [StructuredArrow.isoMk, Comma.isoMk, StructuredArrow.homMk]
[GOAL]
case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : (StructuredArrow d F)ᵒᵖ
f : X ⟶ Y
⊢ 𝟙 Y.unop.right ≫ f.unop.right = f.unop.right ≫ 𝟙 X.unop.right
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : CostructuredArrow F.op (op d)
f : X ⟶ Y
⊢ ((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).map f ≫
      ((fun X =>
            CostructuredArrow.isoMk
              (Iso.refl
                (((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).obj
                    X).left))
          Y).hom =
    ((fun X =>
            CostructuredArrow.isoMk
              (Iso.refl
                (((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).obj
                    X).left))
          X).hom ≫
      (𝟭 (CostructuredArrow F.op (op d))).map f
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : CostructuredArrow F.op (op d)
f : X ⟶ Y
⊢ (((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).map f ≫
        ((fun X =>
              CostructuredArrow.isoMk
                (Iso.refl
                  (((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).obj
                      X).left))
            Y).hom).left =
    (((fun X =>
              CostructuredArrow.isoMk
                (Iso.refl
                  (((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).obj
                      X).left))
            X).hom ≫
        (𝟭 (CostructuredArrow F.op (op d))).map f).left
[PROOFSTEP]
dsimp [CostructuredArrow.isoMk, Comma.isoMk, CostructuredArrow.homMk]
[GOAL]
case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : CostructuredArrow F.op (op d)
f : X ⟶ Y
⊢ (((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).map f ≫
        ((fun X =>
              CostructuredArrow.isoMk
                (Iso.refl
                  (((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).obj
                      X).left))
            Y).hom).right =
    (((fun X =>
              CostructuredArrow.isoMk
                (Iso.refl
                  (((CostructuredArrow.toStructuredArrow' F d).rightOp ⋙ StructuredArrow.toCostructuredArrow F d).obj
                      X).left))
            X).hom ≫
        (𝟭 (CostructuredArrow F.op (op d))).map f).right
[PROOFSTEP]
dsimp [CostructuredArrow.isoMk, Comma.isoMk, CostructuredArrow.homMk]
[GOAL]
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : CostructuredArrow F.op (op d)
f : X ⟶ Y
⊢ f.left ≫ 𝟙 Y.left = 𝟙 X.left ≫ f.left
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : (CostructuredArrow F d)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
        ((fun X => Iso.op (CostructuredArrow.isoMk (Iso.refl X.unop.left))) Y).hom).unop =
    (((fun X => Iso.op (CostructuredArrow.isoMk (Iso.refl X.unop.left))) X).hom ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f).unop
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : (CostructuredArrow F d)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
          ((fun X => Iso.op (CostructuredArrow.isoMk (Iso.refl X.unop.left))) Y).hom).unop.left =
    (((fun X => Iso.op (CostructuredArrow.isoMk (Iso.refl X.unop.left))) X).hom ≫
          (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map
            f).unop.left
[PROOFSTEP]
dsimp [CostructuredArrow.isoMk, CostructuredArrow.homMk, Comma.isoMk]
[GOAL]
case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : (CostructuredArrow F d)ᵒᵖ
f : X ⟶ Y
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
          ((fun X => Iso.op (CostructuredArrow.isoMk (Iso.refl X.unop.left))) Y).hom).unop.right =
    (((fun X => Iso.op (CostructuredArrow.isoMk (Iso.refl X.unop.left))) X).hom ≫
          (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map
            f).unop.right
[PROOFSTEP]
dsimp [CostructuredArrow.isoMk, CostructuredArrow.homMk, Comma.isoMk]
[GOAL]
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : (CostructuredArrow F d)ᵒᵖ
f : X ⟶ Y
⊢ 𝟙 Y.unop.left ≫ f.unop.left = f.unop.left ≫ 𝟙 X.unop.left
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : StructuredArrow (op d) F.op
f : X ⟶ Y
⊢ ((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).map f ≫
      ((fun X =>
            StructuredArrow.isoMk
              (Iso.refl
                (((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).obj
                    X).right))
          Y).hom =
    ((fun X =>
            StructuredArrow.isoMk
              (Iso.refl
                (((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).obj
                    X).right))
          X).hom ≫
      (𝟭 (StructuredArrow (op d) F.op)).map f
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : StructuredArrow (op d) F.op
f : X ⟶ Y
⊢ (((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).map f ≫
        ((fun X =>
              StructuredArrow.isoMk
                (Iso.refl
                  (((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).obj
                      X).right))
            Y).hom).left =
    (((fun X =>
              StructuredArrow.isoMk
                (Iso.refl
                  (((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).obj
                      X).right))
            X).hom ≫
        (𝟭 (StructuredArrow (op d) F.op)).map f).left
[PROOFSTEP]
dsimp [StructuredArrow.isoMk, StructuredArrow.homMk, Comma.isoMk]
[GOAL]
case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : StructuredArrow (op d) F.op
f : X ⟶ Y
⊢ (((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).map f ≫
        ((fun X =>
              StructuredArrow.isoMk
                (Iso.refl
                  (((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).obj
                      X).right))
            Y).hom).right =
    (((fun X =>
              StructuredArrow.isoMk
                (Iso.refl
                  (((StructuredArrow.toCostructuredArrow' F d).rightOp ⋙ CostructuredArrow.toStructuredArrow F d).obj
                      X).right))
            X).hom ≫
        (𝟭 (StructuredArrow (op d) F.op)).map f).right
[PROOFSTEP]
dsimp [StructuredArrow.isoMk, StructuredArrow.homMk, Comma.isoMk]
[GOAL]
case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : StructuredArrow (op d) F.op
f : X ⟶ Y
⊢ f.right ≫ 𝟙 Y.right = 𝟙 X.right ≫ f.right
[PROOFSTEP]
simp
