instUniqueHomFreeRefl — Mathlib

Lean4
instance (V : Type*) [ReflQuiver V] [Unique V] [∀ (x y : V), Unique (x ⟶ y)] (x y : FreeRefl V) : Unique (x ⟶ y)
    where
  default := (FreeRefl.quotientFunctor V).map ((Paths.of V).map default)
  uniq
    f := by
    letI : Unique (Paths V) := inferInstanceAs (Unique V)
    induction f using Quotient.induction with
    | @h x y f =>
      rw [← FreeRefl.quotientFunctor]
      symm
      induction f using Paths.induction with
      | id =>
        apply Quotient.sound
        obtain rfl : x = y := by subsingleton
        rw [show (Paths.of V).map default = (𝟙rq _).toPath by congr; subsingleton]
        exact .mk
      | @comp x y z f g hrec =>
        obtain rfl : x = z := by subsingleton
        obtain rfl : x = y := by subsingleton
        obtain rfl : g = 𝟙rq _ := by subsingleton
        simp only [Paths.of_obj, ↓hrec, Paths.of_map, Functor.map_comp, FreeRefl.quotientFunctor_map_id,
          Category.comp_id]
Похожие утверждения