awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
x y : V
e : x ⟶ y
⊢ ∃ (i : (x : V) × (y : V) × (x ⟶ y)),
    Arrow.mk (homMk e) =
      Arrow.mk
        (homMk
          (i.snd (β := fun (x : V) ↦ (y : V) × (x ⟶ y)).snd (β := fun (y : V) ↦
            i.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)) ⟶ y)))

Tactic:
⟨⟨x, y, e⟩, rfl⟩

Premises used: Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
x y : V
e : x ⟶ y
⊢ ∃ (i : (x : V) × (y : V) × (x ⟶ y)),
    Arrow.mk (homMk e) =
      Arrow.mk
        (homMk
          (i.snd (β := fun (x : V) ↦ (y : V) × (x ⟶ y)).snd (β := fun (y : V) ↦
            i.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)) ⟶ y)))

Tactic:
exact ⟨⟨x, y, e⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
motive : {x y : FreeRefl.{u_1, u_2} V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk :
  ∀ {x y z : V} (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (FreeRefl.mk x) (FreeRefl.mk y)) (g : y ⟶ z),
    motive f → motive (f ≫ homMk g)
x y : FreeRefl.{u_1, u_2} V
f : x ⟶ y
mk : ∀ (x : V) (f : FreeRefl.mk x ⟶ y), motive f
⊢ motive f

Tactic:
induction x using induction with | _ x
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
motive : {x y : FreeRefl.{u_1, u_2} V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk :
  ∀ {x y z : V} (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (FreeRefl.mk x) (FreeRefl.mk y)) (g : y ⟶ z),
    motive f → motive (f ≫ homMk g)
y : FreeRefl.{u_1, u_2} V
x : V
f : FreeRefl.mk x ⟶ y
mk : ∀ (y : V) (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (FreeRefl.mk x) (FreeRefl.mk y)), motive f
⊢ motive f

Tactic:
induction y using induction with | _ y
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
motive : {x y : FreeRefl.{u_1, u_2} V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk :
  ∀ {x y z : V} (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (FreeRefl.mk x) (FreeRefl.mk y)) (g : y ⟶ z),
    motive f → motive (f ≫ homMk g)
x y : V
f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (FreeRefl.mk x) (FreeRefl.mk y)
mk : ∀ (f : x ⟶ y), motive (x := FreeRefl.mk x) (Functor.map (quotientFunctor V) f)
⊢ motive f

Tactic:
obtain ⟨f, rfl⟩ := (quotientFunctor _).map_surjective f

Premises used: CategoryTheory.Cat.FreeRefl.quotientFunctor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
motive : {x y : FreeRefl.{u_1, u_2} V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk :
  ∀ {x y z : V} (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (mk x) (mk y)) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : V
⊢ motive (x := mk x) (Functor.map (quotientFunctor V) Quiver.Path.nil)

Tactic:
simpa using id x
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
motive : {x y : FreeRefl.{u_1, u_2} V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk :
  ∀ {x y z : V} (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (mk x) (mk y)) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y b c : V
a : Quiver.Path.{u_2, u_1} x b
f : b ⟶ c
h : motive (x := mk x) (Functor.map (quotientFunctor V) a)
⊢ motive (x := mk x) (Functor.map (quotientFunctor V) (a.cons f))

Tactic:
simpa using comp_homMk _ f h
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
motive : {x y : FreeRefl.{u_1, u_2} V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk :
  ∀ {x y z : V} (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (FreeRefl.mk x) (FreeRefl.mk y)) (g : y ⟶ z),
    motive f → motive (f ≫ homMk g)
x y : V
f : x ⟶ y
mk : motive (x := FreeRefl.mk x) (Functor.map (quotientFunctor V) Quiver.Path.nil)
mk₁ :
  ∀ {b c : V} (a : Quiver.Path.{u_2, u_1} x b) (f : b ⟶ c)
    (h : motive (x := FreeRefl.mk x) (Functor.map (quotientFunctor V) a)),
    motive (x := FreeRefl.mk x) (Functor.map (quotientFunctor V) (a.cons f))
⊢ motive (x := FreeRefl.mk x) (Functor.map (quotientFunctor V) f)

Tactic:
induction f with
    | nil => simpa using id x
    | cons _ f h => simpa using comp_homMk _ f h
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
⊢ LE.le (α := MorphismProperty (FreeRefl.{u_1, u_2} V)) (multiplicativeClosure (morphismPropertyHomMk V)) ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X : FreeRefl.{u_1, u_2} V
_ : ∀ ⦃Y : FreeRefl.{u_1, u_2} V⦄ (f : X ⟶ Y), ⊤ f → multiplicativeClosure (morphismPropertyHomMk V) f
⊢ ∀ ⦃Y : FreeRefl.{u_1, u_2} V⦄ (f : X ⟶ Y), ⊤ f → multiplicativeClosure (morphismPropertyHomMk V) f

Tactic:
_
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X Y : FreeRefl.{u_1, u_2} V
x : V
⊢ multiplicativeClosure (C := FreeRefl.{u_1, u_2} V) (morphismPropertyHomMk V) (homMk (𝟙rq x))

Tactic:
le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _)

Premises used: CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMk, CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X Y : FreeRefl.{u_1, u_2} V
x : V
⊢ multiplicativeClosure (C := FreeRefl.{u_1, u_2} V) (morphismPropertyHomMk V) (homMk (𝟙rq x))

Tactic:
exact le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _)

Premises used: CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMk, CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X Y : FreeRefl.{u_1, u_2} V
x y z : V
f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (mk x) (mk y)
g : y ⟶ z
h : multiplicativeClosure (morphismPropertyHomMk V) f
⊢ multiplicativeClosure (morphismPropertyHomMk V) (f ≫ homMk g)

Tactic:
comp_mem _ _ _ h (le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _))

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMk, CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X Y : FreeRefl.{u_1, u_2} V
x y z : V
f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (mk x) (mk y)
g : y ⟶ z
h : multiplicativeClosure (morphismPropertyHomMk V) f
⊢ multiplicativeClosure (morphismPropertyHomMk V) (f ≫ homMk g)

Tactic:
exact comp_mem _ _ _ h (le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _))

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMk, CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X Y : FreeRefl.{u_1, u_2} V
f : X ⟶ Y
id : ∀ (x : V), multiplicativeClosure (C := FreeRefl.{u_1, u_2} V) (morphismPropertyHomMk V) (homMk (𝟙rq x))
comp_homMk :
  ∀ {x y z : V} (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (mk x) (mk y)) (g : y ⟶ z)
    (h : multiplicativeClosure (morphismPropertyHomMk V) f),
    multiplicativeClosure (morphismPropertyHomMk V) (f ≫ homMk g)
⊢ multiplicativeClosure (morphismPropertyHomMk V) f

Tactic:
induction f using hom_induction with
    | id => exact le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _)
    | comp_homMk _ _ h =>
      exact comp_mem _ _ _ h (le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _))

