[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ 1 = M.mk F { fst := j, snd := 1 }
[PROOFSTEP]
apply M.mk_eq
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ∃ k f g, ↑(F.map f) { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.snd = ↑(F.map g) { fst := j, snd := 1 }.snd
[PROOFSTEP]
refine' ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, _⟩
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ↑(F.map (IsFiltered.leftToMax { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.fst j))
      { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.snd =
    ↑(F.map (IsFiltered.rightToMax { fst := Nonempty.some (_ : Nonempty J), snd := 1 }.fst j))
      { fst := j, snd := 1 }.snd
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x x' y : (j : J) × ↑(F.obj j)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) x x'
⊢ colimitMulAux F x y = colimitMulAux F x' y
[PROOFSTEP]
cases' x with j₁ x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x' y : (j : J) × ↑(F.obj j)
j₁ : J
x : ↑(F.obj j₁)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) { fst := j₁, snd := x } x'
⊢ colimitMulAux F { fst := j₁, snd := x } y = colimitMulAux F x' y
[PROOFSTEP]
cases' y with j₂ y
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x' : (j : J) × ↑(F.obj j)
j₁ : J
x : ↑(F.obj j₁)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) { fst := j₁, snd := x } x'
j₂ : J
y : ↑(F.obj j₂)
⊢ colimitMulAux F { fst := j₁, snd := x } { fst := j₂, snd := y } = colimitMulAux F x' { fst := j₂, snd := y }
[PROOFSTEP]
cases' x' with j₃ x'
[GOAL]
case mk.mk.mk
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₃)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) { fst := j₁, snd := x } { fst := j₃, snd := x' }
⊢ colimitMulAux F { fst := j₁, snd := x } { fst := j₂, snd := y } =
    colimitMulAux F { fst := j₃, snd := x' } { fst := j₂, snd := y }
[PROOFSTEP]
obtain ⟨l, f, g, hfg⟩ := hxx'
[GOAL]
case mk.mk.mk.intro.intro.intro
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : (F ⋙ forget MonCat).map f { fst := j₁, snd := x }.snd = (F ⋙ forget MonCat).map g { fst := j₃, snd := x' }.snd
⊢ colimitMulAux F { fst := j₁, snd := x } { fst := j₂, snd := y } =
    colimitMulAux F { fst := j₃, snd := x' } { fst := j₂, snd := y }
[PROOFSTEP]
simp at hfg
[GOAL]
case mk.mk.mk.intro.intro.intro
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(F.map g) x'
⊢ colimitMulAux F { fst := j₁, snd := x } { fst := j₂, snd := y } =
    colimitMulAux F { fst := j₃, snd := x' } { fst := j₂, snd := y }
[PROOFSTEP]
obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
  IsFiltered.tulip (IsFiltered.leftToMax j₁ j₂) (IsFiltered.rightToMax j₁ j₂) (IsFiltered.rightToMax j₃ j₂)
    (IsFiltered.leftToMax j₃ j₂) f g
[GOAL]
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
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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 ≫ β
⊢ colimitMulAux F { fst := j₁, snd := x } { fst := j₂, snd := y } =
    colimitMulAux F { fst := j₃, snd := x' } { fst := j₂, snd := y }
[PROOFSTEP]
apply M.mk_eq
[GOAL]
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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,
    ↑(F.map f)
        { fst := IsFiltered.max { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst,
            snd :=
              ↑(F.map (IsFiltered.leftToMax { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst))
                  { fst := j₁, snd := x }.snd *
                ↑(F.map (IsFiltered.rightToMax { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst))
                  { fst := j₂, snd := y }.snd }.snd =
      ↑(F.map g)
        { fst := IsFiltered.max { fst := j₃, snd := x' }.fst { fst := j₂, snd := y }.fst,
            snd :=
              ↑(F.map (IsFiltered.leftToMax { fst := j₃, snd := x' }.fst { fst := j₂, snd := y }.fst))
                  { fst := j₃, snd := x' }.snd *
                ↑(F.map (IsFiltered.rightToMax { fst := j₃, snd := x' }.fst { fst := j₂, snd := y }.fst))
                  { fst := j₂, snd := y }.snd }.snd
[PROOFSTEP]
use s, α, γ
[GOAL]
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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 ≫ β
⊢ ↑(F.map α)
      { fst := IsFiltered.max { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst,
          snd :=
            ↑(F.map (IsFiltered.leftToMax { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst))
                { fst := j₁, snd := x }.snd *
              ↑(F.map (IsFiltered.rightToMax { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst))
                { fst := j₂, snd := y }.snd }.snd =
    ↑(F.map γ)
      { fst := IsFiltered.max { fst := j₃, snd := x' }.fst { fst := j₂, snd := y }.fst,
          snd :=
            ↑(F.map (IsFiltered.leftToMax { fst := j₃, snd := x' }.fst { fst := j₂, snd := y }.fst))
                { fst := j₃, snd := x' }.snd *
              ↑(F.map (IsFiltered.rightToMax { fst := j₃, snd := x' }.fst { fst := j₂, snd := y }.fst))
                { fst := j₂, snd := y }.snd }.snd
[PROOFSTEP]
dsimp
[GOAL]
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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 ≫ β
⊢ ↑(F.map α) (↑(F.map (IsFiltered.leftToMax j₁ j₂)) x * ↑(F.map (IsFiltered.rightToMax j₁ j₂)) y) =
    ↑(F.map γ) (↑(F.map (IsFiltered.leftToMax j₃ j₂)) x' * ↑(F.map (IsFiltered.rightToMax j₃ j₂)) y)
[PROOFSTEP]
simp_rw [MonoidHom.map_mul]
  -- Porting note : Lean cannot seem to use lemmas from concrete categories directly
[GOAL]
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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 ≫ β
⊢ ↑(F.map α) (↑(F.map (IsFiltered.leftToMax j₁ j₂)) x) * ↑(F.map α) (↑(F.map (IsFiltered.rightToMax j₁ j₂)) y) =
    ↑(F.map γ) (↑(F.map (IsFiltered.leftToMax j₃ j₂)) x') * ↑(F.map γ) (↑(F.map (IsFiltered.rightToMax j₃ j₂)) y)
[PROOFSTEP]
change (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _ = (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _
[GOAL]
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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 ≫ β
⊢ ↑(F.map (IsFiltered.leftToMax j₁ j₂) ≫ F.map α) x * ↑(F.map (IsFiltered.rightToMax j₁ j₂) ≫ F.map α) y =
    ↑(F.map (IsFiltered.leftToMax j₃ j₂) ≫ F.map γ) x' * ↑(F.map (IsFiltered.rightToMax j₃ j₂) ≫ F.map γ) y
[PROOFSTEP]
simp_rw [← F.map_comp, h₁, h₂, h₃, F.map_comp]
[GOAL]
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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 ≫ β
⊢ ↑(F.map f ≫ F.map β) x * ↑(F.map (IsFiltered.rightToMax j₃ j₂) ≫ F.map γ) y =
    ↑(F.map g ≫ F.map β) x' * ↑(F.map (IsFiltered.rightToMax j₃ j₂) ≫ F.map γ) y
[PROOFSTEP]
congr 1
[GOAL]
case h.e_a
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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 ≫ β
⊢ ↑(F.map f ≫ F.map β) x = ↑(F.map g ≫ F.map β) x'
[PROOFSTEP]
change F.map _ (F.map _ _) = F.map _ (F.map _ _)
[GOAL]
case h.e_a
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 : { fst := j₁, snd := x }.fst ⟶ l
g : { fst := j₃, snd := x' }.fst ⟶ l
hfg : ↑(F.map f) x = ↑(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 ≫ β
⊢ ↑(F.map β) (↑(F.map f) x) = ↑(F.map β) (↑(F.map g) x')
[PROOFSTEP]
rw [hfg]
[GOAL]
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'
[PROOFSTEP]
cases' y with j₁ y
[GOAL]
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) { fst := j₁, snd := y } y'
⊢ colimitMulAux F x { fst := j₁, snd := y } = colimitMulAux F x y'
[PROOFSTEP]
cases' x with j₂ x
[GOAL]
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) { fst := j₁, snd := y } y'
j₂ : J
x : ↑(F.obj j₂)
⊢ colimitMulAux F { fst := j₂, snd := x } { fst := j₁, snd := y } = colimitMulAux F { fst := j₂, snd := x } y'
[PROOFSTEP]
cases' y' with j₃ y'
[GOAL]
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) { fst := j₁, snd := y } { fst := j₃, snd := y' }
⊢ colimitMulAux F { fst := j₂, snd := x } { fst := j₁, snd := y } =
    colimitMulAux F { fst := j₂, snd := x } { fst := j₃, snd := y' }
[PROOFSTEP]
obtain ⟨l, f, g, hfg⟩ := hyy'
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : (F ⋙ forget MonCat).map f { fst := j₁, snd := y }.snd = (F ⋙ forget MonCat).map g { fst := j₃, snd := y' }.snd
⊢ colimitMulAux F { fst := j₂, snd := x } { fst := j₁, snd := y } =
    colimitMulAux F { fst := j₂, snd := x } { fst := j₃, snd := y' }
[PROOFSTEP]
simp at hfg
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(F.map g) y'
⊢ colimitMulAux F { fst := j₂, snd := x } { fst := j₁, snd := y } =
    colimitMulAux F { fst := j₂, snd := x } { fst := j₃, snd := y' }
[PROOFSTEP]
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
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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 { fst := j₂, snd := x } { fst := j₁, snd := y } =
    colimitMulAux F { fst := j₂, snd := x } { fst := j₃, snd := y' }
[PROOFSTEP]
apply M.mk_eq
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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,
    ↑(F.map f)
        { fst := IsFiltered.max { fst := j₂, snd := x }.fst { fst := j₁, snd := y }.fst,
            snd :=
              ↑(F.map (IsFiltered.leftToMax { fst := j₂, snd := x }.fst { fst := j₁, snd := y }.fst))
                  { fst := j₂, snd := x }.snd *
                ↑(F.map (IsFiltered.rightToMax { fst := j₂, snd := x }.fst { fst := j₁, snd := y }.fst))
                  { fst := j₁, snd := y }.snd }.snd =
      ↑(F.map g)
        { fst := IsFiltered.max { fst := j₂, snd := x }.fst { fst := j₃, snd := y' }.fst,
            snd :=
              ↑(F.map (IsFiltered.leftToMax { fst := j₂, snd := x }.fst { fst := j₃, snd := y' }.fst))
                  { fst := j₂, snd := x }.snd *
                ↑(F.map (IsFiltered.rightToMax { fst := j₂, snd := x }.fst { fst := j₃, snd := y' }.fst))
                  { fst := j₃, snd := y' }.snd }.snd
[PROOFSTEP]
use s, α, γ
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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 ≫ β
⊢ ↑(F.map α)
      { fst := IsFiltered.max { fst := j₂, snd := x }.fst { fst := j₁, snd := y }.fst,
          snd :=
            ↑(F.map (IsFiltered.leftToMax { fst := j₂, snd := x }.fst { fst := j₁, snd := y }.fst))
                { fst := j₂, snd := x }.snd *
              ↑(F.map (IsFiltered.rightToMax { fst := j₂, snd := x }.fst { fst := j₁, snd := y }.fst))
                { fst := j₁, snd := y }.snd }.snd =
    ↑(F.map γ)
      { fst := IsFiltered.max { fst := j₂, snd := x }.fst { fst := j₃, snd := y' }.fst,
          snd :=
            ↑(F.map (IsFiltered.leftToMax { fst := j₂, snd := x }.fst { fst := j₃, snd := y' }.fst))
                { fst := j₂, snd := x }.snd *
              ↑(F.map (IsFiltered.rightToMax { fst := j₂, snd := x }.fst { fst := j₃, snd := y' }.fst))
                { fst := j₃, snd := y' }.snd }.snd
[PROOFSTEP]
dsimp
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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 ≫ β
⊢ ↑(F.map α) (↑(F.map (IsFiltered.leftToMax j₂ j₁)) x * ↑(F.map (IsFiltered.rightToMax j₂ j₁)) y) =
    ↑(F.map γ) (↑(F.map (IsFiltered.leftToMax j₂ j₃)) x * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) y')
[PROOFSTEP]
simp_rw [MonoidHom.map_mul]
  -- Porting note : Lean cannot seem to use lemmas from concrete categories directly
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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 ≫ β
⊢ ↑(F.map α) (↑(F.map (IsFiltered.leftToMax j₂ j₁)) x) * ↑(F.map α) (↑(F.map (IsFiltered.rightToMax j₂ j₁)) y) =
    ↑(F.map γ) (↑(F.map (IsFiltered.leftToMax j₂ j₃)) x) * ↑(F.map γ) (↑(F.map (IsFiltered.rightToMax j₂ j₃)) y')
[PROOFSTEP]
change (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _ = (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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 ≫ β
⊢ ↑(F.map (IsFiltered.leftToMax j₂ j₁) ≫ F.map α) x * ↑(F.map (IsFiltered.rightToMax j₂ j₁) ≫ F.map α) y =
    ↑(F.map (IsFiltered.leftToMax j₂ j₃) ≫ F.map γ) x * ↑(F.map (IsFiltered.rightToMax j₂ j₃) ≫ F.map γ) y'
[PROOFSTEP]
simp_rw [← F.map_comp, h₁, h₂, h₃, F.map_comp]
[GOAL]
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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 ≫ β
⊢ ↑(F.map (IsFiltered.leftToMax j₂ j₃) ≫ F.map γ) x * ↑(F.map f ≫ F.map β) y =
    ↑(F.map (IsFiltered.leftToMax j₂ j₃) ≫ F.map γ) x * ↑(F.map g ≫ F.map β) y'
[PROOFSTEP]
congr 1
[GOAL]
case h.e_a
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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 ≫ β
⊢ ↑(F.map f ≫ F.map β) y = ↑(F.map g ≫ F.map β) y'
[PROOFSTEP]
change F.map _ (F.map _ _) = F.map _ (F.map _ _)
[GOAL]
case h.e_a
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 : { fst := j₁, snd := y }.fst ⟶ l
g : { fst := j₃, snd := y' }.fst ⟶ l
hfg : ↑(F.map f) y = ↑(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 ≫ β
⊢ ↑(F.map β) (↑(F.map f) y) = ↑(F.map β) (↑(F.map g) y')
[PROOFSTEP]
rw [hfg]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y : M F
⊢ M F
[PROOFSTEP]
refine' Quot.lift₂ (colimitMulAux F) _ _ x y
[GOAL]
case refine'_1
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y : M F
⊢ ∀ (a b₁ b₂ : (j : J) × ↑(F.obj j)),
    Types.Quot.Rel (F ⋙ forget MonCat) b₁ b₂ → colimitMulAux F a b₁ = colimitMulAux F a b₂
[PROOFSTEP]
intro x y y' h
[GOAL]
case refine'_1
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x y y' : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel (F ⋙ forget MonCat) y y'
⊢ colimitMulAux F x y = colimitMulAux F x y'
[PROOFSTEP]
apply colimitMulAux_eq_of_rel_right
[GOAL]
case refine'_1.hyy'
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x y y' : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel (F ⋙ forget MonCat) y y'
⊢ Types.FilteredColimit.Rel (F ⋙ forget MonCat) y y'
[PROOFSTEP]
apply Types.FilteredColimit.rel_of_quot_rel
[GOAL]
case refine'_1.hyy'.a
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x y y' : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel (F ⋙ forget MonCat) y y'
⊢ Types.Quot.Rel (F ⋙ forget MonCat) y y'
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y : M F
⊢ ∀ (a₁ a₂ b : (j : J) × ↑(F.obj j)),
    Types.Quot.Rel (F ⋙ forget MonCat) a₁ a₂ → colimitMulAux F a₁ b = colimitMulAux F a₂ b
[PROOFSTEP]
intro x x' y h
[GOAL]
case refine'_2
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x x' y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel (F ⋙ forget MonCat) x x'
⊢ colimitMulAux F x y = colimitMulAux F x' y
[PROOFSTEP]
apply colimitMulAux_eq_of_rel_left
[GOAL]
case refine'_2.hxx'
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x x' y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel (F ⋙ forget MonCat) x x'
⊢ Types.FilteredColimit.Rel (F ⋙ forget MonCat) x x'
[PROOFSTEP]
apply Types.FilteredColimit.rel_of_quot_rel
[GOAL]
case refine'_2.hxx'.a
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x x' y : (j : J) × ↑(F.obj j)
h : Types.Quot.Rel (F ⋙ forget MonCat) x x'
⊢ Types.Quot.Rel (F ⋙ forget MonCat) x x'
[PROOFSTEP]
exact h
[GOAL]
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 { fst := k, snd := ↑(F.map f) x.snd * ↑(F.map g) y.snd }
[PROOFSTEP]
cases' x with j₁ x
[GOAL]
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 : { fst := j₁, snd := x }.fst ⟶ k
⊢ M.mk F { fst := j₁, snd := x } * M.mk F y =
    M.mk F { fst := k, snd := ↑(F.map f) { fst := j₁, snd := x }.snd * ↑(F.map g) y.snd }
[PROOFSTEP]
cases' y with j₂ y
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : { fst := j₁, snd := x }.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : { fst := j₂, snd := y }.fst ⟶ k
⊢ M.mk F { fst := j₁, snd := x } * M.mk F { fst := j₂, snd := y } =
    M.mk F { fst := k, snd := ↑(F.map f) { fst := j₁, snd := x }.snd * ↑(F.map g) { fst := j₂, snd := y }.snd }
[PROOFSTEP]
obtain ⟨s, α, β, h₁, h₂⟩ := IsFiltered.bowtie (IsFiltered.leftToMax j₁ j₂) f (IsFiltered.rightToMax j₁ j₂) g
[GOAL]
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 : { fst := j₁, snd := x }.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : { fst := j₂, snd := 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 { fst := j₁, snd := x } * M.mk F { fst := j₂, snd := y } =
    M.mk F { fst := k, snd := ↑(F.map f) { fst := j₁, snd := x }.snd * ↑(F.map g) { fst := j₂, snd := y }.snd }
[PROOFSTEP]
apply M.mk_eq
[GOAL]
case mk.mk.intro.intro.intro.intro.h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : { fst := j₁, snd := x }.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : { fst := j₂, snd := 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,
    ↑(F.map f_1)
        { fst := IsFiltered.max { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst,
            snd :=
              ↑(F.map (IsFiltered.leftToMax { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst))
                  { fst := j₁, snd := x }.snd *
                ↑(F.map (IsFiltered.rightToMax { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst))
                  { fst := j₂, snd := y }.snd }.snd =
      ↑(F.map g_1)
        { fst := k, snd := ↑(F.map f) { fst := j₁, snd := x }.snd * ↑(F.map g) { fst := j₂, snd := y }.snd }.snd
[PROOFSTEP]
use s, α, β
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : { fst := j₁, snd := x }.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : { fst := j₂, snd := y }.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ ↑(F.map α)
      { fst := IsFiltered.max { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst,
          snd :=
            ↑(F.map (IsFiltered.leftToMax { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst))
                { fst := j₁, snd := x }.snd *
              ↑(F.map (IsFiltered.rightToMax { fst := j₁, snd := x }.fst { fst := j₂, snd := y }.fst))
                { fst := j₂, snd := y }.snd }.snd =
    ↑(F.map β) { fst := k, snd := ↑(F.map f) { fst := j₁, snd := x }.snd * ↑(F.map g) { fst := j₂, snd := y }.snd }.snd
[PROOFSTEP]
dsimp
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : { fst := j₁, snd := x }.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : { fst := j₂, snd := y }.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ ↑(F.map α) (↑(F.map (IsFiltered.leftToMax j₁ j₂)) x * ↑(F.map (IsFiltered.rightToMax j₁ j₂)) y) =
    ↑(F.map β) (↑(F.map f) x * ↑(F.map g) y)
[PROOFSTEP]
simp_rw [MonoidHom.map_mul]
  -- Porting note : Lean cannot seem to use lemmas from concrete categories directly
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : { fst := j₁, snd := x }.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : { fst := j₂, snd := y }.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ ↑(F.map α) (↑(F.map (IsFiltered.leftToMax j₁ j₂)) x) * ↑(F.map α) (↑(F.map (IsFiltered.rightToMax j₁ j₂)) y) =
    ↑(F.map β) (↑(F.map f) x) * ↑(F.map β) (↑(F.map g) y)
[PROOFSTEP]
change (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _ = (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _
[GOAL]
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : { fst := j₁, snd := x }.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : { fst := j₂, snd := y }.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ ↑(F.map (IsFiltered.leftToMax j₁ j₂) ≫ F.map α) x * ↑(F.map (IsFiltered.rightToMax j₁ j₂) ≫ F.map α) y =
    ↑(F.map f ≫ F.map β) x * ↑(F.map g ≫ F.map β) y
[PROOFSTEP]
simp_rw [← F.map_comp, h₁, h₂]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x : M F
⊢ 1 * x = x
[PROOFSTEP]
refine Quot.inductionOn x ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x : M F
⊢ ∀ (a : (j : J) × (F ⋙ forget MonCat).obj j),
    1 * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a = Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a
[PROOFSTEP]
intro x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x✝ : M F
x : (j : J) × (F ⋙ forget MonCat).obj j
⊢ 1 * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) x = Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) x
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x✝ : M F
j : J
x : (F ⋙ forget MonCat).obj j
⊢ 1 * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := x } =
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := x }
[PROOFSTEP]
rw [colimit_one_eq F j, colimit_mul_mk_eq F ⟨j, 1⟩ ⟨j, x⟩ j (𝟙 j) (𝟙 j), MonoidHom.map_one, one_mul, F.map_id]
  -- Porting note : `id_apply` does not work here, but the two sides are def-eq
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x✝ : M F
j : J
x : (F ⋙ forget MonCat).obj j
⊢ M.mk F { fst := j, snd := ↑(𝟙 (F.obj { fst := j, snd := x }.fst)) { fst := j, snd := x }.snd } =
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := x }
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x : M F
⊢ x * 1 = x
[PROOFSTEP]
refine Quot.inductionOn x ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x : M F
⊢ ∀ (a : (j : J) × (F ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a * 1 = Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a
[PROOFSTEP]
intro x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x✝ : M F
x : (j : J) × (F ⋙ forget MonCat).obj j
⊢ Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) x * 1 = Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) x
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x✝ : M F
j : J
x : (F ⋙ forget MonCat).obj j
⊢ Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := x } * 1 =
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := x }
[PROOFSTEP]
rw [colimit_one_eq F j, colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, 1⟩ j (𝟙 j) (𝟙 j), MonoidHom.map_one, mul_one, F.map_id]
  -- Porting note : `id_apply` does not work here, but the two sides are def-eq
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝¹ : One (M F) := colimitOne F
src✝ : Mul (M F) := colimitMul F
x✝ : M F
j : J
x : (F ⋙ forget MonCat).obj j
⊢ M.mk F { fst := j, snd := ↑(𝟙 (F.obj { fst := j, snd := x }.fst)) { fst := j, snd := x }.snd } =
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := x }
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
x y z : M F
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
refine Quot.induction_on₃ x y z ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
x y z : M F
⊢ ∀ (a b c : (j : J) × (F ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) b *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) c =
      Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a *
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) b * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) c)
[PROOFSTEP]
clear x y z
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
⊢ ∀ (a b c : (j : J) × (F ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) b *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) c =
      Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a *
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) b * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) c)
[PROOFSTEP]
intro x y z
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
x y z : (j : J) × (F ⋙ forget MonCat).obj j
⊢ Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) x * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) y *
      Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) z =
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) x *
      (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) y * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) z)
[PROOFSTEP]
cases' x with j₁ x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
y z : (j : J) × (F ⋙ forget MonCat).obj j
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
⊢ Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) y *
      Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) z =
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) y * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) z)
[PROOFSTEP]
cases' y with j₂ y
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
z : (j : J) × (F ⋙ forget MonCat).obj j
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
j₂ : J
y : (F ⋙ forget MonCat).obj j₂
⊢ Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₂, snd := y } *
      Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) z =
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₂, snd := y } *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) z)
[PROOFSTEP]
cases' z with j₃ z
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
j₂ : J
y : (F ⋙ forget MonCat).obj j₂
j₃ : J
z : (F ⋙ forget MonCat).obj j₃
⊢ Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₂, snd := y } *
      Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₃, snd := z } =
    Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₂, snd := y } *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j₃, snd := z })
[PROOFSTEP]
change M.mk F _ * M.mk F _ * M.mk F _ = M.mk F _ * M.mk F _
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
j₂ : J
y : (F ⋙ forget MonCat).obj j₂
j₃ : J
z : (F ⋙ forget MonCat).obj j₃
⊢ M.mk F { fst := j₁, snd := x } * M.mk F { fst := j₂, snd := y } * M.mk F { fst := j₃, snd := z } =
    M.mk F { fst := j₁, snd := x } *
      M.mk F
        { fst := IsFiltered.max { fst := j₂, snd := y }.fst { fst := j₃, snd := z }.fst,
          snd :=
            ↑(F.map (IsFiltered.leftToMax { fst := j₂, snd := y }.fst { fst := j₃, snd := z }.fst))
                { fst := j₂, snd := y }.snd *
              ↑(F.map (IsFiltered.rightToMax { fst := j₂, snd := y }.fst { fst := j₃, snd := z }.fst))
                { fst := j₃, snd := z }.snd }
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
j₂ : J
y : (F ⋙ forget MonCat).obj j₂
j₃ : J
z : (F ⋙ forget MonCat).obj j₃
⊢ M.mk F { fst := j₁, snd := x } * M.mk F { fst := j₂, snd := y } * M.mk F { fst := j₃, snd := z } =
    M.mk F { fst := j₁, snd := x } *
      M.mk F
        { fst := IsFiltered.max j₂ j₃,
          snd := ↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z }
[PROOFSTEP]
rw [colimit_mul_mk_eq F ⟨j₁, x⟩ ⟨j₂, y⟩ (IsFiltered.max j₁ (IsFiltered.max j₂ j₃))
    (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃)) (IsFiltered.leftToMax j₂ j₃ ≫ IsFiltered.rightToMax _ _),
  colimit_mul_mk_eq F ⟨(IsFiltered.max j₁ (IsFiltered.max j₂ j₃)), _⟩ ⟨j₃, z⟩ (IsFiltered.max j₁ (IsFiltered.max j₂ j₃))
    (𝟙 _) (IsFiltered.rightToMax j₂ j₃ ≫ IsFiltered.rightToMax _ _),
  colimit_mul_mk_eq.{v, u} F ⟨j₁, x⟩ ⟨IsFiltered.max j₂ j₃, _⟩ _ (IsFiltered.leftToMax _ _) (IsFiltered.rightToMax _ _)]
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
j₂ : J
y : (F ⋙ forget MonCat).obj j₂
j₃ : J
z : (F ⋙ forget MonCat).obj j₃
⊢ M.mk F
      { fst := IsFiltered.max j₁ (IsFiltered.max j₂ j₃),
        snd :=
          ↑(F.map
                  (𝟙
                    { fst := IsFiltered.max j₁ (IsFiltered.max j₂ j₃),
                        snd :=
                          ↑(F.map (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃))) { fst := j₁, snd := x }.snd *
                            ↑(F.map (IsFiltered.leftToMax j₂ j₃ ≫ IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃)))
                              { fst := j₂, snd := y }.snd }.fst))
              { fst := IsFiltered.max j₁ (IsFiltered.max j₂ j₃),
                  snd :=
                    ↑(F.map (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃))) { fst := j₁, snd := x }.snd *
                      ↑(F.map (IsFiltered.leftToMax j₂ j₃ ≫ IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃)))
                        { fst := j₂, snd := y }.snd }.snd *
            ↑(F.map (IsFiltered.rightToMax j₂ j₃ ≫ IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃)))
              { fst := j₃, snd := z }.snd } =
    M.mk F
      {
        fst :=
          IsFiltered.max { fst := j₁, snd := x }.fst
            { fst := IsFiltered.max j₂ j₃,
                snd := ↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z }.fst,
        snd :=
          ↑(F.map
                  (IsFiltered.leftToMax { fst := j₁, snd := x }.fst
                    { fst := IsFiltered.max j₂ j₃,
                        snd :=
                          ↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z }.fst))
              { fst := j₁, snd := x }.snd *
            ↑(F.map
                  (IsFiltered.rightToMax { fst := j₁, snd := x }.fst
                    { fst := IsFiltered.max j₂ j₃,
                        snd :=
                          ↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z }.fst))
              { fst := IsFiltered.max j₂ j₃,
                  snd := ↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z }.snd }
[PROOFSTEP]
congr 2
[GOAL]
case mk.mk.mk.e_a.e_snd
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
j₂ : J
y : (F ⋙ forget MonCat).obj j₂
j₃ : J
z : (F ⋙ forget MonCat).obj j₃
⊢ ↑(F.map
            (𝟙
              { fst := IsFiltered.max j₁ (IsFiltered.max j₂ j₃),
                  snd :=
                    ↑(F.map (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃))) { fst := j₁, snd := x }.snd *
                      ↑(F.map (IsFiltered.leftToMax j₂ j₃ ≫ IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃)))
                        { fst := j₂, snd := y }.snd }.fst))
        { fst := IsFiltered.max j₁ (IsFiltered.max j₂ j₃),
            snd :=
              ↑(F.map (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃))) { fst := j₁, snd := x }.snd *
                ↑(F.map (IsFiltered.leftToMax j₂ j₃ ≫ IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃)))
                  { fst := j₂, snd := y }.snd }.snd *
      ↑(F.map (IsFiltered.rightToMax j₂ j₃ ≫ IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃)))
        { fst := j₃, snd := z }.snd =
    ↑(F.map
            (IsFiltered.leftToMax { fst := j₁, snd := x }.fst
              { fst := IsFiltered.max j₂ j₃,
                  snd := ↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z }.fst))
        { fst := j₁, snd := x }.snd *
      ↑(F.map
            (IsFiltered.rightToMax { fst := j₁, snd := x }.fst
              { fst := IsFiltered.max j₂ j₃,
                  snd := ↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z }.fst))
        { fst := IsFiltered.max j₂ j₃,
            snd := ↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z }.snd
[PROOFSTEP]
dsimp only
[GOAL]
case mk.mk.mk.e_a.e_snd
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
j₂ : J
y : (F ⋙ forget MonCat).obj j₂
j₃ : J
z : (F ⋙ forget MonCat).obj j₃
⊢ ↑(F.map (𝟙 (IsFiltered.max j₁ (IsFiltered.max j₂ j₃))))
        (↑(F.map (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃))) x *
          ↑(F.map (IsFiltered.leftToMax j₂ j₃ ≫ IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃))) y) *
      ↑(F.map (IsFiltered.rightToMax j₂ j₃ ≫ IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃))) z =
    ↑(F.map (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃))) x *
      ↑(F.map (IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃)))
        (↑(F.map (IsFiltered.leftToMax j₂ j₃)) y * ↑(F.map (IsFiltered.rightToMax j₂ j₃)) z)
[PROOFSTEP]
rw [F.map_id, show ∀ x, (𝟙 (F.obj (IsFiltered.max j₁ (IsFiltered.max j₂ j₃)))) x = x from fun _ => rfl, mul_assoc,
  MonoidHom.map_mul, F.map_comp, F.map_comp]
[GOAL]
case mk.mk.mk.e_a.e_snd
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
src✝ : MulOneClass (M F) := colimitMulOneClass F
j₁ : J
x : (F ⋙ forget MonCat).obj j₁
j₂ : J
y : (F ⋙ forget MonCat).obj j₂
j₃ : J
z : (F ⋙ forget MonCat).obj j₃
⊢ ↑(F.map (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃))) x *
      (↑(F.map (IsFiltered.leftToMax j₂ j₃) ≫ F.map (IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃))) y *
        ↑(F.map (IsFiltered.rightToMax j₂ j₃) ≫ F.map (IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃))) z) =
    ↑(F.map (IsFiltered.leftToMax j₁ (IsFiltered.max j₂ j₃))) x *
      (↑(F.map (IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃))) (↑(F.map (IsFiltered.leftToMax j₂ j₃)) y) *
        ↑(F.map (IsFiltered.rightToMax j₁ (IsFiltered.max j₂ j₃))) (↑(F.map (IsFiltered.rightToMax j₂ j₃)) z))
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x y : ↑(F.obj j)
⊢ OneHom.toFun
      { toFun := NatTrans.app (Types.colimitCocone (F ⋙ forget MonCat)).ι j,
        map_one' := (_ : M.mk F { fst := j, snd := 1 } = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := NatTrans.app (Types.colimitCocone (F ⋙ forget MonCat)).ι j,
          map_one' := (_ : M.mk F { fst := j, snd := 1 } = 1) }
        x *
      OneHom.toFun
        { toFun := NatTrans.app (Types.colimitCocone (F ⋙ forget MonCat)).ι j,
          map_one' := (_ : M.mk F { fst := j, snd := 1 } = 1) }
        y
[PROOFSTEP]
convert (colimit_mul_mk_eq.{v, u} F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 j) (𝟙 j)).symm
[GOAL]
case h.e'_2.h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x y : ↑(F.obj j)
e_1✝ : ↑(colimit F) = M F
⊢ OneHom.toFun
      { toFun := NatTrans.app (Types.colimitCocone (F ⋙ forget MonCat)).ι j,
        map_one' := (_ : M.mk F { fst := j, snd := 1 } = 1) }
      (x * y) =
    M.mk F { fst := j, snd := ↑(F.map (𝟙 j)) { fst := j, snd := x }.snd * ↑(F.map (𝟙 j)) { fst := j, snd := y }.snd }
[PROOFSTEP]
rw [F.map_id]
[GOAL]
case h.e'_2.h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x y : ↑(F.obj j)
e_1✝ : ↑(colimit F) = M F
⊢ OneHom.toFun
      { toFun := NatTrans.app (Types.colimitCocone (F ⋙ forget MonCat)).ι j,
        map_one' := (_ : M.mk F { fst := j, snd := 1 } = 1) }
      (x * y) =
    M.mk F
      { fst := j,
        snd :=
          ↑(𝟙 (F.obj { fst := j, snd := x }.fst)) { fst := j, snd := x }.snd *
            ↑(𝟙 (F.obj { fst := j, snd := x }.fst)) { fst := j, snd := y }.snd }
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
⊢ IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1
[PROOFSTEP]
rw [colimit_one_eq F IsFiltered.Nonempty.some]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
⊢ IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t)
      (M.mk F { fst := Nonempty.some (_ : Nonempty J), snd := 1 }) =
    1
[PROOFSTEP]
exact MonoidHom.map_one _
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
x y : ↑(colimit F)
⊢ OneHom.toFun
      { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
        map_one' :=
          (_ : IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        y
[PROOFSTEP]
refine Quot.induction_on₂ x y ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
x y : ↑(colimit F)
⊢ ∀ (a b : (j : J) × (F ⋙ forget MonCat).obj j),
    OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) b) =
      OneHom.toFun
          { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
            map_one' :=
              (_ :
                IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
          (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a) *
        OneHom.toFun
          { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
            map_one' :=
              (_ :
                IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
          (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) b)
[PROOFSTEP]
clear x y
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
⊢ ∀ (a b : (j : J) × (F ⋙ forget MonCat).obj j),
    OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) b) =
      OneHom.toFun
          { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
            map_one' :=
              (_ :
                IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
          (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) a) *
        OneHom.toFun
          { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
            map_one' :=
              (_ :
                IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
          (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) b)
[PROOFSTEP]
intro x y
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
x y : (j : J) × (F ⋙ forget MonCat).obj j
⊢ OneHom.toFun
      { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
        map_one' :=
          (_ : IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
      (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) x * Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) y) =
    OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) x) *
      OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) y)
[PROOFSTEP]
cases' x with i x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
y : (j : J) × (F ⋙ forget MonCat).obj j
i : J
x : (F ⋙ forget MonCat).obj i
⊢ OneHom.toFun
      { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
        map_one' :=
          (_ : IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
      (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := i, snd := x } *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) y) =
    OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := i, snd := x }) *
      OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) y)
[PROOFSTEP]
cases' y with j y
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : (F ⋙ forget MonCat).obj i
j : J
y : (F ⋙ forget MonCat).obj j
⊢ OneHom.toFun
      { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
        map_one' :=
          (_ : IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
      (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := i, snd := x } *
        Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := y }) =
    OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := i, snd := x }) *
      OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := y })
[PROOFSTEP]
rw [colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j) (IsFiltered.rightToMax i j)]
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : (F ⋙ forget MonCat).obj i
j : J
y : (F ⋙ forget MonCat).obj j
⊢ OneHom.toFun
      { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
        map_one' :=
          (_ : IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
      (M.mk F
        { fst := IsFiltered.max i j,
          snd :=
            ↑(F.map (IsFiltered.leftToMax i j)) { fst := i, snd := x }.snd *
              ↑(F.map (IsFiltered.rightToMax i j)) { fst := j, snd := y }.snd }) =
    OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := i, snd := x }) *
      OneHom.toFun
        { toFun := IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t),
          map_one' :=
            (_ :
              IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget MonCat)) ((forget MonCat).mapCocone t) 1 = 1) }
        (Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat)) { fst := j, snd := y })
[PROOFSTEP]
dsimp [Types.colimitCoconeIsColimit]
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : (F ⋙ forget MonCat).obj i
j : J
y : (F ⋙ forget MonCat).obj j
⊢ ↑(NatTrans.app t.ι (IsFiltered.max i j))
      (↑(F.map (IsFiltered.leftToMax i j)) x * ↑(F.map (IsFiltered.rightToMax i j)) y) =
    ↑(NatTrans.app t.ι i) x * ↑(NatTrans.app t.ι j) y
[PROOFSTEP]
rw [MonoidHom.map_mul]
  -- Porting note : `rw` can't see through coercion is actually forgetful functor,
      -- so can't rewrite `t.w_apply`
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : (F ⋙ forget MonCat).obj i
j : J
y : (F ⋙ forget MonCat).obj j
⊢ ↑(NatTrans.app t.ι (IsFiltered.max i j)) (↑(F.map (IsFiltered.leftToMax i j)) x) *
      ↑(NatTrans.app t.ι (IsFiltered.max i j)) (↑(F.map (IsFiltered.rightToMax i j)) y) =
    ↑(NatTrans.app t.ι i) x * ↑(NatTrans.app t.ι j) y
[PROOFSTEP]
congr 1
[GOAL]
case mk.mk.e_a
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : (F ⋙ forget MonCat).obj i
j : J
y : (F ⋙ forget MonCat).obj j
⊢ ↑(NatTrans.app t.ι (IsFiltered.max i j)) (↑(F.map (IsFiltered.leftToMax i j)) x) = ↑(NatTrans.app t.ι i) x
[PROOFSTEP]
exact t.w_apply _ _
[GOAL]
case mk.mk.e_a
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : (F ⋙ forget MonCat).obj i
j : J
y : (F ⋙ forget MonCat).obj j
⊢ ↑(NatTrans.app t.ι (IsFiltered.max i j)) (↑(F.map (IsFiltered.rightToMax i j)) y) = ↑(NatTrans.app t.ι j) y
[PROOFSTEP]
exact t.w_apply _ _
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
x y : ↑(M F)
⊢ x * y = y * x
[PROOFSTEP]
refine Quot.induction_on₂ x y ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
x y : ↑(M F)
⊢ ∀ (a b : (j : J) × ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) a *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) b =
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) b *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) a
[PROOFSTEP]
clear x y
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
⊢ ∀ (a b : (j : J) × ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) a *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) b =
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) b *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) a
[PROOFSTEP]
intro x y
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
x y : (j : J) × ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat).obj j
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) x *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) y =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) y *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) x
[PROOFSTEP]
let k := max' x.1 y.1
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
x y : (j : J) × ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat).obj j
k : J := IsFiltered.max x.fst y.fst
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) x *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) y =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) y *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) x
[PROOFSTEP]
let f := IsFiltered.leftToMax x.1 y.1
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
x y : (j : J) × ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat).obj j
k : J := IsFiltered.max x.fst y.fst
f : x.fst ⟶ IsFiltered.max x.fst y.fst := IsFiltered.leftToMax x.fst y.fst
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) x *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) y =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) y *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) x
[PROOFSTEP]
let g := IsFiltered.rightToMax x.1 y.1
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
x y : (j : J) × ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat).obj j
k : J := IsFiltered.max x.fst y.fst
f : x.fst ⟶ IsFiltered.max x.fst y.fst := IsFiltered.leftToMax x.fst y.fst
g : y.fst ⟶ IsFiltered.max x.fst y.fst := IsFiltered.rightToMax x.fst y.fst
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) x *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) y =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) y *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat)) x
[PROOFSTEP]
rw [colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) x y k f g,
  colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) y x k g f]
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
x y : (j : J) × ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat).obj j
k : J := IsFiltered.max x.fst y.fst
f : x.fst ⟶ IsFiltered.max x.fst y.fst := IsFiltered.leftToMax x.fst y.fst
g : y.fst ⟶ IsFiltered.max x.fst y.fst := IsFiltered.rightToMax x.fst y.fst
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      { fst := k,
        snd := ↑((F ⋙ forget₂ CommMonCat MonCat).map f) x.snd * ↑((F ⋙ forget₂ CommMonCat MonCat).map g) y.snd } =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      { fst := k,
        snd := ↑((F ⋙ forget₂ CommMonCat MonCat).map g) y.snd * ↑((F ⋙ forget₂ CommMonCat MonCat).map f) x.snd }
