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