instOplaxMonoidal — Mathlib

Lean4
instance : F.OplaxMonoidal where
  η := terminalComparison F
  δ X Y := prodComparison F X Y
  δ_natural_left _ _ := by simp [prodComparison_natural]
  δ_natural_right _ _ := by simp [prodComparison_natural]
  oplax_associativity _ _
    _ := by
    dsimp
    ext
    · dsimp
      simp only [Category.assoc, prod.map_fst, Category.comp_id, prodComparison_fst, ← Functor.map_comp]
      erw [associator_hom_fst, associator_hom_fst]
      simp
    · dsimp
      simp only [Category.assoc, prod.map_snd, prodComparison_snd_assoc, prodComparison_fst, ← Functor.map_comp]
      erw [associator_hom_snd_fst, associator_hom_snd_fst]
      simp
    · dsimp
      simp only [Category.assoc, prod.map_snd, prodComparison_snd_assoc, prodComparison_snd, ← Functor.map_comp]
      erw [associator_hom_snd_snd, associator_hom_snd_snd]
      simp
  oplax_left_unitality _ := by ext; simp [← Functor.map_comp]
  oplax_right_unitality _ := by ext; simp [← Functor.map_comp]
Похожие утверждения