/-
Copyright (c) 2017 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
Ported by: Scott Morrison

! This file was ported from Lean 3 source module category_theory.category.basic
! leanprover-community/mathlib commit 2efd2423f8d25fa57cf7a179f5d8652ab4d0df44
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.Category.Init
import Mathlib.Combinatorics.Quiver.Basic
import Mathlib.Tactic.RestateAxiom

/-!
# Categories

Defines a category, as a type class parametrised by the type of objects.

## Notations

Introduces notations
* `X ⟶ Y` for the morphism spaces (type as `\hom`),
* `𝟙 X` for the identity morphism on `X` (type as `\b1`),
* `f ≫ g` for composition in the 'arrows' convention (type as `\gg`).

Users may like to add `f ⊚ g` for composition in the standard convention, using
```lean
local notation f ` ⊚ `:80 g:80 := category.comp g f    -- type as \oo
```

## Porting note
I am experimenting with using the `aesop` tactic as a replacement for `tidy`.
-/


library_note "CategoryTheory universes"
/--
The typeclass `Category C` describes morphisms associated to objects of type `C : Type u`.

The universe levels of the objects and morphisms are independent, and will often need to be
specified explicitly, as `Category.{v} C`.

Typically any concrete example will either be a `SmallCategory`, where `v = u`,
which can be introduced as
```
universes u
variables {C : Type u} [SmallCategory C]
```
or a `LargeCategory`, where `u = v+1`, which can be introduced as
```
universes u
variables {C : Type (u+1)} [LargeCategory C]
```

In order for the library to handle these cases uniformly,
we generally work with the unconstrained `Category.{v u}`,
for which objects live in `Type u` and morphisms live in `Type v`.

Because the universe parameter `u` for the objects can be inferred from `C`
when we write `Category C`, while the universe parameter `v` for the morphisms
can not be automatically inferred, through the category theory library
we introduce universe parameters with morphism levels listed first,
as in
```
universes v u
```
or
```
universes v₁ v₂ u₁ u₂
```
when multiple independent universes are needed.

This has the effect that we can simply write `Category.{v} C`
(that is, only specifying a single parameter) while `u` will be inferred.

Often, however, it's not even necessary to include the `.{v}`.
(Although it was in earlier versions of Lean.)
If it is omitted a "free" universe will be used.
-/

namespace Std.Tactic.Ext
open Lean Elab Tactic

