case a
C : Type v
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), (forget C).map f x = (forget C).map g x
⊢ (forget C).map f = (forget C).map g
C : Type v
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), (forget C).map f x = (forget C).map g x
⊢ f = g
apply @Faithful.map_injective C _ (Type w) _ (forget C) _ X Y
case a
C : Type v
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), (forget C).map f x = (forget C).map g x
⊢ ConcreteCategory.forget.map f = ConcreteCategory.forget.map g
case a
C : Type v
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), (forget C).map f x = (forget C).map g x
⊢ (forget C).map f = (forget C).map g
dsimp [forget]
case a.h
C : Type v
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), (forget C).map f x = (forget C).map g x
x : ConcreteCategory.forget.obj X
⊢ ConcreteCategory.forget.map f x = ConcreteCategory.forget.map g x
case a
C : Type v
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), (forget C).map f x = (forget C).map g x
⊢ ConcreteCategory.forget.map f = ConcreteCategory.forget.map g
funext x
no goals
case a.h
C : Type v
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), (forget C).map f x = (forget C).map g x
x : ConcreteCategory.forget.obj X
⊢ ConcreteCategory.forget.map f x = ConcreteCategory.forget.map g x
exact w x