[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
X Y : C
⊢ ∀ (a b : X ≅ Y), a = b
[PROOFSTEP]
intro i₁ i₂
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
X Y : C
i₁ i₂ : X ≅ Y
⊢ i₁ = i₂
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
X Y : C
i₁ i₂ : X ≅ Y
⊢ i₁.hom = i₂.hom
[PROOFSTEP]
apply Subsingleton.elim


[GOAL]
α : Type u₁
X : Discrete α
⊢ { as := X.as } = X
[PROOFSTEP]
ext
[GOAL]
case as
α : Type u₁
X : Discrete α
⊢ { as := X.as }.as = X.as
[PROOFSTEP]
rfl
[GOAL]
α : Type u₁
⊢ Function.LeftInverse Discrete.mk Discrete.as
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
⊢ Function.RightInverse Discrete.mk Discrete.as
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
X Y Z : Discrete α
g : X ⟶ Y
f : Y ⟶ Z
⊢ X ⟶ Z
[PROOFSTEP]
cases X
[GOAL]
case mk
α : Type u₁
Y Z : Discrete α
f : Y ⟶ Z
as✝ : α
g : { as := as✝ } ⟶ Y
⊢ { as := as✝ } ⟶ Z
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk
α : Type u₁
Z : Discrete α
as✝¹ as✝ : α
f : { as := as✝ } ⟶ Z
g : { as := as✝¹ } ⟶ { as := as✝ }
⊢ { as := as✝¹ } ⟶ Z
[PROOFSTEP]
cases Z
[GOAL]
case mk.mk.mk
α : Type u₁
as✝² as✝¹ : α
g : { as := as✝² } ⟶ { as := as✝¹ }
as✝ : α
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ { as := as✝² } ⟶ { as := as✝ }
[PROOFSTEP]
rcases f with ⟨⟨⟨⟩⟩⟩
[GOAL]
case mk.mk.mk.up.up.refl
α : Type u₁
as✝¹ as✝ : α
g : { as := as✝¹ } ⟶ { as := as✝ }
⊢ { as := as✝¹ } ⟶ { as := as✝ }
[PROOFSTEP]
exact g
[GOAL]
α : Type u₁
inst✝ : Subsingleton α
⊢ ∀ (a b : Discrete α), a = b
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
X Y : Discrete α
h : X.as = Y.as
⊢ X = Y
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
X Y : Discrete α
h : X.as = Y.as
⊢ X = Y
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
i j : Discrete I
f : i ⟶ j
⊢ f ≫ Discrete.eqToHom (_ : j.as = i.as) = 𝟙 i ∧ Discrete.eqToHom (_ : j.as = i.as) ≫ f = 𝟙 j
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ (F ∘ as) X ⟶ (F ∘ as) Y
[PROOFSTEP]
dsimp
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ F X.as ⟶ F Y.as
[PROOFSTEP]
rcases f with ⟨⟨h⟩⟩
[GOAL]
case up.up
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
h : X.as = Y.as
⊢ F X.as ⟶ F Y.as
[PROOFSTEP]
exact eqToHom (congrArg _ h)
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
i : Discrete I
f : i ⟶ i
⊢ (functor F).map f = 𝟙 (F i.as)
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X Y : Discrete I
x✝ : X ⟶ Y
g : X.as = Y.as
⊢ F.map { down := { down := g } } ≫ f Y = f X ≫ G.map { down := { down := g } }
[PROOFSTEP]
discrete_cases
[GOAL]
case mk.mk.up.up
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
as✝¹ as✝ : I
g down✝ : { as := as✝¹ }.as = { as := as✝ }.as
⊢ F.map { down := { down := g } } ≫ f { as := as✝ } = f { as := as✝¹ } ≫ G.map { down := { down := g } }
[PROOFSTEP]
rcases g
[GOAL]
case mk.mk.up.up.refl
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
as✝ : I
down✝ : { as := as✝ }.as = { as := as✝ }.as
⊢ F.map { down := { down := (_ : { as := as✝ }.as = { as := as✝ }.as) } } ≫ f { as := as✝ } =
    f { as := as✝ } ≫ G.map { down := { down := (_ : { as := as✝ }.as = { as := as✝ }.as) } }
[PROOFSTEP]
change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
[GOAL]
case mk.mk.up.up.refl
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
as✝ : I
down✝ : { as := as✝ }.as = { as := as✝ }.as
⊢ F.map (𝟙 { as := as✝ }) ≫ f { as := as✝ } = f { as := as✝ } ≫ G.map (𝟙 { as := as✝ })
[PROOFSTEP]
simp
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X✝ Y✝ : Discrete I
x✝ : X✝ ⟶ Y✝
g : X✝.as = Y✝.as
⊢ F.map { down := { down := g } } ≫ (f Y✝).hom = (f X✝).hom ≫ G.map { down := { down := g } }
[PROOFSTEP]
discrete_cases
[GOAL]
case mk.mk.up.up
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
as✝¹ as✝ : I
g down✝ : { as := as✝¹ }.as = { as := as✝ }.as
⊢ F.map { down := { down := g } } ≫ (f { as := as✝ }).hom = (f { as := as✝¹ }).hom ≫ G.map { down := { down := g } }
[PROOFSTEP]
rcases g
[GOAL]
case mk.mk.up.up.refl
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
as✝ : I
down✝ : { as := as✝ }.as = { as := as✝ }.as
⊢ F.map { down := { down := (_ : { as := as✝ }.as = { as := as✝ }.as) } } ≫ (f { as := as✝ }).hom =
    (f { as := as✝ }).hom ≫ G.map { down := { down := (_ : { as := as✝ }.as = { as := as✝ }.as) } }
[PROOFSTEP]
change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
[GOAL]
case mk.mk.up.up.refl
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
as✝ : I
down✝ : { as := as✝ }.as = { as := as✝ }.as
⊢ F.map (𝟙 { as := as✝ }) ≫ (f { as := as✝ }).hom = (f { as := as✝ }).hom ≫ G.map (𝟙 { as := as✝ })
[PROOFSTEP]
simp
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
i : Discrete I
⊢ (natIso f).app i = f i
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
i : Discrete I
⊢ (𝟭 (Discrete I)).obj i = (functor (mk ∘ ↑e) ⋙ functor (mk ∘ ↑e.symm)).obj i
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
j : Discrete J
⊢ (functor (mk ∘ ↑e.symm) ⋙ functor (mk ∘ ↑e)).obj j = (𝟭 (Discrete J)).obj j
[PROOFSTEP]
aesop_cat
[GOAL]
α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : α
⊢ (as ∘ h.inverse.obj ∘ mk) ((as ∘ h.functor.obj ∘ mk) a) = a
[PROOFSTEP]
simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2
[GOAL]
α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : β
⊢ (as ∘ h.functor.obj ∘ mk) ((as ∘ h.inverse.obj ∘ mk) a) = a
[PROOFSTEP]
simpa using eq_of_hom (h.counitIso.app (Discrete.mk a)).1
[GOAL]
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ F.map f = 𝟙 (F.obj j)
[PROOFSTEP]
have h : f = 𝟙 j := by aesop_cat
[GOAL]
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ f = 𝟙 j
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map f = 𝟙 (F.obj j)
[PROOFSTEP]
rw [h]
[GOAL]
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)
[PROOFSTEP]
simp


