[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


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
⊢ IsZero X
[PROOFSTEP]
refine' ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => _⟩⟩, fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default
[PROOFSTEP]
rw [← cancel_epi e.inv]
[GOAL]
case refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default
[PROOFSTEP]
apply hY.eq_of_src
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default
[PROOFSTEP]
rw [← cancel_mono e.hom]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom
[PROOFSTEP]
apply hY.eq_of_tgt
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ IsZero F
[PROOFSTEP]
constructor
[GOAL]
case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (F ⟶ Y))
[PROOFSTEP]
intro G
[GOAL]
case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (Y ⟶ F))
[PROOFSTEP]
intro G
[GOAL]
case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (F ⟶ G))
[PROOFSTEP]
refine' ⟨⟨⟨_⟩, _⟩⟩
[GOAL]
case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (G ⟶ F))
[PROOFSTEP]
refine' ⟨⟨⟨_⟩, _⟩⟩
[GOAL]
case unique_to.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ F ⟶ G
[PROOFSTEP]
refine'
  { app := fun X => (hF _).to_ _
    naturality := _ }
[GOAL]
case unique_to.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    F.map f ≫ (fun X => IsZero.to_ (_ : IsZero (F.obj X)) (G.obj X)) Y =
      (fun X => IsZero.to_ (_ : IsZero (F.obj X)) (G.obj X)) X ≫ G.map f
[PROOFSTEP]
intros
[GOAL]
case unique_to.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ (fun X => IsZero.to_ (_ : IsZero (F.obj X)) (G.obj X)) Y✝ =
    (fun X => IsZero.to_ (_ : IsZero (F.obj X)) (G.obj X)) X✝ ≫ G.map f✝
[PROOFSTEP]
exact (hF _).eq_of_src _ _
[GOAL]
case unique_to.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a = default
[PROOFSTEP]
intro f
[GOAL]
case unique_to.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : F ⟶ G
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case unique_to.refine'_2.w.h
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : F ⟶ G
x✝ : C
⊢ NatTrans.app f x✝ = NatTrans.app default x✝
[PROOFSTEP]
apply (hF _).eq_of_src _ _
[GOAL]
case unique_from.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ G ⟶ F
[PROOFSTEP]
refine'
  { app := fun X => (hF _).from_ _
    naturality := _ }
[GOAL]
case unique_from.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    G.map f ≫ (fun X => IsZero.from_ (_ : IsZero (F.obj X)) (G.obj X)) Y =
      (fun X => IsZero.from_ (_ : IsZero (F.obj X)) (G.obj X)) X ≫ F.map f
[PROOFSTEP]
intros
[GOAL]
case unique_from.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ G.map f✝ ≫ (fun X => IsZero.from_ (_ : IsZero (F.obj X)) (G.obj X)) Y✝ =
    (fun X => IsZero.from_ (_ : IsZero (F.obj X)) (G.obj X)) X✝ ≫ F.map f✝
[PROOFSTEP]
exact (hF _).eq_of_tgt _ _
[GOAL]
case unique_from.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : G ⟶ F), a = default
[PROOFSTEP]
intro f
[GOAL]
case unique_from.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : G ⟶ F
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case unique_from.refine'_2.w.h
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
f : G ⟶ F
x✝ : C
⊢ NatTrans.app f x✝ = NatTrans.app default x✝
[PROOFSTEP]
apply (hF _).eq_of_tgt _ _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
⊢ IsZero (F.obj X)
[PROOFSTEP]
let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
⊢ IsZero (F.obj X)
[PROOFSTEP]
have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
⊢ IsZero (F.obj X)
[PROOFSTEP]
let e : F ≅ G := hF.iso hG
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
e : F ≅ G := iso hF hG
⊢ IsZero (F.obj X)
[PROOFSTEP]
exact (isZero_zero _).of_iso (e.app X)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f g : X ≅ 0
⊢ f = g
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f : 0 ⟶ X
Z✝ : C
g h : Z✝ ⟶ 0
x✝ : g ≫ f = h ≫ f
⊢ g = h
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f : X ⟶ 0
Z✝ : C
g h : 0 ⟶ Z✝
x✝ : f ≫ g = f ≫ h
⊢ g = h
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
f : 0 ⟶ 0
⊢ IsIso f
[PROOFSTEP]
convert show IsIso (𝟙 (0 : C)) by infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
f : 0 ⟶ 0
⊢ IsIso (𝟙 0)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
⊢ Mono (IsInitial.to zeroIsInitial X)
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
⊢ f = g
[PROOFSTEP]
haveI := hI.isIso_to f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g
[PROOFSTEP]
haveI := hI.isIso_to g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this✝ : IsIso f
this : IsIso g
⊢ f = g
[PROOFSTEP]
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct X I
hI : IsInitial I
⊢ X ⨯ I ≅ I
[PROOFSTEP]
have := hI.isIso_to (prod.snd : X ⨯ I ⟶ I)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct X I
hI : IsInitial I
this : IsIso prod.snd
⊢ X ⨯ I ≅ I
[PROOFSTEP]
exact asIso prod.snd
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct I X
hI : IsInitial I
⊢ I ⨯ X ≅ I
[PROOFSTEP]
have := hI.isIso_to (prod.fst : I ⨯ X ⟶ I)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct I X
hI : IsInitial I
this : IsIso prod.fst
⊢ I ⨯ X ≅ I
[PROOFSTEP]
exact asIso prod.fst
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
h : ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial I
this : IsIso (f ≫ IsInitial.to hI (⊥_ C))
⊢ f ≫ IsInitial.to hI (⊥_ C) ≫ inv (f ≫ IsInitial.to hI (⊥_ C)) = 𝟙 A
[PROOFSTEP]
rw [← assoc, IsIso.hom_inv_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
⊢ f = g
[PROOFSTEP]
haveI := hI.isIso_from f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
this : IsIso f
⊢ f = g
[PROOFSTEP]
haveI := hI.isIso_from g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
this✝ : IsIso f
this : IsIso g
⊢ f = g
[PROOFSTEP]
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ IsIso (limit.π F i)
[PROOFSTEP]
classical
refine' ⟨⟨limit.lift _ ⟨_, ⟨_, _⟩⟩, _, _⟩⟩
· exact fun j => dite (j = i) (fun h => eqToHom (by cases h; rfl)) fun h => (H _ h).from _
· intro j k f
  split_ifs with h h_1 h_1
  · cases h
    cases h_1
    obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
    simp
  · cases h
    erw [Category.comp_id]
    haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
    rw [← IsIso.comp_inv_eq]
    apply (H _ h_1).hom_ext
  · cases h_1
    apply (H _ h).hom_ext
  · apply (H _ h).hom_ext
· ext
  rw [assoc, limit.lift_π]
  dsimp only
  split_ifs with h
  · cases h
    rw [id_comp, eqToHom_refl]
    exact comp_id _
  · apply (H _ h).hom_ext
· rw [limit.lift_π]
  simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ IsIso (limit.π F i)
[PROOFSTEP]
refine' ⟨⟨limit.lift _ ⟨_, ⟨_, _⟩⟩, _, _⟩⟩
[GOAL]
case refine'_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ (X : J) → ((Functor.const J).obj (F.toPrefunctor.1 i)).obj X ⟶ F.obj X
[PROOFSTEP]
exact fun j => dite (j = i) (fun h => eqToHom (by cases h; rfl)) fun h => (H _ h).from _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h : j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
        if h : Y = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj Y = F.obj Y)
        else IsTerminal.from (H Y h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj Y)) =
      (if h : X = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj X = F.obj X)
        else IsTerminal.from (H X h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj X)) ≫
        F.map f
