-- Mathlib/CategoryTheory/Limits/TypesFiltered.lean
theorem isColimit_eq_iff' {t : Cocone F} (ht : IsColimit t) {i : J} (x y : F.obj i) :
    t.ι.app i x = t.ι.app i y ↔ ∃ (j : _) (f : i ⟶ j), F.map f x = F.map f y

Proof state:
case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ j f, F.map f x = F.map f y) → ∃ k f g, F.map f x = F.map g y

Tactic:
rintro ⟨j, f, h⟩

Result:
case mpr.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
j : J
f : i ⟶ j
h : F.map f x = F.map f y
⊢ ∃ k f g, F.map f x = F.map g y

Proof state:
case mpr.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
j : J
f : i ⟶ j
h : F.map f x = F.map f y
⊢ ∃ k f g, F.map f x = F.map g y

Tactic:
exact ⟨j, f, f, h⟩

Result:
no goals

Proof state:
case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ k f g, F.map f x = F.map g y) → ∃ j f, F.map f x = F.map f y

Tactic:
rintro ⟨k, f, g, h⟩

Result:
case mp.intro.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : F.map f x = F.map g y
⊢ ∃ j f, F.map f x = F.map f y

Proof state:
case mp.intro.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : F.map f x = F.map g y
⊢ F.map (f ≫ IsFiltered.coeqHom f g) x = F.map (f ≫ IsFiltered.coeqHom f g) y

Tactic:
conv_rhs => rw [IsFiltered.coeq_condition]

Result:
case mp.intro.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : F.map f x = F.map g y
⊢ F.map (f ≫ IsFiltered.coeqHom f g) x = F.map (g ≫ IsFiltered.coeqHom f g) y

Proof state:
case mp.intro.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : F.map f x = F.map g y
⊢ F.map (f ≫ IsFiltered.coeqHom f g) x = F.map (g ≫ IsFiltered.coeqHom f g) y

Tactic:
simp only [FunctorToTypes.map_comp_apply, h]

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ k f g, F.map f x = F.map g y) ↔ ∃ j f, F.map f x = F.map f y

Tactic:
constructor

Result:
case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ k f g, F.map f x = F.map g y) → ∃ j f, F.map f x = F.map f y

case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ j f, F.map f x = F.map f y) → ∃ k f g, F.map f x = F.map g y

Proof state:
case mp.intro.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : F.map f x = F.map g y
⊢ ∃ j f, F.map f x = F.map f y

Tactic:
refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩

Result:
case mp.intro.intro.intro
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : F.map f x = F.map g y
⊢ F.map (f ≫ IsFiltered.coeqHom f g) x = F.map (f ≫ IsFiltered.coeqHom f g) y

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ t.ι.app i x = t.ι.app i y ↔ ∃ j f, F.map f x = F.map f y

Tactic:
rw [isColimit_eq_iff _ ht]

Result:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ k f g, F.map f x = F.map g y) ↔ ∃ j f, F.map f x = F.map f y