-- Mathlib/CategoryTheory/Category/RelCat.lean
theorem rel_iso_iff {X Y : RelCat} (r : X ⟶ Y) :
    IsIso (C := RelCat) r ↔ ∃ f : (Iso (C := Type u) X Y), graphFunctor.map f.hom = r

Proof state:
case h.h.mpr
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ r x y → f x = y

Tactic:
intro hr

Result:
case h.h.mpr
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
hr : r x y
⊢ f x = y

Proof state:
case mpr
X Y : RelCat
r : X ⟶ Y
⊢ (∃ f, graphFunctor.map f.hom = r) → IsIso r

Tactic:
rintro ⟨f, rfl⟩

Result:
case mpr.intro
X Y : RelCat
f : X ≅ Y
⊢ IsIso (graphFunctor.map f.hom)

Proof state:
case mp.intro.intro
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
⊢ IsIso f

Tactic:
use g

Result:
case h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
⊢ f ≫ g = 𝟙 X ∧ g ≫ f = 𝟙 Y

Proof state:
case mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
⊢ ∃ f, graphFunctor.map f.hom = r

Tactic:
have h1 := congr_fun₂ h.hom_inv_id

Result:
case mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (r ≫ inv r) a b = 𝟙 X a b
⊢ ∃ f, graphFunctor.map f.hom = r

Proof state:
case h.h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ graphFunctor.map (asIso f).hom x y ↔ r x y

Tactic:
simp only [asIso_hom, graphFunctor_map]

Result:
case h.h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ f x = y ↔ r x y

Proof state:
case h.h.mpr
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
hr : r x y
⊢ f x = y

Tactic:
specialize h2 (f x) y

Result:
case h.h.mpr
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
hr : r x y
h2 : (∃ y_1, inv r (f x) y_1 ∧ r y_1 y) ↔ f x = y
⊢ f x = y

Proof state:
case h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
⊢ graphFunctor.map (asIso f).hom = r

Tactic:
ext x y

Result:
case h.h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ graphFunctor.map (asIso f).hom x y ↔ r x y

Proof state:
case mp
X Y : RelCat
r : X ⟶ Y
⊢ IsIso r → ∃ f, graphFunctor.map f.hom = r

Tactic:
intro h

Result:
case mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
⊢ ∃ f, graphFunctor.map f.hom = r

Proof state:
case h.h.mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ f x = y → r x y

Tactic:
rintro rfl

Result:
case h.h.mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
⊢ r x (f x)

Proof state:
case h.h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ f x = y ↔ r x y

Tactic:
constructor

Result:
case h.h.mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ f x = y → r x y

case h.h.mpr
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ r x y → f x = y

Proof state:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
⊢ ∃ f, graphFunctor.map f.hom = r

Tactic:
use asIso f

Result:
case h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
hif : IsIso f
⊢ graphFunctor.map (asIso f).hom = r

Proof state:
case h.left.h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
x : X
⊢ (f ≫ g) x = 𝟙 X x

Tactic:
apply (h1 _ _).mp

Result:
case h.left.h
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, r a y ∧ inv r y b) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, inv r a y ∧ r y b) ↔ a = b
f : X → Y
hf : ∀ (x : X), r x (f x) ∧ inv r (f x) x
g : Y → X
hg : ∀ (x : Y), inv r x (g x) ∧ r (g x) x
x : X
⊢ ∃ y, r ((f ≫ g) x) y ∧ inv r y (𝟙 X x)