[GOAL]
α : Type u
inst✝ : Group α
x y : SingleObj α
f : x ⟶ y
⊢ inv f = f⁻¹
[PROOFSTEP]
apply IsIso.inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
α : Type u
inst✝ : Group α
x y : SingleObj α
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x
[PROOFSTEP]
rw [comp_as_mul, inv_mul_self, id_as_one]
[GOAL]
α✝ α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
⊢ Function.LeftInverse
    (fun f =>
      {
        toOneHom :=
          { toFun := fun x => f.map (↑(toEnd α) x), map_one' := (_ : f.map (𝟙 (star α)) = 𝟙 (f.obj (star α))) },
        map_mul' := (_ : ∀ (x y : α), f.map (y ≫ x) = f.map y ≫ f.map x) })
    fun f => Functor.mk { obj := id, map := fun {X Y} => ↑f }
[PROOFSTEP]
aesop_cat
[GOAL]
α✝ α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
⊢ Function.RightInverse
    (fun f =>
      {
        toOneHom :=
          { toFun := fun x => f.map (↑(toEnd α) x), map_one' := (_ : f.map (𝟙 (star α)) = 𝟙 (f.obj (star α))) },
        map_mul' := (_ : ∀ (x y : α), f.map (y ≫ x) = f.map y ≫ f.map x) })
    fun f => Functor.mk { obj := id, map := fun {X Y} => ↑f }
[PROOFSTEP]
aesop_cat
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
⊢ ∀ (X : C),
    { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (𝟙 X) =
      𝟙 ({ obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.obj X)
[PROOFSTEP]
intro
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
X✝ : C
⊢ { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (𝟙 X✝) =
    𝟙 ({ obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.obj X✝)
[PROOFSTEP]
simp only [SingleObj.id_as_one, mul_right_inv]
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
⊢ ∀ {X Y Z : C} (f_1 : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (f_1 ≫ g) =
      { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map f_1 ≫
        { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map g
[PROOFSTEP]
intros
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (f✝ ≫ g✝) =
    { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map f✝ ≫
      { obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map g✝
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
C : Type ?u.20048
G : Type ?u.20052
inst✝¹ : Category.{?u.20049, ?u.20048} C
inst✝ : Group G
f : C → G
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f Z✝ * (f X✝)⁻¹ = (f Y✝ * (f X✝)⁻¹) ≫ (f Z✝ * (f Y✝)⁻¹)
[PROOFSTEP]
rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_self, mul_one]
[GOAL]
α : Type u
inst✝ : Monoid α
⊢ α ≃* End (SingleObj.star α)
[PROOFSTEP]
exact SingleObj.toEnd α
[GOAL]
X✝ Y✝ : MonCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toCat.map a₁✝ = toCat.map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
simpa [toCat] using h


[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : IsSplitMono f
inst✝ : Epi f
⊢ f ≫ retraction f = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : IsSplitMono f
inst✝ : Epi f
⊢ retraction f ≫ f = 𝟙 Y
[PROOFSTEP]
simp [← cancel_epi f]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ f ≫ section_ f = 𝟙 X
[PROOFSTEP]
simp [← cancel_mono f]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ section_ f ≫ f = 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : g ≫ f = h ≫ f
⊢ g = h
[PROOFSTEP]
replace w := w =≫ sm.retraction
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : (g ≫ f) ≫ sm.retraction = (h ≫ f) ≫ sm.retraction
⊢ g = h
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : f ≫ g = f ≫ h
⊢ g = h
[PROOFSTEP]
replace w := se.section_ ≫= w
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitMono f
inst✝ : Mono hf.retraction
⊢ f ≫ hf.retraction = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitMono f
inst✝ : Mono hf.retraction
⊢ (hf.retraction ≫ f) ≫ hf.retraction = hf.retraction
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f ≫ hf.section_ = hf.section_
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f = 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
⊢ Groupoid C
[PROOFSTEP]
apply Groupoid.ofIsIso
[GOAL]
case all_is_iso
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
⊢ ∀ {X Y : C} (f : X ⟶ Y), IsIso f
[PROOFSTEP]
intro X Y f
[GOAL]
case all_is_iso
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
⊢ IsIso f
[PROOFSTEP]
have ⟨a, _⟩ := Trunc.exists_rep <| all_split_mono f
[GOAL]
case all_is_iso
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h✝ : (_ : Trunc (IsSplitMono f)) = (_ : Trunc (IsSplitMono f))
⊢ IsIso f
[PROOFSTEP]
have ⟨b, _⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
[GOAL]
case all_is_iso
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h✝¹ : (_ : Trunc (IsSplitMono f)) = (_ : Trunc (IsSplitMono f))
b : IsSplitMono (retraction f)
h✝ : (_ : Trunc (IsSplitMono (retraction f))) = (_ : Trunc (IsSplitMono (retraction f)))
⊢ IsIso f
[PROOFSTEP]
apply IsIso.of_mono_retraction
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
sm : SplitMono f
F : C ⥤ D
⊢ F.map f ≫ F.map sm.retraction = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← Functor.map_comp, SplitMono.id, Functor.map_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : C ⥤ D
⊢ F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)
[PROOFSTEP]
rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]


[GOAL]
α β : Type u
f g : α ⟶ β
h : ∀ (a : α), f a = g a
⊢ f = g
[PROOFSTEP]
funext x
[GOAL]
case h
α β : Type u
f g : α ⟶ β
h : ∀ (a : α), f a = g a
x : α
⊢ f x = g x
[PROOFSTEP]
exact h x
[GOAL]
α β γ : Type u
f : α → β
g : β → γ
inst✝ : IsIso (↾f)
⊢ Mono (↾f)
[PROOFSTEP]
infer_instance
[GOAL]
α β γ : Type u
f : α → β
g : β → γ
inst✝ : IsIso (↾f)
⊢ ↾f ≫ inv (↾f) = 𝟙 α
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Type w
X Y Z : C
σ : F ⟶ G
τ : G ⟶ H
f : X ⟶ Y
g : Y ⟶ Z
a : F.obj X
⊢ F.map (f ≫ g) a = F.map g (F.map f a)
[PROOFSTEP]
simp [types_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Type w
X Y Z : C
σ : F ⟶ G
τ : G ⟶ H
a : F.obj X
⊢ F.map (𝟙 X) a = a
[PROOFSTEP]
simp [types_id]
[GOAL]
X : Type u
x y : X
⊢ x = y → homOfElement x = homOfElement y
[PROOFSTEP]
aesop
[GOAL]
X Y : Type u
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective f
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
⊢ Mono f → Function.Injective f
[PROOFSTEP]
intro H x x' h
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : f x = f x'
⊢ x = x'
[PROOFSTEP]
skip
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : f x = f x'
⊢ x = x'
[PROOFSTEP]
rw [← homOfElement_eq_iff] at h ⊢
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : homOfElement (f x) = homOfElement (f x')
⊢ homOfElement x = homOfElement x'
[PROOFSTEP]
exact (cancel_mono f).mp h
[GOAL]
case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Injective f → Mono f
[PROOFSTEP]
exact fun H => ⟨fun g g' h => H.comp_left h⟩
[GOAL]
X Y : Type u
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective f
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
⊢ Epi f → Function.Surjective f
[PROOFSTEP]
rintro ⟨H⟩
[GOAL]
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
⊢ Function.Surjective f
[PROOFSTEP]
refine' Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => _
[GOAL]
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ g₁ = g₂
[PROOFSTEP]
rw [← Equiv.ulift.symm.injective.comp_left.eq_iff]
[GOAL]
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ (fun x x_1 => x ∘ x_1) (↑Equiv.ulift.symm) g₁ = (fun x x_1 => x ∘ x_1) (↑Equiv.ulift.symm) g₂
[PROOFSTEP]
apply H
[GOAL]
case mp.mk.a
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ f ≫ (fun x x_1 => x ∘ x_1) (↑Equiv.ulift.symm) g₁ = f ≫ (fun x x_1 => x ∘ x_1) (↑Equiv.ulift.symm) g₂
[PROOFSTEP]
change ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f
[GOAL]
case mp.mk.a
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f
[PROOFSTEP]
rw [hg]
[GOAL]
case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Surjective f → Epi f
[PROOFSTEP]
exact fun H => ⟨fun g g' h => H.injective_comp_right h⟩
[GOAL]
m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
⊢ { obj := m, map := fun {X Y} f => Functor.map f }.map (𝟙 α) =
    𝟙 ({ obj := m, map := fun {X Y} f => Functor.map f }.obj α)
[PROOFSTEP]
funext X
[GOAL]
case h
m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
X : { obj := m, map := fun {X Y} f => Functor.map f }.obj α
⊢ { obj := m, map := fun {X Y} f => Functor.map f }.map (𝟙 α) X =
    𝟙 ({ obj := m, map := fun {X Y} f => Functor.map f }.obj α) X
[PROOFSTEP]
apply id_map