-- Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
theorem colimitSMulAux_eq_of_rel (r : R) (x y : Σ j, F.obj j)
    (h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y) :
    colimitSMulAux F r x = colimitSMulAux F r y

Proof state:
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
⊢ ∃ k f g,
    (ConcreteCategory.hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Tactic:
obtain ⟨k, f, g, hfg⟩ := h

Result:
case h.intro.intro.intro
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget (ModuleCat R)).map f x.snd = (F ⋙ forget (ModuleCat R)).map g y.snd
⊢ ∃ k f g,
    (ConcreteCategory.hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Proof state:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
⊢ colimitSMulAux F r x = colimitSMulAux F r y

Tactic:
apply M.mk_eq

Result:
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
⊢ ∃ k f g,
    (ConcreteCategory.hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Proof state:
case h.intro.intro.intro
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget (ModuleCat R)).map f x.snd = (F ⋙ forget (ModuleCat R)).map g y.snd
⊢ ∃ k f g,
    (ConcreteCategory.hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Tactic:
use k, f, g

Result:
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget (ModuleCat R)).map f x.snd = (F ⋙ forget (ModuleCat R)).map g y.snd
⊢ (ConcreteCategory.hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Proof state:
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget (ModuleCat R)).map f x.snd = (F ⋙ forget (ModuleCat R)).map g y.snd
⊢ (ConcreteCategory.hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, forget_map] at hfg

Result:
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd
⊢ (ConcreteCategory.hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Proof state:
case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd
⊢ (ConcreteCategory.hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Tactic:
simp [hfg]

Result:
no goals