J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
⊢ m = homMk s.pt.hom
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
⊢ m = (fun s => homMk s.pt.hom) s
simp only
case h
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
⊢ m.left = (homMk s.pt.hom).left
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
⊢ m = homMk s.pt.hom
ext
case h
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
⊢ m.left = s.pt.hom
case h
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
⊢ m.left = (homMk s.pt.hom).left
rw [Over.homMk_left _]
case h
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
this :
  (𝟭 C).map m.left ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt.hom =
    s.pt.hom ≫ (Functor.fromPUnit B).map m.right
⊢ m.left = s.pt.hom
case h
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
⊢ m.left = s.pt.hom
have := m.w
case h
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
this : m.left ≫ 𝟙 B = s.pt.hom ≫ 𝟙 B
⊢ m.left = s.pt.hom
case h
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
this :
  (𝟭 C).map m.left ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt.hom =
    s.pt.hom ≫ (Functor.fromPUnit B).map m.right
⊢ m.left = s.pt.hom
dsimp at this
no goals
case h
J : Type w
C : Type u
inst✝ : Category C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ : ∀ (j : Discrete PEmpty), m ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π.app j = s.π.app j
this : m.left ≫ 𝟙 B = s.pt.hom ≫ 𝟙 B
⊢ m.left = s.pt.hom
rwa [Category.comp_id, Category.comp_id] at this