[PROOFSTEP]
dsimp
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
src✝ : MonCat := M F
x y : (j : J) × ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat).obj j
k : J := IsFiltered.max x.fst y.fst
f : x.fst ⟶ IsFiltered.max x.fst y.fst := IsFiltered.leftToMax x.fst y.fst
g : y.fst ⟶ IsFiltered.max x.fst y.fst := IsFiltered.rightToMax x.fst y.fst
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      { fst := IsFiltered.max x.fst y.fst,
        snd :=
          ↑((forget₂ CommMonCat MonCat).map (F.map (IsFiltered.leftToMax x.fst y.fst))) x.snd *
            ↑((forget₂ CommMonCat MonCat).map (F.map (IsFiltered.rightToMax x.fst y.fst))) y.snd } =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      { fst := IsFiltered.max x.fst y.fst,
        snd :=
          ↑((forget₂ CommMonCat MonCat).map (F.map (IsFiltered.rightToMax x.fst y.fst))) y.snd *
            ↑((forget₂ CommMonCat MonCat).map (F.map (IsFiltered.leftToMax x.fst y.fst))) x.snd }
[PROOFSTEP]
rw [mul_comm]


[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ↑χ ⁅x, y⁆ = 0
[PROOFSTEP]
rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ⁅↑χ x, ↑χ y⁆ = 0
[PROOFSTEP]
rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ derivedSeries R L 1
⊢ ↑χ x = 0
[PROOFSTEP]
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, ← LieSubmodule.mem_coeSubmodule,
  LieSubmodule.lieIdeal_oper_eq_linear_span] at h
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ↑χ x = 0
[PROOFSTEP]
refine' Submodule.span_induction h _ _ _ _
[GOAL]
case refine'_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (x : L), x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → ↑χ x = 0
[PROOFSTEP]
rintro y ⟨⟨z, hz⟩, ⟨⟨w, hw⟩, rfl⟩⟩
[GOAL]
case refine'_1.intro.mk.intro.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
z : L
hz : z ∈ ⊤
w : L
hw : w ∈ ⊤
⊢ ↑χ ⁅↑{ val := z, property := hz }, ↑{ val := w, property := hw }⁆ = 0
[PROOFSTEP]
apply lieCharacter_apply_lie
[GOAL]
case refine'_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ↑χ 0 = 0
[PROOFSTEP]
exact χ.map_zero
[GOAL]
case refine'_3
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (x y : L), ↑χ x = 0 → ↑χ y = 0 → ↑χ (x + y) = 0
[PROOFSTEP]
intro y z hy hz
[GOAL]
case refine'_3
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
y z : L
hy : ↑χ y = 0
hz : ↑χ z = 0
⊢ ↑χ (y + z) = 0
[PROOFSTEP]
rw [LieHom.map_add, hy, hz, add_zero]
[GOAL]
case refine'_4
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ ∀ (a : R) (x : L), ↑χ x = 0 → ↑χ (a • x) = 0
[PROOFSTEP]
intro t y hy
[GOAL]
case refine'_4
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
h : x ∈ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
t : R
y : L
hy : ↑χ y = 0
⊢ ↑χ (t • y) = 0
[PROOFSTEP]
rw [LieHom.map_smul, hy, smul_zero]
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
x y : L
⊢ AddHom.toFun
      { toAddHom := ψ.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : L),
                AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        { toAddHom := ψ.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
        x,
      AddHom.toFun
        { toAddHom := ψ.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : L),
                  AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
        y⁆
[PROOFSTEP]
rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self, LinearMap.toFun_eq_coe,
  LinearMap.map_zero]
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
χ : LieCharacter R L
⊢ (fun ψ =>
        {
          toLinearMap :=
            { toAddHom := ψ.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : L), AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) },
          map_lie' :=
            (_ :
              ∀ {x y : L},
                AddHom.toFun
                    { toAddHom := ψ.toAddHom,
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : L),
                              AddHom.toFun ψ.toAddHom (r • x) =
                                ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                    ⁅x, y⁆ =
                  ⁅AddHom.toFun
                      { toAddHom := ψ.toAddHom,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : L),
                                AddHom.toFun ψ.toAddHom (r • x) =
                                  ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                      x,
                    AddHom.toFun
                      { toAddHom := ψ.toAddHom,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : L),
                                AddHom.toFun ψ.toAddHom (r • x) =
                                  ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                      y⁆) })
      ((fun χ => ↑χ) χ) =
    χ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
