case mk
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ C
c c' : Cone F
g : c ⟶ c'
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), Hom✝ ≫ c'.π.app j = c.π.app j
w : (mk Hom✝).Hom = g.Hom
⊢ mk Hom✝ = g
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ C
c c' : Cone F
f g : c ⟶ c'
w : f.Hom = g.Hom
⊢ f = g
cases f
case mk.mk
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ C
c c' : Cone F
Hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), Hom✝¹ ≫ c'.π.app j = c.π.app j
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), Hom✝ ≫ c'.π.app j = c.π.app j
w : (mk Hom✝¹).Hom = (mk Hom✝).Hom
⊢ mk Hom✝¹ = mk Hom✝
case mk
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ C
c c' : Cone F
g : c ⟶ c'
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), Hom✝ ≫ c'.π.app j = c.π.app j
w : (mk Hom✝).Hom = g.Hom
⊢ mk Hom✝ = g
cases g
no goals
case mk.mk
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F : J ⥤ C
c c' : Cone F
Hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), Hom✝¹ ≫ c'.π.app j = c.π.app j
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), Hom✝ ≫ c'.π.app j = c.π.app j
w : (mk Hom✝¹).Hom = (mk Hom✝).Hom
⊢ mk Hom✝¹ = mk Hom✝
congr