/-- A wrapper for `ext` that will fail if it does not make progress. -/
-- After https://github.com/leanprover/std4/pull/33
-- we can just `` evalTactic (← `(tactic| ext))``
-- (But it would be good to have a name for that, too, so we can pass it to aesop.)
def extCore': TacticM Unit
extCore' : TacticM: Type → Type
TacticM Unit: Type
Unit := do
  let gs: ?m.274
gs ← Std.Tactic.Ext.extCore: MVarId →
  List (TSyntax `rcasesPat) →
    optParam ℕ 1000000 → optParam Bool true → TermElabM (Array (MVarId × List (TSyntax `rcasesPat)))
Std.Tactic.Ext.extCore (← getMainGoal): ?m.73
(← getMainGoal: TacticM MVarId
getMainGoal(← getMainGoal): ?m.73
) []: List ?m.136
[] 1000000: ?m.147
1000000 true: Bool
true
  replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal <| gs: ?m.274
gs.map: {α : Type ?u.286} → {β : Type ?u.285} → (α → β) → Array α → Array β
map (·.1): MVarId × List (TSyntax `rcasesPat) → MVarId
(·.1) |>.toList: {α : Type ?u.300} → Array α → List α
toList

end Std.Tactic.Ext

universe v u

namespace CategoryTheory

/-- A preliminary structure on the way to defining a category,
containing the data, but none of the axioms. -/
class CategoryStruct: {obj : Type u} →
  [toQuiver : Quiver obj] → ((X : obj) → X ⟶ X) → ({X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)) → CategoryStruct obj
CategoryStruct (obj: Type u
obj : Type u: Type (u+1)
Type u) extends Quiver: Type ?u.894 → Type (max?u.894(v+1))
Quiver.{v + 1} obj: Type u
obj : Type max u (v + 1): Type ((maxu(v+1))+1)
Type max u (v + 1) where
  /-- The identity morphism on an object. -/
  id: {obj : Type u} → [self : CategoryStruct obj] → (X : obj) → X ⟶ X
id : ∀ X: obj
X : obj: Type u
obj, Hom: obj → obj → Type v
Hom X: obj
X X: obj
X
  /-- Composition of morphisms in a category, written `f ≫ g`. -/
  comp: {obj : Type u} → [self : CategoryStruct obj] → {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
comp : ∀ {X: obj
X Y: obj
Y Z: obj
Z : obj: Type u
obj}, (X: obj
X ⟶ Y: obj
Y) → (Y: obj
Y ⟶ Z: obj
Z) → (X: obj
X ⟶ Z: obj
Z)
#align category_theory.category_struct CategoryTheory.CategoryStruct: Type u → Type (maxu(v+1))
CategoryTheory.CategoryStruct

initialize_simps_projections CategoryStruct: Type u → Type (maxu(v+1))
CategoryStruct (-toQuiver_Hom: (obj : Type u) → CategoryStruct obj → obj → obj → Type v
toQuiver_Hom)

/-- Notation for the identity morphism in a category. -/
notation "𝟙" => CategoryStruct.id: {obj : Type u} → [self : CategoryStruct obj] → (X : obj) → X ⟶ X
CategoryStruct.id  -- type as \b1

/-- Notation for composition of morphisms in a category. -/
infixr:80 " ≫ " => CategoryStruct.comp: {obj : Type u} → [self : CategoryStruct obj] → {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
CategoryStruct.comp -- type as \gg

/--
A thin wrapper for `aesop` which adds the `CategoryTheory` rule set and
allows `aesop` to look through semireducible definitions when calling `intros`.
This tactic fails when it is unable to solve the goal, making it suitable for
use in auto-params.
-/
macro (name := aesop_cat: Lean.ParserDescr
aesop_cat) "aesop_cat" c: ?m.15200
c:Aesop.tactic_clause: Lean.Parser.Category
Aesop.tactic_clause*: tactic: Lean.Parser.Category
tactic =>
`(tactic|
  aesop $c: ?m.15200
c* (options := { introsTransparency? := some .default, terminal := true })
  (rule_sets [$(Lean.mkIdent: Lean.Name → Lean.Ident
Lean.mkIdent `CategoryTheory: Lean.Name
`CategoryTheory):ident]))

/--
A variant of `aesop_cat` which does not fail when it is unable to solve the
goal. Use this only for exploration! Nonterminal `aesop` is even worse than
nonterminal `simp`.
-/
macro (name := aesop_cat_nonterminal: Lean.ParserDescr
aesop_cat_nonterminal) "aesop_cat_nonterminal" c: ?m.19116
c:Aesop.tactic_clause: Lean.Parser.Category
Aesop.tactic_clause*: tactic: Lean.Parser.Category
tactic =>
  `(tactic|
    aesop $c: ?m.19116
c* (options := { introsTransparency? := some .default, warnOnNonterminal := false })
    (rule_sets [$(Lean.mkIdent: Lean.Name → Lean.Ident
Lean.mkIdent `CategoryTheory: Lean.Name
`CategoryTheory):ident]))


-- We turn on `ext` inside `aesop_cat`.
attribute [aesop safe tactic (rule_sets [CategoryTheory])] Std.Tactic.Ext.extCore': Lean.Elab.Tactic.TacticM Unit
Std.Tactic.Ext.extCore'

-- Porting note:
-- Workaround for issue discussed at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Failure.20of.20TC.20search.20in.20.60simp.60.20with.20.60etaExperiment.60.2E
-- when etaExperiment is on.
attribute [aesop safe (rule_sets [CategoryTheory])] Subsingleton.elim: ∀ {α : Sort u} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim

/-- The typeclass `Category C` describes morphisms associated to objects of type `C`.
The universe levels of the objects and morphisms are unconstrained, and will often need to be
specified explicitly, as `Category.{v} C`. (See also `LargeCategory` and `SmallCategory`.)

See .
-/
class Category: {obj : Type u} →
  [toCategoryStruct : CategoryStruct obj] →
    autoParam (∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f) _auto✝ →
      autoParam (∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f) _auto✝¹ →
        autoParam (∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h) _auto✝² →
          Category obj
Category (obj: Type u
obj : Type u: Type (u+1)
Type u) extends CategoryStruct: Type ?u.23087 → Type (max?u.23087(v+1))
CategoryStruct.{v} obj: Type u
obj : Type max u (v + 1): Type ((maxu(v+1))+1)
Type max u (v + 1) where
  /-- Identity morphisms are left identities for composition. -/
  id_comp: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
id_comp : ∀ {X: obj
X Y: obj
Y : obj: Type u
obj} (f: X ⟶ Y
f : X: obj
X ⟶ Y: obj
Y), 𝟙: (X : ?m.23136) → X ⟶ X
𝟙 X: obj
X ≫ f: X ⟶ Y
f = f: X ⟶ Y
f := by aesop_cat
  /-- Identity morphisms are right identities for composition. -/
  comp_id: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
comp_id : ∀ {X: obj
X Y: obj
Y : obj: Type u
obj} (f: X ⟶ Y
f : X: obj
X ⟶ Y: obj
Y), f: X ⟶ Y
f ≫ 𝟙: (X : ?m.23213) → X ⟶ X
𝟙 Y: obj
Y = f: X ⟶ Y
f := by aesop_cat
  /-- Composition in a category is associative. -/
  assoc: ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
assoc : ∀ {W: obj
W X: obj
X Y: obj
Y Z: obj
Z : obj: Type u
obj} (f: W ⟶ X
f : W: obj
W ⟶ X: obj
X) (g: X ⟶ Y
g : X: obj
X ⟶ Y: obj
Y) (h: Y ⟶ Z
h : Y: obj
Y ⟶ Z: obj
Z), (f: W ⟶ X
f ≫ g: X ⟶ Y
g) ≫ h: Y ⟶ Z
h = f: W ⟶ X
f ≫ g: X ⟶ Y
g ≫ h: Y ⟶ Z
h :=
    by aesop_cat
#align category_theory.category CategoryTheory.Category: Type u → Type (maxu(v+1))
CategoryTheory.Category
#align category_theory.category.assoc CategoryTheory.Category.assoc: ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
CategoryTheory.Category.assoc
#align category_theory.category.comp_id CategoryTheory.Category.comp_id: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
CategoryTheory.Category.comp_id
#align category_theory.category.id_comp CategoryTheory.Category.id_comp: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
CategoryTheory.Category.id_comp

-- Porting note: `restate_axiom` should not be necessary in lean4
-- Hopefully we can just remove the backticks from field names,
-- then delete the invocation of `restate_axiom`.

attribute [simp] Category.id_comp: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
Category.id_comp Category.comp_id: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
Category.comp_id Category.assoc: ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
Category.assoc
attribute [trans] CategoryStruct.comp: {obj : Type u} → [self : CategoryStruct obj] → {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
CategoryStruct.comp

example: ∀ {C : Type u_1} [inst : Category C] {X Y : C} (f : X ⟶ Y), 𝟙 X ≫ f = f
example {C: Type ?u.23458
C} [Category: Type ?u.23458 → Type (max?u.23458(?u.23459+1))
Category C: ?m.23455
C] {X: C
X Y: C
Y : C: ?m.23455
C} (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) : 𝟙: (X : ?m.23509) → X ⟶ X
𝟙 X: C
X ≫ f: X ⟶ Y
f = f: X ⟶ Y
f := by
Goals accomplished! 🐙 C: Type ?u.23458

inst✝: Category C

X, Y: C

f: X ⟶ Y

𝟙 X ≫ f = fsimp
Goals accomplished! 🐙
example: ∀ {C : Type u_1} [inst : Category C] {X Y : C} (f : X ⟶ Y), f ≫ 𝟙 Y = f
example {C: ?m.23630
C} [Category: Type ?u.23633 → Type (max?u.23633(?u.23634+1))
Category C: ?m.23630
C] {X: C
X Y: C
Y : C: ?m.23630
C} (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) : f: X ⟶ Y
f ≫ 𝟙: (X : ?m.23697) → X ⟶ X
𝟙 Y: C
Y = f: X ⟶ Y
f := by
Goals accomplished! 🐙 C: Type ?u.23633

inst✝: Category C

X, Y: C

f: X ⟶ Y

f ≫ 𝟙 Y = fsimp
Goals accomplished! 🐙

/-- A `LargeCategory` has objects in one universe level higher than the universe level of
the morphisms. It is useful for examples such as the category of types, or the category
of groups, etc.
-/
abbrev LargeCategory: Type (u+1) → Type (u+1)
LargeCategory (C: Type (u+1)
C : Type (u + 1): Type (u+2)
Type (u + 1)) : Type (u + 1): Type (u+2)
Type (u + 1) := Category: Type ?u.23810 → Type (max?u.23810(u+1))
Category.{u} C: Type (u+1)
C
#align category_theory.large_category CategoryTheory.LargeCategory: Type (u+1) → Type (u+1)
CategoryTheory.LargeCategory

/-- A `SmallCategory` has objects and morphisms in the same universe level.
-/
abbrev SmallCategory: Type u → Type (u+1)
SmallCategory (C: Type u
C : Type u: Type (u+1)
Type u) : Type (u + 1): Type (u+2)
Type (u + 1) := Category: Type ?u.23818 → Type (max?u.23818(u+1))
Category.{u} C: Type u
C
#align category_theory.small_category CategoryTheory.SmallCategory: Type u → Type (u+1)
CategoryTheory.SmallCategory

section

variable {C: Type u
C : Type u: Type (u+1)
Type u} [Category: Type ?u.47370 → Type (max?u.47370(v+1))
Category.{v} C: Type u
C] {X: C
X Y: C
Y Z: C
Z : C: Type u
C}

initialize_simps_projections Category: Type u → Type (maxu(v+1))
Category (-Hom: (obj : Type u) → Category obj → obj → obj → Type v
Hom)

/-- postcompose an equation between morphisms by another morphism -/
theorem eq_whisker: ∀ {f g : X ⟶ Y}, f = g → ∀ (h : Y ⟶ Z), f ≫ h = g ≫ h
eq_whisker {f: X ⟶ Y
f g: X ⟶ Y
g : X: C
X ⟶ Y: C
Y} (w: f = g
w : f: X ⟶ Y
f = g: X ⟶ Y
g) (h: Y ⟶ Z
h : Y: C
Y ⟶ Z: C
Z) : f: X ⟶ Y
f ≫ h: Y ⟶ Z
h = g: X ⟶ Y
g ≫ h: Y ⟶ Z
h := by
Goals accomplished! 🐙 C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: f = g

h: Y ⟶ Z

f ≫ h = g ≫ hrw [C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: f = g

h: Y ⟶ Z

f ≫ h = g ≫ hw: f = g
wC: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: f = g

h: Y ⟶ Z

g ≫ h = g ≫ h]
Goals accomplished! 🐙
#align category_theory.eq_whisker CategoryTheory.eq_whisker: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f g : X ⟶ Y}, f = g → ∀ (h : Y ⟶ Z), f ≫ h = g ≫ h
CategoryTheory.eq_whisker

/-- precompose an equation between morphisms by another morphism -/
theorem whisker_eq: ∀ (f : X ⟶ Y) {g h : Y ⟶ Z}, g = h → f ≫ g = f ≫ h
whisker_eq (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) {g: Y ⟶ Z
g h: Y ⟶ Z
h : Y: C
Y ⟶ Z: C
Z} (w: g = h
w : g: Y ⟶ Z
g = h: Y ⟶ Z
h) : f: X ⟶ Y
f ≫ g: Y ⟶ Z
g = f: X ⟶ Y
f ≫ h: Y ⟶ Z
h := by
Goals accomplished! 🐙 C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ Y

g, h: Y ⟶ Z

w: g = h

f ≫ g = f ≫ hrw [C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ Y

g, h: Y ⟶ Z

w: g = h

f ≫ g = f ≫ hw: g = h
wC: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ Y

g, h: Y ⟶ Z

w: g = h

f ≫ h = f ≫ h]
Goals accomplished! 🐙
#align category_theory.whisker_eq CategoryTheory.whisker_eq: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) {g h : Y ⟶ Z}, g = h → f ≫ g = f ≫ h
CategoryTheory.whisker_eq

/--
Notation for whiskering an equation by a morphism (on the right).
If `f g : X ⟶ Y` and `w : f = g` and `h : Y ⟶ Z`, then `w =≫ h : f ≫ h = g ≫ h`.
-/
infixr:80 " =≫ " => eq_whisker: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f g : X ⟶ Y}, f = g → ∀ (h : Y ⟶ Z), f ≫ h = g ≫ h
eq_whisker

/--
Notation for whiskering an equation by a morphism (on the left).
If `g h : Y ⟶ Z` and `w : g = h` and `h : X ⟶ Y`, then `f ≫= w : f ≫ g = f ≫ h`.
-/
infixr:80 " ≫= " => whisker_eq: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) {g h : Y ⟶ Z}, g = h → f ≫ g = f ≫ h
whisker_eq

theorem eq_of_comp_left_eq: ∀ {f g : X ⟶ Y}, (∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) → f = g
eq_of_comp_left_eq {f: X ⟶ Y
f g: X ⟶ Y
g : X: C
X ⟶ Y: C
Y} (w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
w : ∀ {Z: C
Z : C: Type u
C} (h: Y ⟶ Z
h : Y: C
Y ⟶ Z: C
Z), f: X ⟶ Y
f ≫ h: Y ⟶ Z
h = g: X ⟶ Y
g ≫ h: Y ⟶ Z
h) :
    f: X ⟶ Y
f = g: X ⟶ Y
g := by
Goals accomplished! 🐙
  C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h

f = gconvert w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
w (𝟙: (X : ?m.39985) → X ⟶ X
𝟙 Y: C
Y)C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h

h.e'_2f = f ≫ 𝟙 Y
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h

h.e'_3g = g ≫ 𝟙 Y C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h

f = g<;>C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h

h.e'_2f = f ≫ 𝟙 Y
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h

h.e'_3g = g ≫ 𝟙 Y
  C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h

f = gaesop
Goals accomplished! 🐙
#align category_theory.eq_of_comp_left_eq CategoryTheory.eq_of_comp_left_eq: ∀ {C : Type u} [inst : Category C] {X Y : C} {f g : X ⟶ Y}, (∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) → f = g
CategoryTheory.eq_of_comp_left_eq

theorem eq_of_comp_right_eq: ∀ {f g : Y ⟶ Z}, (∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) → f = g
eq_of_comp_right_eq {f: Y ⟶ Z
f g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z} (w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
w : ∀ {X: C
X : C: Type u
C} (h: X ⟶ Y
h : X: C
X ⟶ Y: C
Y), h: X ⟶ Y
h ≫ f: Y ⟶ Z
f = h: X ⟶ Y
h ≫ g: Y ⟶ Z
g) :
    f: Y ⟶ Z
f = g: Y ⟶ Z
g := by
Goals accomplished! 🐙
  C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g

f = gconvert w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
w (𝟙: (X : ?m.43766) → X ⟶ X
𝟙 Y: C
Y)C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g

h.e'_2f = 𝟙 Y ≫ f
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g

h.e'_3g = 𝟙 Y ≫ g C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g

f = g<;>C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g

h.e'_2f = 𝟙 Y ≫ f
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g

h.e'_3g = 𝟙 Y ≫ g
  C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g

f = gaesop
Goals accomplished! 🐙
#align category_theory.eq_of_comp_right_eq CategoryTheory.eq_of_comp_right_eq: ∀ {C : Type u} [inst : Category C] {Y Z : C} {f g : Y ⟶ Z}, (∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) → f = g
CategoryTheory.eq_of_comp_right_eq

theorem eq_of_comp_left_eq': ∀ (f g : X ⟶ Y), ((fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h) → f = g
eq_of_comp_left_eq' (f: X ⟶ Y
f g: X ⟶ Y
g : X: C
X ⟶ Y: C
Y)
    (w: (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h
w : (fun {Z: ?m.47446
Z} (h: Y ⟶ Z
h : Y: C
Y ⟶ Z: ?m.47446
Z) => f: X ⟶ Y
f ≫ h: Y ⟶ Z
h) = fun {Z: ?m.47511
Z} (h: Y ⟶ Z
h : Y: C
Y ⟶ Z: ?m.47511
Z) => g: X ⟶ Y
g ≫ h: Y ⟶ Z
h) : f: X ⟶ Y
f = g: X ⟶ Y
g :=
  eq_of_comp_left_eq: ∀ {C : Type ?u.47589} [inst : Category C] {X Y : C} {f g : X ⟶ Y}, (∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) → f = g
eq_of_comp_left_eq @fun Z: ?m.47610
Z h: ?m.47613
h => by
Goals accomplished! 🐙 C: Type u

inst✝: Category C

X, Y, Z✝: C

f, g: X ⟶ Y

w: (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h

Z: C

h: Y ⟶ Z

f ≫ h = g ≫ hconvert congr_fun: ∀ {α : Sort ?u.47625} {β : α → Sort ?u.47624} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_fun (congr_fun: ∀ {α : Sort ?u.47631} {β : α → Sort ?u.47630} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_fun w: (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h
w Z: C
Z) h: Y ⟶ Z
h
Goals accomplished! 🐙
#align category_theory.eq_of_comp_left_eq' CategoryTheory.eq_of_comp_left_eq': ∀ {C : Type u} [inst : Category C] {X Y : C} (f g : X ⟶ Y), ((fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h) → f = g
CategoryTheory.eq_of_comp_left_eq'

theorem eq_of_comp_right_eq': ∀ (f g : Y ⟶ Z), ((fun {X} h => h ≫ f) = fun {X} h => h ≫ g) → f = g
eq_of_comp_right_eq' (f: Y ⟶ Z
f g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z)
    (w: (fun {X} h => h ≫ f) = fun {X} h => h ≫ g
w : (fun {X: ?m.47795
X} (h: X ⟶ Y
h : X: ?m.47795
X ⟶ Y: C
Y) => h: X ⟶ Y
h ≫ f: Y ⟶ Z
f) = fun {X: ?m.47860
X} (h: X ⟶ Y
h : X: ?m.47860
X ⟶ Y: C
Y) => h: X ⟶ Y
h ≫ g: Y ⟶ Z
g) : f: Y ⟶ Z
f = g: Y ⟶ Z
g :=
  eq_of_comp_right_eq: ∀ {C : Type ?u.47938} [inst : Category C] {Y Z : C} {f g : Y ⟶ Z}, (∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) → f = g
eq_of_comp_right_eq @fun X: ?m.47959
X h: ?m.47962
h => by
Goals accomplished! 🐙 C: Type u

inst✝: Category C

X✝, Y, Z: C

f, g: Y ⟶ Z

w: (fun {X} h => h ≫ f) = fun {X} h => h ≫ g

X: C

h: X ⟶ Y

h ≫ f = h ≫ gconvert congr_fun: ∀ {α : Sort ?u.47974} {β : α → Sort ?u.47973} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_fun (congr_fun: ∀ {α : Sort ?u.47980} {β : α → Sort ?u.47979} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_fun w: (fun {X} h => h ≫ f) = fun {X} h => h ≫ g
w X: C
X) h: X ⟶ Y
h
Goals accomplished! 🐙
#align category_theory.eq_of_comp_right_eq' CategoryTheory.eq_of_comp_right_eq': ∀ {C : Type u} [inst : Category C] {Y Z : C} (f g : Y ⟶ Z), ((fun {X} h => h ≫ f) = fun {X} h => h ≫ g) → f = g
CategoryTheory.eq_of_comp_right_eq'

theorem id_of_comp_left_id: ∀ {C : Type u} [inst : Category C] {X : C} (f : X ⟶ X), (∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) → f = 𝟙 X
id_of_comp_left_id (f: X ⟶ X
f : X: C
X ⟶ X: C
X) (w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
w : ∀ {Y: C
Y : C: Type u
C} (g: X ⟶ Y
g : X: C
X ⟶ Y: C
Y), f: X ⟶ X
f ≫ g: X ⟶ Y
g = g: X ⟶ Y
g) : f: X ⟶ X
f = 𝟙: (X : ?m.48183) → X ⟶ X
𝟙 X: C
X := by
Goals accomplished! 🐙
  C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g

f = 𝟙 Xconvert w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
w (𝟙: (X : ?m.48213) → X ⟶ X
𝟙 X: C
X)C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g

h.e'_2f = f ≫ 𝟙 X
  C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g

f = 𝟙 Xaesop
Goals accomplished! 🐙
#align category_theory.id_of_comp_left_id CategoryTheory.id_of_comp_left_id: ∀ {C : Type u} [inst : Category C] {X : C} (f : X ⟶ X), (∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) → f = 𝟙 X
CategoryTheory.id_of_comp_left_id

theorem id_of_comp_right_id: ∀ {C : Type u} [inst : Category C] {X : C} (f : X ⟶ X), (∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) → f = 𝟙 X
id_of_comp_right_id (f: X ⟶ X
f : X: C
X ⟶ X: C
X) (w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
w : ∀ {Y: C
Y : C: Type u
C} (g: Y ⟶ X
g : Y: C
Y ⟶ X: C
X), g: Y ⟶ X
g ≫ f: X ⟶ X
f = g: Y ⟶ X
g) : f: X ⟶ X
f = 𝟙: (X : ?m.50257) → X ⟶ X
𝟙 X: C
X := by
Goals accomplished! 🐙
  C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g

f = 𝟙 Xconvert w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
w (𝟙: (X : ?m.50287) → X ⟶ X
𝟙 X: C
X)C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g

h.e'_2f = 𝟙 X ≫ f
  C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g

f = 𝟙 Xaesop
Goals accomplished! 🐙
#align category_theory.id_of_comp_right_id CategoryTheory.id_of_comp_right_id: ∀ {C : Type u} [inst : Category C] {X : C} (f : X ⟶ X), (∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) → f = 𝟙 X
CategoryTheory.id_of_comp_right_id

theorem comp_ite: ∀ {P : Prop} [inst : Decidable P] {X Y Z : C} (f : X ⟶ Y) (g g' : Y ⟶ Z),
  (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'
comp_ite {P: Prop
P : Prop: Type
Prop} [Decidable: Prop → Type
Decidable P: Prop
P] {X: C
X Y: C
Y Z: C
Z : C: Type u
C} (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) (g: Y ⟶ Z
g g': Y ⟶ Z
g' : Y: C
Y ⟶ Z: C
Z) :
    (f: X ⟶ Y
f ≫ if P: Prop
P then g: Y ⟶ Z
g else g': Y ⟶ Z
g') = if P: Prop
P then f: X ⟶ Y
f ≫ g: Y ⟶ Z
g else f: X ⟶ Y
f ≫ g': Y ⟶ Z
g' := by
Goals accomplished! 🐙 C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝: C

P: Prop

inst✝: Decidable P

X, Y, Z: C

f: X ⟶ Y

g, g': Y ⟶ Z

(f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'aesop
Goals accomplished! 🐙
#align category_theory.comp_ite CategoryTheory.comp_ite: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f : X ⟶ Y) (g g' : Y ⟶ Z),
  (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'
CategoryTheory.comp_ite

theorem ite_comp: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f f' : X ⟶ Y) (g : Y ⟶ Z),
  (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g
ite_comp {P: Prop
P : Prop: Type
Prop} [Decidable: Prop → Type
Decidable P: Prop
P] {X: C
X Y: C
Y Z: C
Z : C: Type u
C} (f: X ⟶ Y
f f': X ⟶ Y
f' : X: C
X ⟶ Y: C
Y) (g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z) :
    (if P: Prop
P then f: X ⟶ Y
f else f': X ⟶ Y
f') ≫ g: Y ⟶ Z
g = if P: Prop
P then f: X ⟶ Y
f ≫ g: Y ⟶ Z
g else f': X ⟶ Y
f' ≫ g: Y ⟶ Z
g := by
Goals accomplished! 🐙 C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝: C

P: Prop

inst✝: Decidable P

X, Y, Z: C

f, f': X ⟶ Y

g: Y ⟶ Z

(if P then f else f') ≫ g = if P then f ≫ g else f' ≫ gaesop
Goals accomplished! 🐙
#align category_theory.ite_comp CategoryTheory.ite_comp: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f f' : X ⟶ Y) (g : Y ⟶ Z),
  (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g
CategoryTheory.ite_comp

theorem comp_dite: ∀ {P : Prop} [inst : Decidable P] {X Y Z : C} (f : X ⟶ Y) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)),
  (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h
comp_dite {P: Prop
P : Prop: Type
Prop} [Decidable: Prop → Type
Decidable P: Prop
P]
    {X: C
X Y: C
Y Z: C
Z : C: Type u
C} (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) (g: P → (Y ⟶ Z)
g : P: Prop
P → (Y: C
Y ⟶ Z: C
Z)) (g': ¬P → (Y ⟶ Z)
g' : ¬P: Prop
P → (Y: C
Y ⟶ Z: C
Z)) :
    (f: X ⟶ Y
f ≫ if h: ?m.55087
h : P: Prop
P then g: P → (Y ⟶ Z)
g h: ?m.55078
h else g': ¬P → (Y ⟶ Z)
g' h: ?m.55087
h) = if h: ?m.55105
h : P: Prop
P then f: X ⟶ Y
f ≫ g: P → (Y ⟶ Z)
g h: ?m.55105
h else f: X ⟶ Y
f ≫ g': ¬P → (Y ⟶ Z)
g' h: ?m.55141
h := by
Goals accomplished! 🐙 C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝: C

P: Prop

inst✝: Decidable P

X, Y, Z: C

f: X ⟶ Y

g: P → (Y ⟶ Z)

g': ¬P → (Y ⟶ Z)

(f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' haesop
Goals accomplished! 🐙
#align category_theory.comp_dite CategoryTheory.comp_dite: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f : X ⟶ Y) (g : P → (Y ⟶ Z))
  (g' : ¬P → (Y ⟶ Z)), (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h
CategoryTheory.comp_dite

theorem dite_comp: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y))
  (g : Y ⟶ Z), (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g
dite_comp {P: Prop
P : Prop: Type
Prop} [Decidable: Prop → Type
Decidable P: Prop
P]
    {X: C
X Y: C
Y Z: C
Z : C: Type u
C} (f: P → (X ⟶ Y)
f : P: Prop
P → (X: C
X ⟶ Y: C
Y)) (f': ¬P → (X ⟶ Y)
f' : ¬P: Prop
P → (X: C
X ⟶ Y: C
Y)) (g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z) :
    (if h: ?m.56863
h : P: Prop
P then f: P → (X ⟶ Y)
f h: ?m.56845
h else f': ¬P → (X ⟶ Y)
f' h: ?m.56863
h) ≫ g: Y ⟶ Z
g = if h: ?m.56921
h : P: Prop
P then f: P → (X ⟶ Y)
f h: ?m.56885
h ≫ g: Y ⟶ Z
g else f': ¬P → (X ⟶ Y)
f' h: ?m.56921
h ≫ g: Y ⟶ Z
g := by
Goals accomplished! 🐙 C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝: C

P: Prop

inst✝: Decidable P

X, Y, Z: C

f: P → (X ⟶ Y)

f': ¬P → (X ⟶ Y)

g: Y ⟶ Z

(if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ gaesop
Goals accomplished! 🐙
#align category_theory.dite_comp CategoryTheory.dite_comp: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y))
  (g : Y ⟶ Z), (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g
CategoryTheory.dite_comp

/-- A morphism `f` is an epimorphism if it can be cancelled when precomposed:
`f ≫ g = f ≫ h` implies `g = h`.

See .
-/
class Epi: ∀ {C : Type u} [inst : Category C] {X Y : C} {f : X ⟶ Y}, (∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h) → Epi f
Epi (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) : Prop: Type
Prop where
  /-- A morphism `f` is an epimorphism if it can be cancelled when precomposed. -/
  left_cancellation: ∀ {C : Type u} [inst : Category C] {X Y : C} {f : X ⟶ Y} [self : Epi f] {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
left_cancellation : ∀ {Z: C
Z : C: Type u
C} (g: Y ⟶ Z
g h: Y ⟶ Z
h : Y: C
Y ⟶ Z: C
Z), f: X ⟶ Y
f ≫ g: Y ⟶ Z
g = f: X ⟶ Y
f ≫ h: Y ⟶ Z
h → g: Y ⟶ Z
g = h: Y ⟶ Z
h
#align category_theory.epi CategoryTheory.Epi: {C : Type u} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
CategoryTheory.Epi

/-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed:
`g ≫ f = h ≫ f` implies `g = h`.

See .
-/
class Mono: {C : Type u} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) : Prop: Type
Prop where
  /-- A morphism `f` is an monomorphism if it can be cancelled when postcomposed. -/
  right_cancellation: ∀ {C : Type u} [inst : Category C] {X Y : C} {f : X ⟶ Y} [self : Mono f] {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
right_cancellation : ∀ {Z: C
Z : C: Type u
C} (g: Z ⟶ X
g h: Z ⟶ X
h : Z: C
Z ⟶ X: C
X), g: Z ⟶ X
g ≫ f: X ⟶ Y
f = h: Z ⟶ X
h ≫ f: X ⟶ Y
f → g: Z ⟶ X
g = h: Z ⟶ X
h
#align category_theory.mono CategoryTheory.Mono: {C : Type u} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
CategoryTheory.Mono

instance: ∀ {C : Type u} [inst : Category C] (X : C), Epi (𝟙 X)
instance (X: C
X : C: Type u
C) : Epi: {C : Type ?u.58872} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi (𝟙: (X : ?m.58882) → X ⟶ X
𝟙 X: C
X) :=
  ⟨fun g: ?m.58943
g h: ?m.58946
h w: ?m.58949
w => by
Goals accomplished! 🐙 C: Type u

inst✝: Category C

X✝, Y, Z, X, Z✝: C

g, h: X ⟶ Z✝

w: 𝟙 X ≫ g = 𝟙 X ≫ h

g = haesop
Goals accomplished! 🐙⟩

instance: ∀ {C : Type u} [inst : Category C] (X : C), Mono (𝟙 X)
instance (X: C
X : C: Type u
C) : Mono: {C : Type ?u.59190} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono (𝟙: (X : ?m.59200) → X ⟶ X
𝟙 X: C
X) :=
  ⟨fun g: ?m.59261
g h: ?m.59264
h w: ?m.59267
w => by
Goals accomplished! 🐙 C: Type u

inst✝: Category C

X✝, Y, Z, X, Z✝: C

g, h: Z✝ ⟶ X

w: g ≫ 𝟙 X = h ≫ 𝟙 X

g = haesop
Goals accomplished! 🐙⟩

theorem cancel_epi: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] {g h : Y ⟶ Z}, f ≫ g = f ≫ h ↔ g = h
cancel_epi (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) [Epi: {C : Type ?u.59542} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi f: X ⟶ Y
f] {g: Y ⟶ Z
g h: Y ⟶ Z
h : Y: C
Y ⟶ Z: C
Z} : f: X ⟶ Y
f ≫ g: Y ⟶ Z
g = f: X ⟶ Y
f ≫ h: Y ⟶ Z
h ↔ g: Y ⟶ Z
g = h: Y ⟶ Z
h :=
  ⟨fun p: ?m.59691
p => Epi.left_cancellation: ∀ {C : Type ?u.59693} [inst : Category C] {X Y : C} {f : X ⟶ Y} [self : Epi f] {Z : C} (g h : Y ⟶ Z),
  f ≫ g = f ≫ h → g = h
Epi.left_cancellation g: Y ⟶ Z
g h: Y ⟶ Z
h p: ?m.59691
p, congr_arg: ∀ {α : Sort ?u.59737} {β : Sort ?u.59736} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg _: ?m.59738 → ?m.59739
_⟩
#align category_theory.cancel_epi CategoryTheory.cancel_epi: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] {g h : Y ⟶ Z}, f ≫ g = f ≫ h ↔ g = h
CategoryTheory.cancel_epi

theorem cancel_mono: ∀ (f : X ⟶ Y) [inst : Mono f] {g h : Z ⟶ X}, g ≫ f = h ≫ f ↔ g = h
cancel_mono (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) [Mono: {C : Type ?u.59803} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono f: X ⟶ Y
f] {g: Z ⟶ X
g h: Z ⟶ X
h : Z: C
Z ⟶ X: C
X} : g: Z ⟶ X
g ≫ f: X ⟶ Y
f = h: Z ⟶ X
h ≫ f: X ⟶ Y
f ↔ g: Z ⟶ X
g = h: Z ⟶ X
h :=
  -- Porting note: in Lean 3 we could just write `congr_arg _` here.
  ⟨fun p: ?m.59952
p => Mono.right_cancellation: ∀ {C : Type ?u.59954} [inst : Category C] {X Y : C} {f : X ⟶ Y} [self : Mono f] {Z : C} (g h : Z ⟶ X),
  g ≫ f = h ≫ f → g = h
Mono.right_cancellation g: Z ⟶ X
g h: Z ⟶ X
h p: ?m.59952
p, congr_arg: ∀ {α : Sort ?u.59998} {β : Sort ?u.59997} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg (fun k: ?m.60004
k => k: ?m.60004
k ≫ f: X ⟶ Y
f)⟩
#align category_theory.cancel_mono CategoryTheory.cancel_mono: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] {g h : Z ⟶ X}, g ≫ f = h ≫ f ↔ g = h
CategoryTheory.cancel_mono

theorem cancel_epi_id: ∀ (f : X ⟶ Y) [inst : Epi f] {h : Y ⟶ Y}, f ≫ h = f ↔ h = 𝟙 Y
cancel_epi_id (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) [Epi: {C : Type ?u.60115} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi f: X ⟶ Y
f] {h: Y ⟶ Y
h : Y: C
Y ⟶ Y: C
Y} : f: X ⟶ Y
f ≫ h: Y ⟶ Y
h = f: X ⟶ Y
f ↔ h: Y ⟶ Y
h = 𝟙: (X : ?m.60200) → X ⟶ X
𝟙 Y: C
Y := by
Goals accomplished! 🐙
  C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Epi f

h: Y ⟶ Y

f ≫ h = f ↔ h = 𝟙 Yconvert cancel_epi: ∀ {C : Type ?u.60228} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] {g h : Y ⟶ Z}, f ≫ g = f ≫ h ↔ g = h
cancel_epi f: X ⟶ Y
fC: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Epi f

h: Y ⟶ Y

h.e'_1.h.e'_3.hf = f ≫ 𝟙 Y
  C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Epi f

h: Y ⟶ Y

f ≫ h = f ↔ h = 𝟙 Ysimp
Goals accomplished! 🐙
#align category_theory.cancel_epi_id CategoryTheory.cancel_epi_id: ∀ {C : Type u} [inst : Category C] {X Y : C} (f : X ⟶ Y) [inst_1 : Epi f] {h : Y ⟶ Y}, f ≫ h = f ↔ h = 𝟙 Y
CategoryTheory.cancel_epi_id

theorem cancel_mono_id: ∀ (f : X ⟶ Y) [inst : Mono f] {g : X ⟶ X}, g ≫ f = f ↔ g = 𝟙 X
cancel_mono_id (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) [Mono: {C : Type ?u.62959} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono f: X ⟶ Y
f] {g: X ⟶ X
g : X: C
X ⟶ X: C
X} : g: X ⟶ X
g ≫ f: X ⟶ Y
f = f: X ⟶ Y
f ↔ g: X ⟶ X
g = 𝟙: (X : ?m.63044) → X ⟶ X
𝟙 X: C
X := by
Goals accomplished! 🐙
  C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Mono f

g: X ⟶ X

g ≫ f = f ↔ g = 𝟙 Xconvert cancel_mono: ∀ {C : Type ?u.63072} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] {g h : Z ⟶ X}, g ≫ f = h ≫ f ↔ g = h
cancel_mono f: X ⟶ Y
fC: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Mono f

g: X ⟶ X

h.e'_1.h.e'_3.hf = 𝟙 X ≫ f
  C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Mono f

g: X ⟶ X

g ≫ f = f ↔ g = 𝟙 Xsimp
Goals accomplished! 🐙
#align category_theory.cancel_mono_id CategoryTheory.cancel_mono_id: ∀ {C : Type u} [inst : Category C] {X Y : C} (f : X ⟶ Y) [inst_1 : Mono f] {g : X ⟶ X}, g ≫ f = f ↔ g = 𝟙 X
CategoryTheory.cancel_mono_id

theorem epi_comp: ∀ {X Y Z : C} (f : X ⟶ Y) [inst : Epi f] (g : Y ⟶ Z) [inst : Epi g], Epi (f ≫ g)
epi_comp {X: C
X Y: C
Y Z: C
Z : C: Type u
C} (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) [Epi: {C : Type ?u.65808} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi f: X ⟶ Y
f] (g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z) [Epi: {C : Type ?u.65858} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi g: Y ⟶ Z
g] : Epi: {C : Type ?u.65876} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi (f: X ⟶ Y
f ≫ g: Y ⟶ Z
g) := by
Goals accomplished! 🐙
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g

Epi (f ≫ g)constructorC: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g

left_cancellation∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), (f ≫ g) ≫ g_1 = (f ≫ g) ≫ h → g_1 = h
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g

Epi (f ≫ g)intro Z: ?C
Z a: ?Y ⟶ Z
a b: ?Y ⟶ Z
b w: ?f ≫ a = ?f ≫ b
wC: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z✝

inst✝: Epi g

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b

left_cancellationa = b
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g

Epi (f ≫ g)apply (cancel_epi: ∀ {C : Type ?u.65970} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] {g h : Y ⟶ Z}, f ≫ g = f ≫ h ↔ g = h
cancel_epi g: Y ⟶ Z✝
g).1: ∀ {a b : Prop}, (a ↔ b) → a → b
1C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z✝

inst✝: Epi g

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b

left_cancellationg ≫ a = g ≫ b
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g

Epi (f ≫ g)apply (cancel_epi: ∀ {C : Type ?u.65998} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] {g h : Y ⟶ Z}, f ≫ g = f ≫ h ↔ g = h
cancel_epi f: X ⟶ Y
f).1: ∀ {a b : Prop}, (a ↔ b) → a → b
1C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z✝

inst✝: Epi g

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b

left_cancellationf ≫ g ≫ a = f ≫ g ≫ b
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g

Epi (f ≫ g)simpa using w: ?f ≫ a = ?f ≫ b
w
Goals accomplished! 🐙
#align category_theory.epi_comp CategoryTheory.epi_comp: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] (g : Y ⟶ Z) [inst_2 : Epi g], Epi (f ≫ g)
CategoryTheory.epi_comp

theorem mono_comp: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] (g : Y ⟶ Z) [inst_2 : Mono g], Mono (f ≫ g)
mono_comp {X: C
X Y: C
Y Z: C
Z : C: Type u
C} (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) [Mono: {C : Type ?u.66258} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono f: X ⟶ Y
f] (g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z) [Mono: {C : Type ?u.66308} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono g: Y ⟶ Z
g] : Mono: {C : Type ?u.66326} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono (f: X ⟶ Y
f ≫ g: Y ⟶ Z
g) := by
Goals accomplished! 🐙
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g

Mono (f ≫ g)constructorC: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g

right_cancellation∀ {Z_1 : C} (g_1 h : Z_1 ⟶ X), g_1 ≫ f ≫ g = h ≫ f ≫ g → g_1 = h
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g

Mono (f ≫ g)intro Z: ?C
Z a: Z ⟶ ?X
a b: Z ⟶ ?X
b w: a ≫ ?f = b ≫ ?f
wC: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z✝

inst✝: Mono g

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g

right_cancellationa = b
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g

Mono (f ≫ g)apply (cancel_mono: ∀ {C : Type ?u.66420} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] {g h : Z ⟶ X}, g ≫ f = h ≫ f ↔ g = h
cancel_mono f: X ⟶ Y
f).1: ∀ {a b : Prop}, (a ↔ b) → a → b
1C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z✝

inst✝: Mono g

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g

right_cancellationa ≫ f = b ≫ f
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g

Mono (f ≫ g)apply (cancel_mono: ∀ {C : Type ?u.66453} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] {g h : Z ⟶ X}, g ≫ f = h ≫ f ↔ g = h
cancel_mono g: Y ⟶ Z✝
g).1: ∀ {a b : Prop}, (a ↔ b) → a → b
1C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z✝

inst✝: Mono g

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g

right_cancellation(a ≫ f) ≫ g = (b ≫ f) ≫ g
  C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g

Mono (f ≫ g)simpa using w: a ≫ ?f = b ≫ ?f
w
Goals accomplished! 🐙
#align category_theory.mono_comp CategoryTheory.mono_comp: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] (g : Y ⟶ Z) [inst_2 : Mono g], Mono (f ≫ g)
CategoryTheory.mono_comp

theorem mono_of_mono: ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : Mono (f ≫ g)], Mono f
mono_of_mono {X: C
X Y: C
Y Z: C
Z : C: Type u
C} (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) (g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z) [Mono: {C : Type ?u.66730} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono (f: X ⟶ Y
f ≫ g: Y ⟶ Z
g)] : Mono: {C : Type ?u.66787} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono f: X ⟶ Y
f := by
Goals accomplished! 🐙
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)

Mono fconstructorC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)

right_cancellation∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)

Mono fintro Z: ?C
Z a: Z ⟶ ?X
a b: Z ⟶ ?X
b w: a ≫ ?f = b ≫ ?f
wC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f = b ≫ f

right_cancellationa = b
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)

Mono freplace w: ?m.66843
w := congr_arg: ∀ {α : Sort ?u.66845} {β : Sort ?u.66844} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg (fun k: ?m.66851
k => k: ?m.66851
k ≫ g: Y ⟶ Z✝
g) w: a ≫ ?f = b ≫ ?f
wC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: (fun k => k ≫ g) (a ≫ f) = (fun k => k ≫ g) (b ≫ f)

right_cancellationa = b
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)

Mono fdsimp at w: ?m.66843
wC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: (a ≫ f) ≫ g = (b ≫ f) ≫ g

right_cancellationa = b
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)

