-- Mathlib/CategoryTheory/Limits/TypesFiltered.lean
theorem rel_equiv : _root_.Equivalence (FilteredColimit.Rel.{v, u} F) where
  refl x := ⟨x.1, 𝟙 x.1, 𝟙 x.1, rfl⟩
  symm := fun ⟨k, f, g, h⟩ => ⟨k, g, f, h.symm⟩
  trans {x y z} := fun ⟨k, f, g, h⟩ ⟨k', f', g', h'⟩ =>
    let ⟨l, fl, gl, _⟩ := IsFilteredOrEmpty.cocone_objs k k'
    let ⟨m, n, hn⟩ := IsFilteredOrEmpty.cocone_maps (g ≫ fl) (f' ≫ gl)
    ⟨m, f ≫ fl ≫ n, g' ≫ gl ≫ n,
      calc
        F.map (f ≫ fl ≫ n) x.2 = F.map (fl ≫ n) (F.map f x.2)

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map ((f' ≫ gl) ≫ n) y.snd = F.map (gl ≫ n) (F.map f' y.snd)

Tactic:
simp

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (gl ≫ n) (F.map f' y.snd) = F.map (gl ≫ n) (F.map g' z.snd)

Tactic:
rw [h']

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (fl ≫ n) (F.map g y.snd) = F.map ((g ≫ fl) ≫ n) y.snd

Tactic:
simp

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (gl ≫ n) (F.map g' z.snd) = F.map (g' ≫ gl ≫ n) z.snd

Tactic:
simp

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map ((g ≫ fl) ≫ n) y.snd = F.map ((f' ≫ gl) ≫ n) y.snd

Tactic:
rw [hn]

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (f ≫ fl ≫ n) x.snd = F.map (fl ≫ n) (F.map f x.snd)

Tactic:
simp

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : F.map f' y.snd = F.map g' z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ F.map (fl ≫ n) (F.map f x.snd) = F.map (fl ≫ n) (F.map g y.snd)

Tactic:
rw [h]

Result:
no goals