Lean4
noncomputable instance : Category (Localization W)
where
Hom X Y := Localization.Hom W X Y
id _ := Localization.Hom.mk (ofHom W (𝟙 _))
comp f g := f.comp g
comp_id := by
rintro (X Y : C) f
obtain ⟨z, rfl⟩ := Hom.mk_surjective f
change (Hom.mk z).comp (Hom.mk (ofHom W (𝟙 Y))) = Hom.mk z
rw [Hom.comp_eq, comp_eq z (ofHom W (𝟙 Y)) (ofInv z.s z.hs) (by simp)]
dsimp [comp₀]
simp only [comp_id, id_comp]
id_comp := by
rintro (X Y : C) f
obtain ⟨z, rfl⟩ := Hom.mk_surjective f
change (Hom.mk (ofHom W (𝟙 X))).comp (Hom.mk z) = Hom.mk z
rw [Hom.comp_eq, comp_eq (ofHom W (𝟙 X)) z (ofHom W z.f) (by simp)]
dsimp
simp only [id_comp, comp_id]
assoc := by
rintro (X₁ X₂ X₃ X₄ : C) f₁ f₂ f₃
obtain ⟨z₁, rfl⟩ := Hom.mk_surjective f₁
obtain ⟨z₂, rfl⟩ := Hom.mk_surjective f₂
obtain ⟨z₃, rfl⟩ := Hom.mk_surjective f₃
change ((Hom.mk z₁).comp (Hom.mk z₂)).comp (Hom.mk z₃) = (Hom.mk z₁).comp ((Hom.mk z₂).comp (Hom.mk z₃))
rw [Hom.comp_eq z₁ z₂, Hom.comp_eq z₂ z₃]
obtain ⟨z₁₂, fac₁₂⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs z₂.f)
obtain ⟨z₂₃, fac₂₃⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs z₃.f)
obtain ⟨z', fac⟩ := exists_leftFraction (RightFraction.mk z₁₂.s z₁₂.hs z₂₃.f)
dsimp at fac₁₂ fac₂₃ fac
rw [comp_eq z₁ z₂ z₁₂ fac₁₂, comp_eq z₂ z₃ z₂₃ fac₂₃, comp₀, comp₀, Hom.comp_eq, Hom.comp_eq,
comp_eq _ z₃ (mk z'.f (z₂₃.s ≫ z'.s) (W.comp_mem _ _ z₂₃.hs z'.hs))
(by dsimp; rw [assoc, reassoc_of% fac₂₃, fac]),
comp_eq z₁ _ (mk (z₁₂.f ≫ z'.f) z'.s z'.hs) (by dsimp; rw [assoc, ← reassoc_of% fac₁₂, fac])]
simp