Premises used: id, CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMk, CategoryTheory.MorphismProperty.le_multiplicativeClosure
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
W : MorphismProperty (FreeRefl.{u_1, u_2} V)
inst_1 : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
⊢ W ≤ ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
W : MorphismProperty (FreeRefl.{u_1, u_2} V)
inst_1 : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
rw : morphismPropertyHomMk V ≤ W
⊢ ⊤ ≤ W

Tactic:
rw [← multiplicativeClosure_morphismPropertyHomMk,
      MorphismProperty.multiplicativeClosure_le_iff]

Premises used: CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk, CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
W : MorphismProperty (FreeRefl.{u_1, u_2} V)
inst_1 : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
X Y : FreeRefl.{u_1, u_2} V
h : (x : V) × (y : V) × (x ⟶ y)
⊢ W
    (homMk
      (h.snd (β := fun (x : V) ↦ (y : V) × (x ⟶ y)).snd (β := fun (y : V) ↦
        h.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)) ⟶ y)))

Tactic:
apply hW
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
F : ReflPrefunctor.{u_3, v_1, u_1, u_2} V D
x Y : Paths V
⊢ (Paths.lift F.toPrefunctor).map (Quiver.Hom.toPath (𝟙rq x)) = (Paths.lift F.toPrefunctor).map Quiver.Path.nil

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
F : ReflPrefunctor.{u_3, v_1, u_1, u_2} V D
v : V
⊢ (lift F).obj (mk v) = F.obj v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
F : ReflPrefunctor.{u_3, v_1, u_1, u_2} V D
v w : V
f : v ⟶ w
⊢ (lift F).map (homMk f) = F.map f

