T : Type u₁
inst✝ : Category T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
h : (CommaMorphism.mk left✝ b).left = g.left
⊢ CommaMorphism.mk left✝ b = g
T : Type u₁
inst✝ : Category T
X✝ X : T
U V : Over X
f g : U ⟶ V
h : f.left = g.left
⊢ f = g
let ⟨_,b,_⟩ := f
T : Type u₁
inst✝ : Category T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : (CommaMorphism.mk left✝¹ b).left = (CommaMorphism.mk left✝ e).left
⊢ CommaMorphism.mk left✝¹ b = CommaMorphism.mk left✝ e
T : Type u₁
inst✝ : Category T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
h : (CommaMorphism.mk left✝ b).left = g.left
⊢ CommaMorphism.mk left✝ b = g
let ⟨_,e,_⟩ := g
case e_right
T : Type u₁
inst✝ : Category T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : (CommaMorphism.mk left✝¹ b).left = (CommaMorphism.mk left✝ e).left
⊢ b = e
T : Type u₁
inst✝ : Category T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : (CommaMorphism.mk left✝¹ b).left = (CommaMorphism.mk left✝ e).left
⊢ CommaMorphism.mk left✝¹ b = CommaMorphism.mk left✝ e
congr
no goals
case e_right
T : Type u₁
inst✝ : Category T
X✝ X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : (CommaMorphism.mk left✝¹ b).left = (CommaMorphism.mk left✝ e).left
⊢ b = e
simp only [eq_iff_true_of_subsingleton]