[PROOFSTEP]
intro j k f
[GOAL]
case refine'_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
⊢ (((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      if h : k = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj k = F.obj k)
      else IsTerminal.from (H k h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k)) =
    (if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
      else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j)) ≫
      F.map f
[PROOFSTEP]
split_ifs with h h_1 h_1
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj k = F.obj k) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j) ≫ F.map f
[PROOFSTEP]
cases h
[GOAL]
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j) ≫ F.map f
[PROOFSTEP]
cases h_1
[GOAL]
case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
f : i ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) ≫ F.map f
[PROOFSTEP]
obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
[GOAL]
case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map (𝟙 i) ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) ≫ F.map (𝟙 i)
[PROOFSTEP]
simp
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj k = F.obj k) =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
cases h
[GOAL]
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
[GOAL]
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
rw [← IsIso.comp_inv_eq]
[GOAL]
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ inv (F.map f) =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j)
[PROOFSTEP]
apply (H _ h_1).hom_ext
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      IsTerminal.from (H k h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j) ≫ F.map f
[PROOFSTEP]
cases h_1
[GOAL]
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
k : J
h : ¬k = i
f : i ⟶ k
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      IsTerminal.from (H k h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) ≫ F.map f
[PROOFSTEP]
apply (H _ h).hom_ext
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      IsTerminal.from (H k h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
apply (H _ h).hom_ext
[GOAL]
case refine'_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫
      limit.lift F
        { pt := F.toPrefunctor.1 i,
          π :=
            NatTrans.mk fun j =>
              if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
              else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) } =
    𝟙 (limit F)
[PROOFSTEP]
ext
[GOAL]
case refine'_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ (limit.π F i ≫
        limit.lift F
          { pt := F.toPrefunctor.1 i,
            π :=
              NatTrans.mk fun j =>
                if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
                else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) }) ≫
      limit.π F j✝ =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
rw [assoc, limit.lift_π]
[GOAL]
case refine'_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ limit.π F i ≫
      NatTrans.app
        { pt := F.toPrefunctor.1 i,
            π :=
              NatTrans.mk fun j =>
                if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
                else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) }.π
        j✝ =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ (limit.π F i ≫
      if h : j✝ = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝ = F.obj j✝)
      else IsTerminal.from (H j✝ h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝)) =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
h : j✝ = i
⊢ limit.π F i ≫ eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝ = F.obj j✝) =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
cases h
[GOAL]
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) = 𝟙 (limit F) ≫ limit.π F i
[PROOFSTEP]
rw [id_comp, eqToHom_refl]
[GOAL]
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ 𝟙 (((Functor.const J).obj (F.toPrefunctor.1 i)).obj i) = limit.π F i
[PROOFSTEP]
exact comp_id _
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
h : ¬j✝ = i
⊢ limit.π F i ≫ IsTerminal.from (H j✝ h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝) =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
apply (H _ h).hom_ext
[GOAL]
case refine'_4
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.lift F
        { pt := F.toPrefunctor.1 i,
          π :=
            NatTrans.mk fun j =>
              if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
              else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) } ≫
      limit.π F i =
    𝟙 (F.obj i)
[PROOFSTEP]
rw [limit.lift_π]
[GOAL]
case refine'_4
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ NatTrans.app
      { pt := F.toPrefunctor.1 i,
          π :=
            NatTrans.mk fun j =>
              if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
              else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) }.π
      i =
    𝟙 (F.obj i)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal I'
this : IsIso (IsTerminal.from hI' I ≫ f)
⊢ (inv (IsTerminal.from hI' I ≫ f) ≫ IsTerminal.from hI' I) ≫ f = 𝟙 A
[PROOFSTEP]
rw [assoc, IsIso.inv_hom_id]