Tactic:
Category.id_comp _

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
obj : V → D
map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w)
map_id : ∀ (v : V), map (𝟙rq v) = 𝟙 (obj v)
v : V
⊢ (lift' obj (fun {v w : V} ↦ map) map_id).obj (mk v) = obj v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
obj : V → D
map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w)
map_id : ∀ (v : V), map (𝟙rq v) = 𝟙 (obj v)
v w : V
f : v ⟶ w
⊢ (lift' obj (fun {v w : V} ↦ map) map_id).map (homMk f) = map f

Tactic:
simp [lift']

Premises used: CategoryTheory.Cat.FreeRefl.lift'
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_2
inst : ReflQuiver.{u_3, u_2} V
D : Type u_4
inst_1 : Category.{v_1, u_4} D
F₁ F₂ : FreeRefl.{u_2, u_3} V ⥤ D
h : quotientFunctor V ⋙ F₁ = quotientFunctor V ⋙ F₂
⊢ F₁ = F₂

Tactic:
Quotient.lift_unique' (C := Cat.free.obj (Quiv.of V)) (FreeReflRel (V := V)) _ _ h

Premises used: CategoryTheory.Paths, CategoryTheory.Quotient.lift_unique', CategoryTheory.Cat.FreeRefl, CategoryTheory.Cat.FreeReflRel
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
F G : FreeRefl.{u_1, u_3} V ⥤ D
h₁ : ∀ (v : V), F.obj (mk v) = G.obj (mk v)
h₂ : ∀ {v w : V} (f : v ⟶ w), F.map (homMk f) = eqToHom ⋯ ≫ G.map (homMk f) ≫ eqToHom ⋯
h : ∀ (x : Paths V), (quotientFunctor V ⋙ F).obj x = (quotientFunctor V ⋙ G).obj x
⊢ (quotientFunctor V ⋙ F).obj = (quotientFunctor V ⋙ G).obj

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
F G : FreeRefl.{u_1, u_3} V ⥤ D
h₁ : ∀ (v : V), F.obj (mk v) = G.obj (mk v)
h₂ : ∀ {v w : V} (f : v ⟶ w), F.map (homMk f) = eqToHom ⋯ ≫ G.map (homMk f) ≫ eqToHom ⋯
x : Paths V
⊢ (quotientFunctor V ⋙ F).obj x = (quotientFunctor V ⋙ G).obj x

Tactic:
apply h₁
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_2
inst : ReflQuiver.{u_3, u_2} V
X : V
⊢ Eq (α :=
    Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (Functor.obj (quotientFunctor V) X) (Functor.obj (quotientFunctor V) X))
    (Functor.map (quotientFunctor V) (Quiver.Hom.toPath (𝟙rq X))) (𝟙 (Functor.obj (quotientFunctor V) X))

Tactic:
Quotient.sound _ .mk

Premises used: CategoryTheory.Cat.FreeReflRel.mk, CategoryTheory.Quotient.sound
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : (x y : V) → Unique (x ⟶ y)
x y : FreeRefl.{u_2, u_3} V
x_1 : V
id : Eq.{u_3 + 1} (α := x_1 ⟶ x_1) (𝟙rq x_1) default
⊢ Eq (α := Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (mk x_1) (mk x_1)) (homMk (𝟙rq x_1)) (homMk default)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : (x y : V) → Unique (x ⟶ y)
x y : FreeRefl.{u_2, u_3} V
x_1 : V
⊢ Eq.{u_3 + 1} (α := x_1 ⟶ x_1) (𝟙rq x_1) default

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : (x y : V) → Unique (x ⟶ y)
x_1 y_1 : FreeRefl.{u_2, u_3} V
x y z : V
f : Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (mk x) (mk y)
g : y ⟶ z
h : f = homMk default
comp_homMk : ∀ (g : y ⟶ y), f ≫ homMk g = homMk default
⊢ f ≫ homMk g = homMk default

Tactic:
obtain rfl := Subsingleton.elim y z

Premises used: Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : (x y : V) → Unique (x ⟶ y)
x_1 y_1 : FreeRefl.{u_2, u_3} V
x y : V
f : Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (mk x) (mk y)
h : f = homMk default
g : y ⟶ y
comp_homMk : f ≫ homMk (𝟙rq y) = homMk default
⊢ f ≫ homMk g = homMk default

Tactic:
obtain rfl := Subsingleton.elim g (𝟙rq _)

Premises used: Subsingleton.elim, rfl, CategoryTheory.ReflQuiver.id
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : (x y : V) → Unique (x ⟶ y)
x_1 y_1 : FreeRefl.{u_2, u_3} V
x y : V
f : Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (mk x) (mk y)
h : f = homMk default
⊢ f ≫ homMk (𝟙rq y) = homMk default

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : (x y : V) → Unique (x ⟶ y)
x y : FreeRefl.{u_2, u_3} V
f : x ⟶ y
id : ∀ (x : V), Eq (α := Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (mk x) (mk x)) (homMk (𝟙rq x)) (homMk default)
comp_homMk :
  ∀ {x y z : V} (f : Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (mk x) (mk y)) (g : y ⟶ z) (h : f = homMk default),
    f ≫ homMk g = homMk default
⊢ f = homMk default

Tactic:
induction f using hom_induction with
    | id => congr; subsingleton
    | @comp_homMk x y z _ g h =>
      obtain rfl := Subsingleton.elim y z
      obtain rfl := Subsingleton.elim g (𝟙rq _)
      simp [h]

Premises used: id, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : ∀ (x y : V), Subsingleton.{u_3 + 1} (x ⟶ y)
x_1 y_1 : FreeRefl.{u_2, u_3} V
x y : V
⊢ x = y

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : ∀ (x y : V), Subsingleton.{u_3 + 1} (x ⟶ y)
x_1 y_1 : FreeRefl.{u_2, u_3} V
x y : V
obtain : Unique (x ⟶ x)
⊢ Unique (x ⟶ y)

Tactic:
obtain rfl : x = y := by subsingleton

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V_1 : Type u_1
inst : ReflQuiver V_1
V : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} V
inst_2 : Unique V
inst_3 : ∀ (x y : V), Subsingleton.{u_3 + 1} (x ⟶ y)
x_1 y : FreeRefl.{u_2, u_3} V
x : V
⊢ Unique (x ⟶ x)

Tactic:
exact (unique_iff_subsingleton_and_nonempty _ |>.mpr ⟨inferInstance, ⟨𝟙rq _⟩⟩).some

Premises used: Iff.mpr, inferInstance, Nonempty.some, Nonempty.intro, unique_iff_subsingleton_and_nonempty, And.intro, CategoryTheory.ReflQuiver.id
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
F : ReflPrefunctor.{u_3, v_1, u_1, u_2} V D
v : V
⊢ (toFreeRefl V ⋙rq (lift F).toReflPrefunctor).obj v = F.obj v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
D : Type u_2
inst_1 : Category.{v_1, u_2} D
F : ReflPrefunctor.{u_3, v_1, u_1, u_2} V D
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (toFreeRefl V ⋙rq (lift F).toReflPrefunctor).map f =
      @Eq.recOn _ _ (fun (x : D) (x_1 : F.obj Y = x) ↦ (toFreeRefl V ⋙rq (lift F).toReflPrefunctor).obj X ⟶ x)
        ((toFreeRefl V ⋙rq (lift F).toReflPrefunctor).obj Y) ⋯
        (@Eq.recOn _ _ (fun (x : D) (x_1 : F.obj X = x) ↦ x ⟶ F.obj Y)
          ((toFreeRefl V ⋙rq (lift F).toReflPrefunctor).obj X) ⋯ (F.map f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
W : Type u_2
inst_1 : ReflQuiver.{u_4, u_2} W
F : ReflPrefunctor.{u_3, u_4, u_1, u_2} V W
v : V
⊢ Eq (α :=
    Quiver.Hom (V := FreeRefl.{u_2, u_4} W) ((fun (v : V) ↦ (FreeRefl.mk (F.obj v) : FreeRefl.{u_2, u_4} W)) v)
      ((fun (v : V) ↦ (FreeRefl.mk (F.obj v) : FreeRefl.{u_2, u_4} W)) v))
    ((fun {v w : V} (f : v ⟶ w) ↦ FreeRefl.homMk (F.map f)) (𝟙rq v))
    (𝟙 ((fun (v : V) ↦ (FreeRefl.mk (F.obj v) : FreeRefl.{u_2, u_4} W)) v))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_4, u_1} V
W : Type u_2
inst_1 : ReflQuiver.{u_3, u_2} W
F : ReflPrefunctor.{u_4, u_3, u_1, u_2} V W
v : V
⊢ (freeReflMap F).obj (FreeRefl.mk v) = FreeRefl.mk (F.obj v)

Tactic:
rfl

Premises used: CategoryTheory.Cat.FreeRefl.mk, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_3, u_1} V
W : Type u_2
inst_1 : ReflQuiver.{u_4, u_2} W
F : ReflPrefunctor.{u_3, u_4, u_1, u_2} V W
v w : V
f : v ⟶ w
⊢ (freeReflMap F).map (FreeRefl.homMk f) = FreeRefl.homMk (F.map f)

Tactic:
rfl

Premises used: CategoryTheory.Cat.FreeRefl.homMk, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, Quiver.Path.comp, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_3
W : Type u_4
inst : ReflQuiver.{v₁, u_3} V
inst_1 : ReflQuiver.{v₂, u_4} W
F : ReflPrefunctor.{v₁, v₂, u_3, u_4} V W
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (a b : V) (e : a ⟶ b),
    (FreeRefl.quotientFunctor V ⋙ freeReflMap F).map e.toPath =
      eqToHom ⋯ ≫ (freeMap F.toPrefunctor ⋙ FreeRefl.quotientFunctor W).map e.toPath ≫ eqToHom ⋯
⊢ ∀ (a b : V) (e : a ⟶ b),
    (FreeRefl.quotientFunctor V ⋙ freeReflMap F).map e.toPath =
      eqToHom ⋯ ≫ (freeMap F.toPrefunctor ⋙ FreeRefl.quotientFunctor W).map e.toPath ≫ eqToHom ⋯

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
h : (freeReflMap (𝟙 X)).toCatHom.toFunctor = Hom.toFunctor (𝟙 (of (FreeRefl.{u, v} (↑X : Type u))))
⊢ (freeReflMap (𝟙 X)).toCatHom = 𝟙 (of (FreeRefl.{u, v} (↑X : Type u)))

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ ∀ (v : (↑X : Type u)),
    (freeReflMap (𝟙 X)).toCatHom.toFunctor.obj (FreeRefl.mk v) =
      (Hom.toFunctor (𝟙 (of (FreeRefl.{u, v} (↑X : Type u))))).obj (FreeRefl.mk v)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ ∀ {v w : (↑X : Type u)} (f : v ⟶ w),
    (freeReflMap (𝟙 X)).toCatHom.toFunctor.map (FreeRefl.homMk f) =
      eqToHom ⋯ ≫ (Hom.toFunctor (𝟙 (of (FreeRefl.{u, v} (↑X : Type u))))).map (FreeRefl.homMk f) ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ (freeReflMap (𝟙 X)).toCatHom.toFunctor = Hom.toFunctor (𝟙 (of (FreeRefl.{u, v} (↑X : Type u))))

Tactic:
exact FreeRefl.functor_ext (by simp) (by simp)

Premises used: CategoryTheory.Cat.FreeRefl.functor_ext
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
h : (freeReflMap (f ≫ g)).toCatHom.toFunctor = ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor
⊢ (freeReflMap (f ≫ g)).toCatHom = (freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (v : (↑X : Type u)),
    (freeReflMap (f ≫ g)).toCatHom.toFunctor.obj (FreeRefl.mk v) =
      ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor.obj (FreeRefl.mk v)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {v w : (↑X : Type u)} (f_1 : v ⟶ w),
    (freeReflMap (f ≫ g)).toCatHom.toFunctor.map (FreeRefl.homMk f_1) =
      eqToHom ⋯ ≫ ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor.map (FreeRefl.homMk f_1) ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ (freeReflMap (f ≫ g)).toCatHom.toFunctor = ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor

Tactic:
exact FreeRefl.functor_ext (by simp) (by simp)

Premises used: CategoryTheory.Cat.FreeRefl.functor_ext
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
h :
  ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ Functor.toCatHom (FreeRefl.quotientFunctor (↑w : Type u_3))).toFunctor =
    (Functor.toCatHom (FreeRefl.quotientFunctor (↑v : Type u_3)) ≫ freeRefl.map f).toFunctor
⊢ (ReflQuiv.forgetToQuiv ⋙ free).map f ≫ Functor.toCatHom (FreeRefl.quotientFunctor (↑w : Type u_3)) =
    Functor.toCatHom (FreeRefl.quotientFunctor (↑v : Type u_3)) ≫ freeRefl.map f

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
W : Type u_2
inst_1 : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ Functor.toCatHom (FreeRefl.quotientFunctor (↑w : Type u_3))).toFunctor.obj =
    (Functor.toCatHom (FreeRefl.quotientFunctor (↑v : Type u_3)) ≫ freeRefl.map f).toFunctor.obj
⊢ ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ Functor.toCatHom (FreeRefl.quotientFunctor (↑w : Type u_3))).toFunctor.obj =
    (Functor.toCatHom (FreeRefl.quotientFunctor (↑v : Type u_3)) ≫ freeRefl.map f).toFunctor.obj

Tactic:
cat_disch