Mono frw [C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: (a ≫ f) ≫ g = (b ≫ f) ≫ g

right_cancellationa = bCategory.assoc: ∀ {obj : Type ?u.66912} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
  (f ≫ g) ≫ h = f ≫ g ≫ h
Category.assoc,C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = (b ≫ f) ≫ g

right_cancellationa = b C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: (a ≫ f) ≫ g = (b ≫ f) ≫ g

right_cancellationa = bCategory.assoc: ∀ {obj : Type ?u.66960} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
  (f ≫ g) ≫ h = f ≫ g ≫ h
Category.assocC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g

right_cancellationa = b]C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g

right_cancellationa = b at w: a ≫ f ≫ g = (b ≫ f) ≫ g
wC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g

right_cancellationa = b
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)

Mono fexact (cancel_mono: ∀ {C : Type ?u.67016} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] {g h : Z ⟶ X}, g ≫ f = h ≫ f ↔ g = h
cancel_mono _: ?m.67020 ⟶ ?m.67021
_).1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 w: a ≫ f ≫ g = b ≫ f ≫ g
w
Goals accomplished! 🐙
#align category_theory.mono_of_mono CategoryTheory.mono_of_mono: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : Mono (f ≫ g)], Mono f
CategoryTheory.mono_of_mono

theorem mono_of_mono_fac: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst_1 : Mono h], f ≫ g = h → Mono f
mono_of_mono_fac {X: C
X Y: C
Y Z: C
Z : C: Type u
C} {f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y} {g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z} {h: X ⟶ Z
h : X: C
X ⟶ Z: C
Z} [Mono: {C : Type ?u.67186} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono h: X ⟶ Z
h]
    (w: f ≫ g = h
w : f: X ⟶ Y
f ≫ g: Y ⟶ Z
g = h: X ⟶ Z
h) : Mono: {C : Type ?u.67239} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono f: X ⟶ Y
f := by
Goals accomplished! 🐙
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

