awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃ :
  ∀ (a b : (↑(Quiv.of (↑v : Type u_3)) : Type u_3)) (e : a ⟶ b),
    ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ Functor.toCatHom (FreeRefl.quotientFunctor (↑w : Type u_3))).toFunctor.map
        e.toPath =
      eqToHom ⋯ ≫
        (Functor.toCatHom (FreeRefl.quotientFunctor (↑v : Type u_3)) ≫ freeRefl.map f).toFunctor.map e.toPath ≫
          eqToHom ⋯
⊢ ∀ (a b : (↑(Quiv.of (↑v : Type u_3)) : Type u_3)) (e : a ⟶ b),
    ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ Functor.toCatHom (FreeRefl.quotientFunctor (↑w : Type u_3))).toFunctor.map
        e.toPath =
      eqToHom ⋯ ≫
        (Functor.toCatHom (FreeRefl.quotientFunctor (↑v : Type u_3)) ≫ freeRefl.map f).toFunctor.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
v w : ReflQuiv
f : v ⟶ w
⊢ ((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:
exact Paths.ext_functor (V := Quiv.of v) (by cat_disch) (by cat_disch)

Premises used: CategoryTheory.Paths.ext_functor
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
W : Type u_2
inst : ReflQuiver W
inst_1 : ReflQuiver.{u_5, u_1} V
C : Type u_3
D : Type u_4
inst_2 : Category.{v_1, u_3} C
inst_3 : Category.{v_2, u_4} D
F : Cat.FreeRefl.{u_1, u_5} V ⥤ C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (v : V),
    obj (C := Cat.FreeRefl.{u_1, u_5} V)
        (Cat.FreeRefl.lift ((fun (F : Cat.FreeRefl.{u_1, u_5} V ⥤ C) ↦ Cat.toFreeRefl V ⋙rq F.toReflPrefunctor) F))
        (Cat.FreeRefl.mk v) =
      F.obj (Cat.FreeRefl.mk v)
⊢ ∀ (v : V),
    obj (C := Cat.FreeRefl.{u_1, u_5} V)
        (Cat.FreeRefl.lift ((fun (F : Cat.FreeRefl.{u_1, u_5} V ⥤ C) ↦ Cat.toFreeRefl V ⋙rq F.toReflPrefunctor) F))
        (Cat.FreeRefl.mk v) =
      F.obj (Cat.FreeRefl.mk v)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
W : Type u_2
inst : ReflQuiver.{u_6, u_2} W
inst_1 : ReflQuiver.{u_5, u_1} V
C : Type u_3
inst_2 : Category.{v_1, u_3} C
F : ReflPrefunctor.{u_5, u_6, u_1, u_2} V W
G : ReflPrefunctor.{u_6, v_1, u_2, u_3} W C
⊢ ∀ (v : V),
    Eq.{u_3 + 1} (α := C)
      (obj (C := Cat.FreeRefl.{u_1, u_5} V) ((Equiv.symm homEquiv : (a : V ⥤rq C) → Cat.FreeRefl V ⥤ C) (F ⋙rq G))
        (Cat.FreeRefl.mk v))
      (obj (Cat.freeReflMap F ⋙ (Equiv.symm homEquiv : (a : W ⥤rq C) → Cat.FreeRefl W ⥤ C) G) (Cat.FreeRefl.mk v))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
W : Type u_2
inst : ReflQuiver.{u_6, u_2} W
inst_1 : ReflQuiver.{u_5, u_1} V
C : Type u_3
inst_2 : Category.{v_1, u_3} C
F : ReflPrefunctor.{u_5, u_6, u_1, u_2} V W
G : ReflPrefunctor.{u_6, v_1, u_2, u_3} W C
⊢ ∀ {v w : V} (f : v ⟶ w),
    Eq.{v_1 + 1} (α :=
      Quiver.Hom.{v_1, u_3} (V := C)
        (obj (C := Cat.FreeRefl.{u_1, u_5} V) ((Equiv.symm homEquiv : (a : V ⥤rq C) → Cat.FreeRefl V ⥤ C) (F ⋙rq G))
          (Cat.FreeRefl.mk v))
        (obj (C := Cat.FreeRefl.{u_1, u_5} V) ((Equiv.symm homEquiv : (a : V ⥤rq C) → Cat.FreeRefl V ⥤ C) (F ⋙rq G))
          (Cat.FreeRefl.mk w)))
      (map ((Equiv.symm homEquiv : (a : V ⥤rq C) → Cat.FreeRefl V ⥤ C) (F ⋙rq G)) (Cat.FreeRefl.homMk f))
      (CategoryStruct.comp (Y :=
        obj (Cat.freeReflMap F ⋙ (Equiv.symm homEquiv : (a : W ⥤rq C) → Cat.FreeRefl W ⥤ C) G) (Cat.FreeRefl.mk v))
        (eqToHom ⋯)
        (map (Cat.freeReflMap F ⋙ (Equiv.symm homEquiv : (a : W ⥤rq C) → Cat.FreeRefl W ⥤ C) G) (Cat.FreeRefl.homMk f) ≫
          eqToHom ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_5, u_1} V
C : Type u_3
D : Type u_4
inst_1 : Category.{v_1, u_3} C
inst_2 : Category.{v_2, u_4} D
F : Cat.FreeRefl.{u_1, u_5} V ⥤ C
G : Functor.{v_1, v_2, u_3, u_4} C D
⊢ Eq (α := ReflPrefunctor.{u_5, v_2, u_1, u_4} V D)
    ((homEquiv : (a : Cat.FreeRefl V ⥤ D) → V ⥤rq D) (F ⋙ G) : ReflPrefunctor.{u_5, v_2, u_1, u_4} V D)
    ((homEquiv : (a : Cat.FreeRefl V ⥤ C) → V ⥤rq C) F ⋙rq G.toReflPrefunctor : ReflPrefunctor.{u_5, v_2, u_1, u_4} V D)

Tactic:
rfl

Premises used: CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.ReflPrefunctor.comp, Prefunctor.comp, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
X' X : ReflQuiv
Y : Cat
x : X' ⟶ X
x_1 : X ⟶ forget.obj Y
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))
⊢ 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)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
X' X : ReflQuiv
Y : Cat
x : X' ⟶ X
x_1 : X ⟶ forget.obj Y
⊢ 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:
adj.homEquiv_naturality_left_symm _ _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Cat, CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm, CategoryTheory.Cat.FreeRefl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
X' X : ReflQuiv
Y : Cat
x : X' ⟶ X
x_1 : X ⟶ forget.obj Y
⊢ 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:
exact adj.homEquiv_naturality_left_symm _ _

