awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
C D : Cat
obj : (↑C : Type u) → (↑D : Type u)
map : {X Y : (↑C : Type u)} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : (↑C : Type u)), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj_1 : (↑C : Type u) → (↑D : Type u)
map_1 : {X Y : (↑C : Type u)} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y)
map_id_1 : ∀ (X : (↑C : Type u)), map_1 (𝟙 X) = 𝟙 (obj_1 X)
map_comp_1 : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
hyp :
  forget.map
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
          Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) }.toCatHom =
    forget.map { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }.toCatHom
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
      Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) } =
    { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }
have mk : ∀ (map_id_2 : ∀ (X : (↑C : Type u)), map (𝟙 X) = 𝟙 (obj X))
  (map_comp_2 : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g),
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
      Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) } =
    { obj := obj, map := @map, map_id := map_id_2, map_comp := @map_comp_2 }
Tactic: cases hyp
Cleared hypotheses: obj_1, map_1, map_id_1, map_comp_1, hyp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
V W : ReflQuiv
F G : ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
hyp : forgetToQuiv.map F = forgetToQuiv.map G
⊢ F = G
have mk : ∀ (toPrefunctor : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2))
  (map_id : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X))
  (hyp :
    forgetToQuiv.map
        { toPrefunctor := toPrefunctor, map_id := map_id :
          ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
      forgetToQuiv.map G),
  { toPrefunctor := toPrefunctor, map_id := map_id :
      ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    G
Tactic: cases F
Cleared hypotheses: F, hyp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
V W : ReflQuiv
G : ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
toPrefunctor : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
map_id : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X)
hyp :
  forgetToQuiv.map
      { toPrefunctor := toPrefunctor, map_id := map_id :
        ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    forgetToQuiv.map G
⊢ { toPrefunctor := toPrefunctor, map_id := map_id :
      ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    G
have mk : ∀ (toPrefunctor_1 : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2))
  (map_id_1 : ∀ (X : (↑V : Type u_2)), toPrefunctor_1.map (𝟙rq X) = 𝟙rq (toPrefunctor_1.obj X))
  (hyp :
    forgetToQuiv.map
        { toPrefunctor := toPrefunctor, map_id := map_id :
          ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
      forgetToQuiv.map { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }),
  { toPrefunctor := toPrefunctor, map_id := map_id :
      ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }
Tactic: cases G
Cleared hypotheses: G, hyp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
V W : ReflQuiv
toPrefunctor : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
map_id : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X)
toPrefunctor_1 : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
map_id_1 : ∀ (X : (↑V : Type u_2)), toPrefunctor_1.map (𝟙rq X) = 𝟙rq (toPrefunctor_1.obj X)
hyp :
  forgetToQuiv.map
      { toPrefunctor := toPrefunctor, map_id := map_id :
        ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    forgetToQuiv.map { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }
⊢ { toPrefunctor := toPrefunctor, map_id := map_id :
      ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }
have mk : ∀ (map_id_2 : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X)),
  { toPrefunctor := toPrefunctor, map_id := map_id :
      ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    { toPrefunctor := toPrefunctor, map_id := map_id_2 }
Tactic: cases hyp
Cleared hypotheses: toPrefunctor_1, map_id_1, hyp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ { toPrefunctor := e.hom, map_id := h_id : ReflPrefunctor.{u_1, u_1, u, u} (↑(of V) : Type u) (↑(of W) : Type u) } ≫
      { toPrefunctor := e.inv, map_id := ⋯ } =
    𝟙 (of V)
have a : forgetToQuiv.map
    ({ toPrefunctor := e.hom, map_id := h_id : ReflPrefunctor.{u_1, u_1, u, u} (↑(of V) : Type u) (↑(of W) : Type u) } ≫
      { toPrefunctor := e.inv, map_id := sorry }) =
  forgetToQuiv.map (𝟙 (of V))
Tactic: apply forgetToQuiv.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ { toPrefunctor := e.inv, map_id := ⋯ : ReflPrefunctor.{u_1, u_1, u, u} (↑(of W) : Type u) (↑(of V) : Type u) } ≫
      { toPrefunctor := e.hom, map_id := h_id } =
    𝟙 (of W)
have a : forgetToQuiv.map
    ({ toPrefunctor := e.inv, map_id := sorry : ReflPrefunctor.{u_1, u_1, u, u} (↑(of W) : Type u) (↑(of V) : Type u) } ≫
      { toPrefunctor := e.hom, map_id := h_id }) =
  forgetToQuiv.map (𝟙 (of W))
Tactic: apply forgetToQuiv.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
x y : V
e : x ⟶ y
⊢ MorphismProperty.ofHoms (X := fun (e : (x : V) × (y : V) × (x ⟶ y)) ↦
    mk (e.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)))) (Y := fun (e : (x : V) × (y : V) × (x ⟶ y)) ↦
    mk
      (e.snd (β := fun (x : V) ↦ (y : V) × (x ⟶ y)).fst (β := fun (y : V) ↦
        e.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)) ⟶ y)))
    (fun (e : (x : V) × (y : V) × (x ⟶ y)) ↦
      homMk
        (e.snd (β := fun (x : V) ↦ (y : V) × (x ⟶ y)).snd (β := fun (y : V) ↦
          e.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)) ⟶ y)))
    (homMk e)
