[GOAL]
⊢ ∀ {X' X : SemigroupCat} {Y : MonCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ MonCat SemigroupCat).obj Y),
    ↑((fun S M => WithOne.lift.symm) X' Y).symm (f ≫ g) = adjoinOne.map f ≫ ↑((fun S M => WithOne.lift.symm) X Y).symm g
[PROOFSTEP]
intro S T M f g
[GOAL]
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
⊢ ↑((fun S M => WithOne.lift.symm) S M).symm (f ≫ g) = adjoinOne.map f ≫ ↑((fun S M => WithOne.lift.symm) T M).symm g
[PROOFSTEP]
ext x
[GOAL]
case w
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
x : ↑(adjoinOne.obj S)
⊢ ↑(↑((fun S M => WithOne.lift.symm) S M).symm (f ≫ g)) x =
    ↑(adjoinOne.map f ≫ ↑((fun S M => WithOne.lift.symm) T M).symm g) x
[PROOFSTEP]
simp only [Equiv.symm_symm, adjoinOne_map, coe_comp]
[GOAL]
case w
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
x : ↑(adjoinOne.obj S)
⊢ ↑(↑WithOne.lift (f ≫ g)) x = ↑(WithOne.map f ≫ ↑WithOne.lift g) x
[PROOFSTEP]
simp_rw [WithOne.map]
[GOAL]
case w
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
x : ↑(adjoinOne.obj S)
⊢ ↑(↑WithOne.lift (f ≫ g)) x = ↑(↑WithOne.lift (MulHom.comp WithOne.coeMulHom f) ≫ ↑WithOne.lift g) x
[PROOFSTEP]
cases x
[GOAL]
case w.none
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
⊢ ↑(↑WithOne.lift (f ≫ g)) none = ↑(↑WithOne.lift (MulHom.comp WithOne.coeMulHom f) ≫ ↑WithOne.lift g) none
[PROOFSTEP]
rfl
[GOAL]
case w.some
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
val✝ : ↑S
⊢ ↑(↑WithOne.lift (f ≫ g)) (some val✝) =
    ↑(↑WithOne.lift (MulHom.comp WithOne.coeMulHom f) ≫ ↑WithOne.lift g) (some val✝)
[PROOFSTEP]
simp
[GOAL]
case w.some
S T : SemigroupCat
M : MonCat
f : S ⟶ T
g : T ⟶ (forget₂ MonCat SemigroupCat).obj M
val✝ : ↑S
⊢ ↑(↑WithOne.lift (f ≫ g)) (some val✝) =
    ↑(↑WithOne.lift g) (↑(↑WithOne.lift (MulHom.comp WithOne.coeMulHom f)) (some val✝))
[PROOFSTEP]
rfl
