[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ ((f ≫ g) ≫ h).as = (f ≫ g ≫ h).as
[PROOFSTEP]
change (f.as ≫ g.as) ≫ h.as = f.as ≫ (g.as ≫ h.as)
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (f.as ≫ g.as) ≫ h.as = f.as ≫ g.as ≫ h.as
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ 𝟙 a✝ ≫ f = f
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ (𝟙 a✝ ≫ f).as = f.as
[PROOFSTEP]
change 𝟙 _ ≫ _ = _
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ 𝟙 a✝ ≫ f.as = f.as
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ f ≫ 𝟙 b✝ = f
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ (f ≫ 𝟙 b✝).as = f.as
[PROOFSTEP]
change _ ≫ 𝟙 _ = _
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ f.as ≫ 𝟙 b✝ = f.as
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : LocallyDiscrete C} (f : a ⟶ b), 𝟙 a ≫ f = f
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
⊢ 𝟙 a✝ ≫ f✝ = f✝
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
⊢ (𝟙 a✝ ≫ f✝).as = f✝.as
[PROOFSTEP]
apply Category.id_comp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : LocallyDiscrete C} (f : a ⟶ b), f ≫ 𝟙 b = f
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
⊢ f✝ ≫ 𝟙 b✝ = f✝
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
⊢ (f✝ ≫ 𝟙 b✝).as = f✝.as
[PROOFSTEP]
apply Category.comp_id
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c d : LocallyDiscrete C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case as
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ ((f✝ ≫ g✝) ≫ h✝).as = (f✝ ≫ g✝ ≫ h✝).as
[PROOFSTEP]
apply Category.assoc
