-- Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
theorem colimitMulAux_eq_of_rel_left {x x' y : Σ j, F.obj j}
    (hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) x x') :
    colimitMulAux.{v, u} F x y = colimitMulAux.{v, u} F x' y

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map α))
      ⟨IsFiltered.max ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst,
          (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst))) ⟨j₁, x⟩.snd *
            (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst))) ⟨j₂, y⟩.snd⟩.snd =
    (ConcreteCategory.hom (F.map γ))
      ⟨IsFiltered.max ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst,
          (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst))) ⟨j₃, x'⟩.snd *
            (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst))) ⟨j₂, y⟩.snd⟩.snd

Tactic:
simp_rw [MonoidHom.map_mul, ← ConcreteCategory.comp_apply, ← F.map_comp, h₁, h₂, h₃, F.map_comp,
  ConcreteCategory.comp_apply, hfg]

Result:
no goals

Proof state:
case mk.mk.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ ∃ k f g,
    (ConcreteCategory.hom (F.map f))
        ⟨IsFiltered.max ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst,
            (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst))) ⟨j₁, x⟩.snd *
              (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst))) ⟨j₂, y⟩.snd⟩.snd =
      (ConcreteCategory.hom (F.map g))
        ⟨IsFiltered.max ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst,
            (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst))) ⟨j₃, x'⟩.snd *
              (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst))) ⟨j₂, y⟩.snd⟩.snd

Tactic:
use s, α, γ

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map α))
      ⟨IsFiltered.max ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst,
          (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst))) ⟨j₁, x⟩.snd *
            (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst))) ⟨j₂, y⟩.snd⟩.snd =
    (ConcreteCategory.hom (F.map γ))
      ⟨IsFiltered.max ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst,
          (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst))) ⟨j₃, x'⟩.snd *
            (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst))) ⟨j₂, y⟩.snd⟩.snd