h: X ⟶ Z

inst✝: Mono h

w: f ≫ g = h

Mono fsubst h: X ⟶ Z
hC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)

Mono f
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

h: X ⟶ Z

inst✝: Mono h

w: f ≫ g = h

Mono fexact mono_of_mono: ∀ {C : Type ?u.67279} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : Mono (f ≫ g)], Mono f
mono_of_mono f: X ⟶ Y
f g: Y ⟶ Z
g
Goals accomplished! 🐙
#align category_theory.mono_of_mono_fac CategoryTheory.mono_of_mono_fac: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst_1 : Mono h], f ≫ g = h → Mono f
CategoryTheory.mono_of_mono_fac

theorem epi_of_epi: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : Epi (f ≫ g)], Epi g
epi_of_epi {X: C
X Y: C
Y Z: C
Z : C: Type u
C} (f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y) (g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z) [Epi: {C : Type ?u.67397} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi (f: X ⟶ Y
f ≫ g: Y ⟶ Z
g)] : Epi: {C : Type ?u.67454} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi g: Y ⟶ Z
g := by
Goals accomplished! 🐙
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

Epi gconstructorC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

left_cancellation∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), g ≫ g_1 = g ≫ h → g_1 = h
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

Epi gintro Z: ?C
Z a: ?Y ⟶ Z
a b: ?Y ⟶ Z
b w: ?f ≫ a = ?f ≫ b
wC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: g ≫ a = g ≫ b