χ : LieCharacter R L
x✝ : L
⊢ ↑((fun ψ =>
            {
              toLinearMap :=
                { toAddHom := ψ.toAddHom,
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : L),
                        AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) },
              map_lie' :=
                (_ :
                  ∀ {x y : L},
                    AddHom.toFun
                        { toAddHom := ψ.toAddHom,
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : L),
                                  AddHom.toFun ψ.toAddHom (r • x) =
                                    ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                        ⁅x, y⁆ =
                      ⁅AddHom.toFun
                          { toAddHom := ψ.toAddHom,
                              map_smul' :=
                                (_ :
                                  ∀ (r : R) (x : L),
                                    AddHom.toFun ψ.toAddHom (r • x) =
                                      ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                          x,
                        AddHom.toFun
                          { toAddHom := ψ.toAddHom,
                              map_smul' :=
                                (_ :
                                  ∀ (r : R) (x : L),
                                    AddHom.toFun ψ.toAddHom (r • x) =
                                      ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                          y⁆) })
          ((fun χ => ↑χ) χ))
      x✝ =
    ↑χ x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
⊢ (fun χ => ↑χ)
      ((fun ψ =>
          {
            toLinearMap :=
              { toAddHom := ψ.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : L),
                      AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) },
            map_lie' :=
              (_ :
                ∀ {x y : L},
                  AddHom.toFun
                      { toAddHom := ψ.toAddHom,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : L),
                                AddHom.toFun ψ.toAddHom (r • x) =
                                  ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                      ⁅x, y⁆ =
                    ⁅AddHom.toFun
                        { toAddHom := ψ.toAddHom,
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : L),
                                  AddHom.toFun ψ.toAddHom (r • x) =
                                    ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                        x,
                      AddHom.toFun
                        { toAddHom := ψ.toAddHom,
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : L),
                                  AddHom.toFun ψ.toAddHom (r • x) =
                                    ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                        y⁆) })
        ψ) =
    ψ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsLieAbelian L
