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

Proof state:
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
⊢ colimitMulAux F x ⟨j₁, y⟩ = colimitMulAux F x y'

Tactic:
obtain ⟨j₂, x⟩ := x

Result:
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
j₂ : J
x : ↑(F.obj j₂)
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ y'

Proof state:
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
j₂ : J
x : ↑(F.obj j₂)
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ y'

Tactic:
obtain ⟨j₃, y'⟩ := y'

Result:
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ ⟨j₃, y'⟩
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩

Proof state:
case mk.mk.mk.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩

Tactic:
obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
  IsFiltered.tulip (IsFiltered.rightToMax j₂ j₁) (IsFiltered.leftToMax j₂ j₁)
    (IsFiltered.leftToMax j₂ j₃) (IsFiltered.rightToMax j₂ j₃) f g

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

Proof state:
case mk.mk.mk.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (F ⋙ forget MonCat).map f ⟨j₁, y⟩.snd = (F ⋙ forget MonCat).map g ⟨j₃, y'⟩.snd
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩

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

Result:
case mk.mk.mk.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩

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
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax 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
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax 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

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

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:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y y' : (j : J) × ↑(F.obj j)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) y y'
⊢ colimitMulAux F x y = colimitMulAux F x y'

Tactic:
obtain ⟨j₁, y⟩ := y

Result:
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
⊢ colimitMulAux F x ⟨j₁, y⟩ = colimitMulAux F x y'