left_cancellationa = b
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

Epi greplace w: ?m.67510
w := congr_arg: ∀ {α : Sort ?u.67512} {β : Sort ?u.67511} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg (fun k: ?m.67518
k => f: X ⟶ Y
f ≫ k: ?m.67518
k) w: ?f ≫ a = ?f ≫ b
wC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (fun k => f ≫ k) (g ≫ a) = (fun k => f ≫ k) (g ≫ b)

left_cancellationa = b
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

Epi gdsimp at w: ?m.67510
wC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: f ≫ g ≫ a = f ≫ g ≫ b

left_cancellationa = b
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

Epi grw [C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: f ≫ g ≫ a = f ≫ g ≫ b

left_cancellationa = b← Category.assoc: ∀ {obj : Type ?u.67568} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
  (f ≫ g) ≫ h = f ≫ g ≫ h
Category.assoc,C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = f ≫ g ≫ b

left_cancellationa = b C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: f ≫ g ≫ a = f ≫ g ≫ b

left_cancellationa = b← Category.assoc: ∀ {obj : Type ?u.67614} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
  (f ≫ g) ≫ h = f ≫ g ≫ h
Category.assocC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b

left_cancellationa = b]C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b

left_cancellationa = b at w: f ≫ g ≫ a = f ≫ g ≫ b
wC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b