ψ : Module.Dual R L
x✝ : L
⊢ ↑((fun χ => ↑χ)
          ((fun ψ =>
              {
                toLinearMap :=
                  { toAddHom := ψ.toAddHom,
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : L),
                          AddHom.toFun ψ.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) },
                map_lie' :=
                  (_ :
                    ∀ {x y : L},
                      AddHom.toFun
                          { toAddHom := ψ.toAddHom,
                              map_smul' :=
                                (_ :
                                  ∀ (r : R) (x : L),
                                    AddHom.toFun ψ.toAddHom (r • x) =
                                      ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                          ⁅x, y⁆ =
                        ⁅AddHom.toFun
                            { toAddHom := ψ.toAddHom,
                                map_smul' :=
                                  (_ :
                                    ∀ (r : R) (x : L),
                                      AddHom.toFun ψ.toAddHom (r • x) =
                                        ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                            x,
                          AddHom.toFun
                            { toAddHom := ψ.toAddHom,
                                map_smul' :=
                                  (_ :
                                    ∀ (r : R) (x : L),
                                      AddHom.toFun ψ.toAddHom (r • x) =
                                        ↑(RingHom.id R) r • AddHom.toFun ψ.toAddHom x) }.toAddHom
                            y⁆) })
            ψ))
      x✝ =
    ↑ψ x✝
[PROOFSTEP]
rfl