-- Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
theorem colimit_mul_mk_eq (x y : Σ j, F.obj j) (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k) :
    M.mk.{v, u} F x * M.mk F y = M.mk F ⟨k, F.map f x.2 * F.map g y.2⟩

Proof state:
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
⊢ M.mk F ⟨j₁, x⟩ * M.mk F ⟨j₂, y⟩ =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩

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

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

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

Tactic:
refine M.mk_eq F _ _ ?_

Result:
case mk.mk.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ ∃ k_1 f_1 g_1,
    (ConcreteCategory.hom (F.map f_1))
        ⟨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_1))
        ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩.snd

Proof state:
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
y : (j : J) × ↑(F.obj j)
k : J
g : y.fst ⟶ k
j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
⊢ M.mk F ⟨j₁, x⟩ * M.mk F y =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) y.snd⟩

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

Result:
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
⊢ M.mk F ⟨j₁, x⟩ * M.mk F ⟨j₂, y⟩ =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
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 β))
      ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩.snd

Tactic:
dsimp

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
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 f)) x * (ConcreteCategory.hom (F.map g)) y)

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
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 f)) x * (ConcreteCategory.hom (F.map g)) y)

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

Result:
no goals

Proof state:
case mk.mk.intro.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ ∃ k_1 f_1 g_1,
    (ConcreteCategory.hom (F.map f_1))
        ⟨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_1))
        ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩.snd

Tactic:
use s, α, β

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
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 β))
      ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩.snd

Proof state:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
⊢ M.mk F x * M.mk F y = M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) x.snd * (ConcreteCategory.hom (F.map g)) y.snd⟩

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

Result:
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
y : (j : J) × ↑(F.obj j)
k : J
g : y.fst ⟶ k
j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
⊢ M.mk F ⟨j₁, x⟩ * M.mk F y =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) y.snd⟩