left_cancellationa = b
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

Epi gexact (cancel_epi: ∀ {C : Type ?u.67668} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] {g h : Y ⟶ Z}, f ≫ g = f ≫ h ↔ g = h
cancel_epi _: ?m.67672 ⟶ ?m.67673
_).1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 w: (f ≫ g) ≫ a = (f ≫ g) ≫ b
w
Goals accomplished! 🐙
#align category_theory.epi_of_epi CategoryTheory.epi_of_epi: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : Epi (f ≫ g)], Epi g
CategoryTheory.epi_of_epi

theorem epi_of_epi_fac: ∀ {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst : Epi h], f ≫ g = h → Epi g
epi_of_epi_fac {X: C
X Y: C
Y Z: C
Z : C: Type u
C} {f: X ⟶ Y
f : X: C
X ⟶ Y: C
Y} {g: Y ⟶ Z
g : Y: C
Y ⟶ Z: C
Z} {h: X ⟶ Z
h : X: C
X ⟶ Z: C
Z} [Epi: {C : Type ?u.67838} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi h: X ⟶ Z
h]
    (w: f ≫ g = h
w : f: X ⟶ Y
f ≫ g: Y ⟶ Z
g = h: X ⟶ Z
h) : Epi: {C : Type ?u.67891} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi g: Y ⟶ Z
g := by
Goals accomplished! 🐙
  C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