have rw : ∃ (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: rw [MorphismProperty.ofHoms_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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 : FreeRefl.{u_1, u_2} V
f : x ⟶ y
⊢ motive f
have mk : ∀ (x : V) (f : mk x ⟶ y), motive f
Tactic: induction x using induction with | _ x
Cleared hypotheses: x, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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)
y : FreeRefl.{u_1, u_2} V
x : V
f : mk x ⟶ y
⊢ motive f
have mk : ∀ (y : V) (f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (mk x) (mk y)), motive f
Tactic: induction y using induction with | _ y
Cleared hypotheses: y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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
f : Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (mk x) (mk y)
⊢ motive f
have mk : ∀ (f : x ⟶ y), motive (x := mk x) (Functor.map (quotientFunctor V) f)
Tactic: obtain ⟨f, rfl⟩ := (quotientFunctor _).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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
f : x ⟶ y
⊢ motive (x := mk x) (Functor.map (quotientFunctor V) f)
have mk : motive (x := mk x) (Functor.map (quotientFunctor V) Quiver.Path.nil)
Tactic: induction f with
    | nil => simpa using id x
    | cons _ f h => simpa using comp_homMk _ f h
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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)
⊢ motive (x := FreeRefl.mk x) (Functor.map (quotientFunctor V) f)
have 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))
Tactic: induction f with
    | nil => simpa using id x
    | cons _ f h => simpa using comp_homMk _ f h
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X Y : FreeRefl.{u_1, u_2} V
f : X ⟶ Y
⊢ multiplicativeClosure (morphismPropertyHomMk V) f
have id : ∀ (x : V), multiplicativeClosure (C := FreeRefl.{u_1, u_2} V) (morphismPropertyHomMk V) (homMk (𝟙rq x))
Tactic: induction f using hom_induction with
    | id => exact le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _)
    | comp_homMk _ _ h =>
      exact comp_mem _ _ _ h (le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _))
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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))
⊢ multiplicativeClosure (morphismPropertyHomMk V) f
have 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)
Tactic: induction f using hom_induction with
    | id => exact le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _)
    | comp_homMk _ _ h =>
      exact comp_mem _ _ _ h (le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _))
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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
have rw : morphismPropertyHomMk V ≤ W
Tactic: rw [← multiplicativeClosure_morphismPropertyHomMk,
      MorphismProperty.multiplicativeClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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 ⋯
⊢ (quotientFunctor V ⋙ F).obj = (quotientFunctor V ⋙ G).obj
have h : ∀ (x : Paths V), (quotientFunctor V ⋙ F).obj x = (quotientFunctor V ⋙ G).obj x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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 (α := Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (mk x_1) (mk x_1)) (homMk (𝟙rq x_1)) (homMk default)
have id : Eq.{u_3 + 1} (α := x_1 ⟶ x_1) (𝟙rq x_1) default
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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
⊢ f ≫ homMk g = homMk default
have comp_homMk : ∀ (g : y ⟶ y), f ≫ homMk g = homMk default
Tactic: obtain rfl := Subsingleton.elim y z
Cleared hypotheses: z, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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
⊢ f ≫ homMk g = homMk default
have comp_homMk : f ≫ homMk (𝟙rq y) = homMk default
Tactic: obtain rfl := Subsingleton.elim g (𝟙rq _)
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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
⊢ f = homMk default
have id : ∀ (x : V), Eq (α := Quiver.Hom (V := FreeRefl.{u_2, u_3} V) (mk x) (mk x)) (homMk (𝟙rq x)) (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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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)
⊢ f = homMk default
have 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
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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
⊢ Unique (x ⟶ y)
have obtain : Unique (x ⟶ x)
Tactic: obtain rfl : x = y := by subsingleton
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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 = 𝟙 (of (FreeRefl.{u, v} (↑X : Type u)))
have h : (freeReflMap (𝟙 X)).toCatHom.toFunctor = Hom.toFunctor (𝟙 (of (FreeRefl.{u, v} (↑X : Type u))))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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 = (freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom
have h : (freeReflMap (f ≫ g)).toCatHom.toFunctor = ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
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
⊢ (ReflQuiv.forgetToQuiv ⋙ free).map f ≫ Functor.toCatHom (FreeRefl.quotientFunctor (↑w : Type u_3)) =
    Functor.toCatHom (FreeRefl.quotientFunctor (↑v : Type u_3)) ≫ freeRefl.map f
have 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
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
X' X : ReflQuiv
Y : Cat
x : X' ⟶ X
x_1 : X ⟶ forget.obj Y
⊢ Eq (α := Cat.freeRefl.obj X' ⟶ Y)
    ((Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (Cat.freeRefl.obj X') Y) adj.homEquiv) :
          (a : X' ⟶ forget.obj Y) → Cat.freeRefl.obj X' ⟶ Y)
        (x ≫ x_1) :
      Cat.freeRefl.obj X' ⟶ Y)
    (Cat.freeRefl.map x ≫
        (Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (Cat.freeRefl.obj X) Y) adj.homEquiv) :
            (a : X ⟶ forget.obj Y) → Cat.freeRefl.obj X ⟶ Y)
          x_1 :
      Cat.freeRefl.obj X' ⟶ Y)
have h : Eq (α := (↑(Cat.freeRefl.obj X') : Type u) ⥤ (↑Y : Type u))
  (Cat.Hom.toFunctor
    ((Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (Cat.freeRefl.obj X') Y) adj.homEquiv) :
        (a : X' ⟶ forget.obj Y) → Cat.freeRefl.obj X' ⟶ Y)
      (x ≫ x_1)))
  (Cat.Hom.toFunctor
    (Cat.freeRefl.map x ≫
      (Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (Cat.freeRefl.obj X) Y) adj.homEquiv) :
          (a : X ⟶ forget.obj Y) → Cat.freeRefl.obj X ⟶ Y)
        x_1))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
V : Type u
inst : ReflQuiver V
C : Type u
inst_1 : Category.{max u v, u} C
⊢ Eq (α := (Cat.freeRefl.obj (of V) ⟶ Cat.of C) ≃ (of V ⟶ forget.obj (Cat.of C))) (adj.homEquiv (of V) (Cat.of C))
    (Equiv.trans (Cat.Hom.equivFunctor (Cat.freeRefl.obj (of V)) (Cat.of C)) adj.homEquiv)
have H : ∀ (F : Cat.freeRefl.obj (of V) ⟶ Cat.of C),
  Eq (α := of V ⟶ forget.obj (Cat.of C))
    ((adj.homEquiv (of V) (Cat.of C) : (a : Cat.freeRefl.obj (of V) ⟶ Cat.of C) → of V ⟶ forget.obj (Cat.of C)) F :
      of V ⟶ forget.obj (Cat.of C))
    ((Equiv.trans (Cat.Hom.equivFunctor (Cat.freeRefl.obj (of V)) (Cat.of C)) adj.homEquiv :
          (a : Cat.freeRefl.obj (of V) ⟶ Cat.of C) → of V ⟶ forget.obj (Cat.of C))
        F :
      of V ⟶ forget.obj (Cat.of C))
Tactic: ext F
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
C : Type u
inst : Category.{max u v, u} C
x x_1 : C
f : x ⟶ x_1
⊢ Eq (α :=
    Quiver.Hom (V := (↑(obj (𝟭 Cat) (Cat.of C)) : Type u))
      (obj (Cat.FreeRefl.quotientFunctor C ⋙ Cat.Hom.toFunctor (adj.counit.app (Cat.of C))) x)
      (obj (Cat.FreeRefl.quotientFunctor C ⋙ Cat.Hom.toFunctor (adj.counit.app (Cat.of C))) x_1))
    (map (Cat.FreeRefl.quotientFunctor C ⋙ Cat.Hom.toFunctor (adj.counit.app (Cat.of C))) f.toPath)
    (eqToHom ⋯ ≫ map (pathComposition C) f.toPath ≫ eqToHom ⋯)
have dsimp : map (Cat.Hom.toFunctor (adj.counit.app (Cat.of C))) (map (Cat.FreeRefl.quotientFunctor C) f.toPath) =
  𝟙
      (obj (C := Cat.FreeRefl C) (Cat.Hom.toFunctor (adj.counit.app (Cat.of C)))
        (obj (Cat.FreeRefl.quotientFunctor C) x)) ≫
    composePath f.toPath ≫ 𝟙 x_1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.ReflQuiv (goal)
Goal:
C : Type u
inst : Category.{max u v, u} C
x x_1 : C
f : x ⟶ x_1
⊢ map (Cat.Hom.toFunctor (adj.counit.app (Cat.of C))) (map (Cat.FreeRefl.quotientFunctor C) f.toPath) =
    𝟙
        (obj (C := Cat.FreeRefl C) (Cat.Hom.toFunctor (adj.counit.app (Cat.of C)))
          (obj (Cat.FreeRefl.quotientFunctor C) x)) ≫
      composePath f.toPath ≫ 𝟙 x_1
have simp : map (Cat.Hom.toFunctor (toCatHom (Cat.FreeRefl.lift (𝟭rq C)))) (map (Cat.FreeRefl.quotientFunctor C) f.toPath) = f
Tactic: simp only [adj_counit_app, composePath_toPath, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.RelCat (goal)
Goal:
X Y : RelCat
f g : X ⟶ Y
h : f.rel = g.rel
⊢ f = g
have ofRel : ∀ (rel : SetRel X Y) (h : { rel := rel : X.Hom Y }.rel = g.rel), { rel := rel : X.Hom Y } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.RelCat (goal)
Goal:
X Y : RelCat
g : X ⟶ Y
rel : SetRel X Y
h : { rel := rel : X.Hom Y }.rel = g.rel
⊢ { rel := rel : X.Hom Y } = g
have ofRel : ∀ (rel_1 : SetRel X Y) (h : { rel := rel : X.Hom Y }.rel = { rel := rel_1 }.rel),
  { rel := rel : X.Hom Y } = { rel := rel_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.RelCat (goal)
Goal:
X Y Z : RelCat
X_1 Y_1 : Type u_1
a₁ a₂ : X_1 ⟶ Y_1
h : graphFunctor.map a₁ = graphFunctor.map a₂
⊢ a₁ = a₂
have h₁ : ∀ (x : X_1),
  (ConcreteCategory.hom (FC := TypeCat.Fun) a₁).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂).toFun x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.RelCat (goal)
Goal:
X Y : RelCat
r : X ⟶ Y
⊢ IsIso r ↔ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
have mp : IsIso r → ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.RelCat (goal)
Goal:
X Y : RelCat
r : X ⟶ Y
mp : IsIso r → ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
⊢ IsIso r ↔ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
have mpr : (∃ (f : X ≅ Y), graphFunctor.map f.hom = r) → IsIso r
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.RelCat (hypothesis)
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
⊢ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
have h1 : ∀ (a b : X),
  Membership.mem (γ := SetRel X X) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (r ≫ inv r) (p := r ≫ inv r = 𝟙 X) sorry))
      (a, b) =
    Membership.mem (γ := SetRel X X) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (𝟙 X) (p := r ≫ inv r = 𝟙 X) sorry)) (a, b)
Tactic: have h1 := congr_fun₂ congr((· ~[($h.hom_inv_id).rel] ·))
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.RelCat (hypothesis)
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 :
  ∀ (a b : X),
    Membership.mem (γ := SetRel X X) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (r ≫ inv r) (p := r ≫ inv r = 𝟙 X) ⋯))
        (a, b) =
      Membership.mem (γ := SetRel X X) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (𝟙 X) (p := r ≫ inv r = 𝟙 X) ⋯)) (a, b)
⊢ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
have h2 : ∀ (a b : Y),
  Membership.mem (γ := SetRel Y Y) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (inv r ≫ r) (p := inv r ≫ r = 𝟙 Y) sorry))
      (a, b) =
    Membership.mem (γ := SetRel Y Y) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (𝟙 Y) (p := inv r ≫ r = 𝟙 Y) sorry)) (a, b)
Tactic: have h2 := congr_fun₂ congr((· ~[($h.inv_hom_id).rel] ·))
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.RelCat (hypothesis)
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 :
  ∀ (a b : X),
    Membership.mem (γ := SetRel X X) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (r ≫ inv r) (p := r ≫ inv r = 𝟙 X) ⋯))
        (a, b) =
      Membership.mem (γ := SetRel X X) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (𝟙 X) (p := r ≫ inv r = 𝟙 X) ⋯)) (a, b)
h2 :
  ∀ (a b : Y),
    Membership.mem (γ := SetRel Y Y) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (inv r ≫ r) (p := inv r ≫ r = 𝟙 Y) ⋯))
        (a, b) =
      Membership.mem (γ := SetRel Y Y) (Hom.rel (Mathlib.Tactic.TermCongr.cHole (𝟙 Y) (p := inv r ≫ r = 𝟙 Y) ⋯)) (a, b)
⊢ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
have h1₁ : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
Tactic: simp only [RelCat.Hom.rel_comp_apply₂, RelCat.Hom.rel_id_apply₂, eq_iff_iff] at h1 h2
Cleared hypotheses: h1, h2