Premises used: CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver V
⊢ Eq (α := obj (𝟭 ReflQuiv) (of V) ⟶ (Cat.freeRefl ⋙ forget).obj (of V)) (adj.unit.app (of V)) (Cat.toFreeRefl V)

Tactic:
rfl

Premises used: CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.ReflPrefunctor.comp, CategoryTheory.Paths, Prefunctor.comp, CategoryTheory.Cat.toFreeRefl, CategoryTheory.Cat.FreeRefl.homMk, CategoryTheory.Cat.FreeRefl, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
D : Type u
inst : Category.{max u v, u} D
⊢ Eq (α := (forget ⋙ Cat.freeRefl).obj (Cat.of D) ⟶ obj (𝟭 Cat) (Cat.of D)) (adj.counit.app (Cat.of D))
    (toCatHom (Cat.FreeRefl.lift (𝟭rq D)))

Tactic:
rfl

Premises used: CategoryTheory.Paths, CategoryTheory.Functor.toCatHom, CategoryTheory.Cat.FreeRefl.lift, CategoryTheory.Cat.FreeRefl, CategoryTheory.Quotient.lift, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u
inst : ReflQuiver V
C : Type u
inst_1 : Category.{max u v, u} C
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))
⊢ 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)

Tactic:
ext F
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u
inst : ReflQuiver V
C : Type u
inst_1 : Category.{max u v, u} C
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:
apply Adjunction.homEquiv_unit