h: X ⟶ Z

inst✝: Epi h

w: f ≫ g = h

Epi gsubst h: X ⟶ Z
hC: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

Epi g;C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)

Epi g C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

h: X ⟶ Z

inst✝: Epi h

w: f ≫ g = h

Epi gexact epi_of_epi: ∀ {C : Type ?u.67931} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : Epi (f ≫ g)], Epi g
epi_of_epi f: X ⟶ Y
f g: Y ⟶ Z
g
Goals accomplished! 🐙
#align category_theory.epi_of_epi_fac CategoryTheory.epi_of_epi_fac: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst_1 : Epi h], f ≫ g = h → Epi g
CategoryTheory.epi_of_epi_fac

end

section

variable (C: Type u
C : Type u: Type (u+1)
Type u)

variable [Category: Type ?u.67976 → Type (max?u.67976(v+1))
Category.{v} C: Type u
C]

universe u'

instance uliftCategory: Category (ULift C)
uliftCategory : Category: Type ?u.67979 → Type (max?u.67979(v+1))
Category.{v} (ULift: Type ?u.67980 → Type (max?u.67980u')
ULift.{u'} C: Type u
C) where
  Hom X: ?m.67995
X Y: ?m.67998
Y := X: ?m.67995
X.down: {α : Type ?u.68012} → ULift α → α
down ⟶ Y: ?m.67998
Y.down: {α : Type ?u.68016} → ULift α → α
down
  id X: ?m.68040
X := 𝟙: (X : ?m.68044) → X ⟶ X
𝟙 X: ?m.68040
X.down: {α : Type ?u.68054} → ULift α → α
down
  comp f: ?m.68072
f g: ?m.68075
g := f: ?m.68072
f ≫ g: ?m.68075
g
#align category_theory.ulift_category CategoryTheory.uliftCategory: (C : Type u) → [inst : Category C] → Category (ULift C)
CategoryTheory.uliftCategory

-- We verify that this previous instance can lift small categories to large categories.
example: (D : Type u) → [inst : SmallCategory D] → LargeCategory (ULift D)
example (D: Type u
D : Type u: Type (u+1)
Type u) [SmallCategory: Type ?u.69448 → Type (?u.69448+1)
SmallCategory D: Type u
D] : LargeCategory: Type (?u.69451+1) → Type (?u.69451+1)
LargeCategory (ULift: Type ?u.69452 → Type (max?u.69452(u+1))
ULift.{u + 1} D: Type u
D) := by
Goals accomplished! 🐙 C: Type u

inst✝¹: Category C

D: Type u

inst✝: SmallCategory D

LargeCategory (ULift D)infer_instance
Goals accomplished! 🐙

end

end CategoryTheory

-- Porting note: We hope that this will become less necessary,
-- as in Lean4 `simp` will automatically enter "`dsimp` mode" when needed with dependent arguments.
-- Optimistically, we will eventually remove this library note.
library_note "dsimp, simp"
/-- Many proofs in the category theory library use the `dsimp, simp` pattern,
which typically isn't necessary elsewhere.

One would usually hope that the same effect could be achieved simply with `simp`.

The essential issue is that composition of morphisms involves dependent types.
When you have a chain of morphisms being composed, say `f : X ⟶ Y` and `g : Y ⟶ Z`,
then `simp` can operate successfully on the morphisms
(e.g. if `f` is the identity it can strip that off).

However if we have an equality of objects, say `Y = Y'`,
then `simp` can't operate because it would break the typing of the composition operations.
We rarely have interesting equalities of objects
(because that would be "evil" --- anything interesting should be expressed as an isomorphism
and tracked explicitly),
except of course that we have plenty of definitional equalities of objects.

`dsimp` can apply these safely, even inside a composition.

After `dsimp` has cleared up the object level, `simp` can resume work on the morphism level ---
but without the `dsimp` step, because `simp` looks at expressions syntactically,
the relevant lemmas might not fire.

There's no bound on how many times you potentially could have to switch back and forth,
if the `simp` introduced new objects we again need to `dsimp`.
In practice this does occur, but only rarely, because `simp` tends to shorten chains of compositions
(i.e. not introduce new objects at all).
-/