[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), ↑f x = ↑g x
⊢ f = g
[PROOFSTEP]
apply @Faithful.map_injective C _ (Type w) _ (forget C) _ X Y
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), ↑f x = ↑g x
⊢ (forget C).map f = (forget C).map g
[PROOFSTEP]
dsimp [forget]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), ↑f x = ↑g x
⊢ ConcreteCategory.forget.map f = ConcreteCategory.forget.map g
[PROOFSTEP]
funext x
[GOAL]
case a.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), ↑f x = ↑g x
x : ConcreteCategory.forget.obj X
⊢ ConcreteCategory.forget.map f x = ConcreteCategory.forget.map g x
[PROOFSTEP]
exact w x
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ConcreteCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Function.Bijective ((forget C).map f)
[PROOFSTEP]
rw [← isIso_iff_bijective]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ConcreteCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ IsIso ((forget C).map f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
inst✝³ : Category.{v', u'} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : Functor.PreservesMonomorphisms (forget C)
⊢ Functor.PreservesMonomorphisms (forget₂ C D ⋙ forget D)
[PROOFSTEP]
simp only [HasForget₂.forget_comp]
[GOAL]
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
inst✝³ : Category.{v', u'} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : Functor.PreservesMonomorphisms (forget C)
⊢ Functor.PreservesMonomorphisms (forget C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
inst✝³ : Category.{v', u'} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : Functor.PreservesEpimorphisms (forget C)
⊢ Functor.PreservesEpimorphisms (forget₂ C D ⋙ forget D)
[PROOFSTEP]
simp only [HasForget₂.forget_comp]
[GOAL]
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
inst✝³ : Category.{v', u'} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : Functor.PreservesEpimorphisms (forget C)
⊢ Functor.PreservesEpimorphisms (forget C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
D : Type u'
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
inst✝¹ : Category.{v', u'} D
inst✝ : ConcreteCategory D
obj : C → D
h_obj : ∀ (X : C), (forget D).obj (obj X) = (forget C).obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ((forget D).map (map f)) ((forget C).map f)
⊢ Faithful.div (forget C) (forget D) (fun X => obj X) h_obj (fun X Y f => map f) h_map ⋙ forget D = forget C
[PROOFSTEP]
apply Faithful.div_comp