Premises used: CategoryTheory.Adjunction.homEquiv_unit
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u
inst : ReflQuiver V
⊢ Eq (α := (↑(obj (𝟭 ReflQuiv) (of V)) : Type u) ⥤q (↑((Cat.freeRefl ⋙ forget).obj (of V)) : Type u))
    (ReflPrefunctor.toPrefunctor (adj.unit.app (of V)))
    (Quiv.adj.unit.app (Quiv.of V) ⋙q toPrefunctor (Cat.FreeRefl.quotientFunctor V))

Tactic:
rfl

Premises used: CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Paths, Prefunctor.comp, CategoryTheory.Cat.FreeRefl.homMk, Quiver.Hom.toPath, CategoryTheory.Cat.FreeRefl, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
C : Type u
inst : Category.{max u v, u} C
x x_1 : C
f : x ⟶ x_1
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
⊢ 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 ⋯)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
C : Type u
inst : Category.{max u v, u} C
x x_1 : C
f : x ⟶ x_1
simp :
  map (Cat.Hom.toFunctor (toCatHom (Cat.FreeRefl.lift (𝟭rq C)))) (map (Cat.FreeRefl.quotientFunctor C) f.toPath) = f
⊢ 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:
simp only [adj_counit_app, composePath_toPath, comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.ReflQuiv.adj_counit_app, CategoryTheory.composePath_toPath, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
C : Type u
inst : Category.{max u v, u} C
x x_1 : C
f : x ⟶ x_1
⊢ map (Cat.Hom.toFunctor (toCatHom (Cat.FreeRefl.lift (𝟭rq C)))) (map (Cat.FreeRefl.quotientFunctor C) f.toPath) = f

Tactic:
apply Cat.FreeRefl.lift_map

Premises used: CategoryTheory.Cat.FreeRefl.lift_map
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
f g : X ⟶ Y
h : f.rel = g.rel
ofRel : ∀ (rel : SetRel X Y) (h : { rel := rel : X.Hom Y }.rel = g.rel), { rel := rel : X.Hom Y } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
g : X ⟶ Y
rel : SetRel X Y
h : { rel := rel : X.Hom Y }.rel = g.rel
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 }
⊢ { rel := rel : X.Hom Y } = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
rel 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:
congr
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X : RelCat
⊢ rel (𝟙 X) = SetRel.id

Tactic:
rfl

Premises used: SetRel.id, setOf, rfl
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y Z : RelCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).rel = f.rel ○ g.rel

Tactic:
rfl

Premises used: setOf, SetRel.comp, rfl
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X : RelCat
x y : X
⊢ (x, y) ∈ rel (𝟙 X) ↔ x = y

Tactic:
.rfl

Premises used: SetRel.id, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y Z : RelCat
f : X ⟶ Y
g : Y ⟶ Z
x : X
z : Z
⊢ (x, z) ∈ (f ≫ g).rel ↔ ∃ (y : Y), (x, y) ∈ f.rel ∧ (y, z) ∈ g.rel

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.comp
-- Module: Mathlib.CategoryTheory.Category.RelCat
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₂
h₁ :
  ∀ (x : X_1),
    (ConcreteCategory.hom (FC := TypeCat.Fun) a₁).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂).toFun x
⊢ a₁ = a₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Category.RelCat
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₂
x : X_1
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) a₁).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂).toFun x

Tactic:
simp [Function.graph_injective congr(($h).rel)]

Premises used: congrArg, Function.graph_injective, id, CategoryTheory.RelCat.Hom.rel
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y Z : RelCat
⊢ graphFunctor.EssSurj

Tactic:
graphFunctor.essSurj_of_surj Function.surjective_id

