[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
⊢ (fun f => (initial.to (StructuredArrow.mk f)).right) ((fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
[PROOFSTEP]
let B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
⊢ (fun f => (initial.to (StructuredArrow.mk f)).right) ((fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
[PROOFSTEP]
let g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
⊢ (fun f => (initial.to (StructuredArrow.mk f)).right) ((fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
[PROOFSTEP]
have : initial.to _ = g' := by aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
⊢ initial.to B' = g'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
this : initial.to B' = g'
⊢ (fun f => (initial.to (StructuredArrow.mk f)).right) ((fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
[PROOFSTEP]
change CommaMorphism.right (initial.to B') = _
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
this : initial.to B' = g'
⊢ (initial.to B').right = g
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g
this : initial.to B' = g'
⊢ g'.right = g
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
⊢ (fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f => (initial.to (StructuredArrow.mk f)).right) f) = f
[PROOFSTEP]
let B' : StructuredArrow A G := StructuredArrow.mk f
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
B' : StructuredArrow A G := StructuredArrow.mk f
⊢ (fun g => (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f => (initial.to (StructuredArrow.mk f)).right) f) = f
[PROOFSTEP]
apply (CommaMorphism.w (initial.to B')).symm.trans (Category.id_comp _)
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
x✝¹ : C
x✝ : D
⊢ ∀ (Y' : D) (g : x✝ ⟶ Y') (h : (⊥_ StructuredArrow x✝¹ G).right ⟶ x✝),
    ↑(leftAdjointOfStructuredArrowInitialsAux G x✝¹ Y') (h ≫ g) =
      ↑(leftAdjointOfStructuredArrowInitialsAux G x✝¹ x✝) h ≫ G.map g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
⊢ Function.LeftInverse (fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) fun g =>
    (terminal.from (CostructuredArrow.mk g)).left
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
⊢ (fun g => (terminal.from (CostructuredArrow.mk g)).left) ((fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
[PROOFSTEP]
let B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
⊢ (fun g => (terminal.from (CostructuredArrow.mk g)).left) ((fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
[PROOFSTEP]
let g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
⊢ (fun g => (terminal.from (CostructuredArrow.mk g)).left) ((fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
[PROOFSTEP]
have : terminal.from _ = g' := by aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
⊢ terminal.from B' = g'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
this : terminal.from B' = g'
⊢ (fun g => (terminal.from (CostructuredArrow.mk g)).left) ((fun g => G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
[PROOFSTEP]
change CommaMorphism.left (terminal.from B') = _
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
this : terminal.from B' = g'
⊢ (terminal.from B').left = g
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g
this : terminal.from B' = g'
⊢ g'.left = g
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ ↑(rightAdjointOfCostructuredArrowTerminalsAux G B₁ A) (G.map f ≫ g) =
    f ≫ ↑(rightAdjointOfCostructuredArrowTerminalsAux G B₂ A) g
[PROOFSTEP]
rw [← Equiv.eq_symm_apply]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ G.map f ≫ g =
    ↑(rightAdjointOfCostructuredArrowTerminalsAux G B₁ A).symm
      (f ≫ ↑(rightAdjointOfCostructuredArrowTerminalsAux G B₂ A) g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).pt ⟶ s.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).ι j ≫ m = NatTrans.app s.ι j
⊢ m =
    (fun B =>
        StructuredArrow.homMk (↑(Adjunction.homEquiv h ((Functor.fromPUnit A).obj B.pt.left) B.pt.right).symm B.pt.hom))
      s
[PROOFSTEP]
apply StructuredArrow.ext
[GOAL]
case a
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).pt ⟶ s.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).ι j ≫ m = NatTrans.app s.ι j
⊢ m.right =
    ((fun B =>
          StructuredArrow.homMk
            (↑(Adjunction.homEquiv h ((Functor.fromPUnit A).obj B.pt.left) B.pt.right).symm B.pt.hom))
        s).right
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).pt ⟶ s.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).ι j ≫ m = NatTrans.app s.ι j
⊢ m.right = ↑(Adjunction.homEquiv h A s.pt.right).symm s.pt.hom
[PROOFSTEP]
rw [Equiv.eq_symm_apply, Adjunction.homEquiv_unit]
[GOAL]
case a
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : C
s : Cocone (Functor.empty (StructuredArrow A G))
m : (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).pt ⟶ s.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app (asEmptyCocone (StructuredArrow.mk (NatTrans.app h.unit A))).ι j ≫ m = NatTrans.app s.ι j
⊢ NatTrans.app h.unit A ≫ G.map m.right = s.pt.hom
[PROOFSTEP]
apply StructuredArrow.w m
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).π j = NatTrans.app s.π j
⊢ m =
    (fun B =>
        CostructuredArrow.homMk (↑(Adjunction.homEquiv h B.pt.left ((Functor.fromPUnit A).obj B.pt.right)) B.pt.hom))
      s
[PROOFSTEP]
apply CostructuredArrow.ext
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).π j = NatTrans.app s.π j
⊢ m.left =
    ((fun B =>
          CostructuredArrow.homMk (↑(Adjunction.homEquiv h B.pt.left ((Functor.fromPUnit A).obj B.pt.right)) B.pt.hom))
        s).left
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).π j = NatTrans.app s.π j
⊢ m.left = ↑(Adjunction.homEquiv h s.pt.left A) s.pt.hom
[PROOFSTEP]
rw [h.eq_homEquiv_apply, Adjunction.homEquiv_counit]
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app (asEmptyCone (CostructuredArrow.mk (NatTrans.app h.counit A))).π j = NatTrans.app s.π j
⊢ F.map m.left ≫ NatTrans.app h.counit A = s.pt.hom
[PROOFSTEP]
exact CostructuredArrow.w m