Premises used: CategoryTheory.Functor.essSurj_of_surj, Function.surjective_id
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
mp : IsIso r → ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
mpr : (∃ (f : X ≅ Y), graphFunctor.map f.hom = r) → IsIso r
⊢ IsIso r ↔ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
⊢ ∀ (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)

Tactic:
have h1 := congr_fun₂ congr((· ~[($h.hom_inv_id).rel] ·))
-- Module: Mathlib.CategoryTheory.Category.RelCat
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)
⊢ ∀ (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)

Tactic:
have h2 := congr_fun₂ congr((· ~[($h.inv_hom_id).rel] ·))
-- Module: Mathlib.CategoryTheory.Category.RelCat
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)
⊢ ∀ (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

Premises used: CategoryTheory.RelCat.Hom.rel_id_apply₂, CategoryTheory.RelCat.Hom.rel_comp_apply₂, eq_iff_iff
-- Module: Mathlib.CategoryTheory.Category.RelCat
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)
h1₁ : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
⊢ ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b

Tactic:
simp only [RelCat.Hom.rel_comp_apply₂, RelCat.Hom.rel_id_apply₂, eq_iff_iff] at h1 h2

Premises used: CategoryTheory.RelCat.Hom.rel_id_apply₂, CategoryTheory.RelCat.Hom.rel_comp_apply₂, eq_iff_iff
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
mp :
  ∀ (f : (x : X) → Y) (hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel),
    ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
⊢ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r

Tactic:
obtain ⟨f, hf⟩ := Classical.axiomOfChoice (fun a => (h1 a a).mpr rfl)

Premises used: Iff.mpr, Classical.axiomOfChoice, rfl
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
mp :
  ∀ (g : (x : Y) → X) (hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel),
    ∃ (f : X ≅ Y), graphFunctor.map f.hom = r
⊢ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r

Tactic:
obtain ⟨g, hg⟩ := Classical.axiomOfChoice (fun a => (h2 a a).mpr rfl)

Premises used: Iff.mpr, Classical.axiomOfChoice, rfl
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
hif : IsIso (↾f)
h₁ : graphFunctor.map (asIso (↾f)).hom = r
⊢ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r

Tactic:
use asIso (↾f)

Premises used: TypeCat.ofHom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
hif : IsIso (↾f)
h₁ :
  ∀ (x : graphFunctor.obj X) (y : graphFunctor.obj Y), (x, y) ∈ (graphFunctor.map (asIso (↾f)).hom).rel ↔ (x, y) ∈ r.rel
⊢ graphFunctor.map (asIso (↾f)).hom = r

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
hif : IsIso (↾f)
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ (x, y) ∈ (graphFunctor.map (asIso (↾f)).hom).rel → (x, y) ∈ r.rel

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
hif : IsIso (↾f)
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ (x, y) ∈ (graphFunctor.map (asIso (↾f)).hom).rel ↔ (x, y) ∈ r.rel

Tactic:
exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
mp : IsIso (↾f)
⊢ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r

Tactic:
suffices hif : IsIso (C := Type u) (↾f) by
      use asIso (↾f)
      ext ⟨x, y⟩
      exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
h₁ : ↾f ≫ ↾g = 𝟙 X ∧ ↾g ≫ ↾f = 𝟙 Y
⊢ IsIso (↾f)

Tactic:
use ↾g
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
h₁ : ↾f ≫ ↾g = 𝟙 X
h₂ : ↾g ≫ ↾f = 𝟙 Y
⊢ ↾f ≫ ↾g = 𝟙 X ∧ ↾g ≫ ↾f = 𝟙 Y

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
h₁ :
  ∀ (x : X),
    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾f ≫ ↾g)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x
⊢ ↾f ≫ ↾g = 𝟙 X

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
x : X
h₁ :
  ∃ (y : Y),
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾f ≫ ↾g)).toFun x, y) ∈ r.rel ∧
      (y, (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x) ∈ (inv r).rel
⊢ (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾f ≫ ↾g)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x

Tactic:
apply (h1 _ _).mp

Premises used: Iff.mp