awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst_2 : HasPushout f g
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q P)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Q (pushout f g)) (Q ◁ pushout.inl f g)
      (Q ◁ Iso.inv hP.isoPushout))
    (Q ◁ inl)

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst_2 : HasPushout f g
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q P)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Q (pushout f g)) (Q ◁ pushout.inr f g)
      (Q ◁ Iso.inv hP.isoPushout))
    (Q ◁ inr)

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst_2 : HasPushout f g
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout f g))
    (Q ◁ inl ≫ Q ◁ Iso.hom hP.isoPushout) (Q ◁ pushout.inl f g)

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst_2 : HasPushout f g
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout f g))
    (Q ◁ inr ≫ Q ◁ Iso.hom hP.isoPushout) (Q ◁ pushout.inr f g)

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst_2 : HasPushout f g
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) P Q)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (pushout f g) Q) (pushout.inl f g ▷ Q)
      (Iso.inv hP.isoPushout ▷ Q))
    (inl ▷ Q)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst_2 : HasPushout f g
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) P Q)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (pushout f g) Q) (pushout.inr f g ▷ Q)
      (Iso.inv hP.isoPushout ▷ Q))
    (inr ▷ Q)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst_2 : HasPushout f g
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout f g) Q)
    (inl ▷ Q ≫ Iso.hom hP.isoPushout ▷ Q) (pushout.inl f g ▷ Q)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst_2 : HasPushout f g
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout f g) Q)
    (inr ▷ Q ≫ Iso.hom hP.isoPushout ▷ Q) (pushout.inr f g ▷ Q)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout f g))
    (Q ◁ f ≫ Q ◁ pushout.inl f g) (Q ◁ g ≫ Q ◁ pushout.inr f g)

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp, pushout.condition]

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout f g) Q)
    (f ▷ Q ≫ pushout.inl f g ▷ Q) (g ▷ Q ≫ pushout.inr f g ▷ Q)

Tactic:
simp [← comp_whiskerRight, pushout.condition]

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ X
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ f ▷ tensorObj.{v, u} (𝒞 := inst) Z W ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ h ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ h ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
rw₃ rw₄ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (f ▷ Z ▷ W ≫ Iso.hom (α_ B Z W) ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))

Tactic:
rw [associator_naturality_left_assoc, ← whisker_exchange_assoc, pushout.condition,
    ← MonoidalCategory.whiskerLeft_comp_assoc]

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.associator_naturality_left_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ A
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ tensorObj.{v, u} (𝒞 := inst) Z W ◁ g ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ h ▷ X ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ h ▷ X ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
rw₃ rw₄ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Z ◁ W ◁ g ≫ Iso.inv (α_ Z W Y) ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ← pushout.condition,
    ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc, CategoryTheory.Limits.pushout.condition, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout g f))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Q (pushout f g)) (Q ◁ pushout.inl f g)
        (Q ◁ Iso.hom (pushoutSymmetry f g)) :
      tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout g f))
    (Q ◁ pushout.inr g f : tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout g f))

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Z ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout g f))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Q (pushout f g)) (Q ◁ pushout.inr f g)
        (Q ◁ Iso.hom (pushoutSymmetry f g)) :
      tensorObj.{v, u} (𝒞 := inst) Q Z ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout g f))
    (Q ◁ pushout.inl g f : tensorObj.{v, u} (𝒞 := inst) Q Z ⟶ tensorObj.{v, u} (𝒞 := inst) Q (pushout g f))

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout g f) Q)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (pushout f g) Q) (pushout.inl f g ▷ Q)
        (Iso.hom (pushoutSymmetry f g) ▷ Q) :
      tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout g f) Q)
    (pushout.inr g f ▷ Q : tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout g f) Q)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Z Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout g f) Q)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (pushout f g) Q) (pushout.inr f g ▷ Q)
        (Iso.hom (pushoutSymmetry f g) ▷ Q) :
      tensorObj.{v, u} (𝒞 := inst) Z Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout g f) Q)
    (pushout.inl g f ▷ Q : tensorObj.{v, u} (𝒞 := inst) Z Q ⟶ tensorObj.{v, u} (𝒞 := inst) (pushout g f) Q)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Linear
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
a :
  F.map (X ◁ (r • f)) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f))
⊢ X ◁ (r • f) =
    HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f)

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Linear
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
a :
  CategoryStruct.comp (Y := tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Y)) (Functor.OplaxMonoidal.δ F X Y)
      (F.obj X ◁ F.map (r • f) ≫ Functor.LaxMonoidal.μ F X Z) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f))
⊢ F.map (X ◁ (r • f)) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f))

Tactic:
rw [Functor.Monoidal.map_whiskerLeft]

Premises used: CategoryTheory.Functor.Monoidal.map_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Linear
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ CategoryStruct.comp (Y := tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Y)) (Functor.OplaxMonoidal.δ F X Y)
      (F.obj X ◁ F.map (r • f) ≫ Functor.LaxMonoidal.μ F X Z) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Linear
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
a :
  F.map ((r • f) ▷ Z) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z))
⊢ (r • f) ▷ Z =
    HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z)

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Linear
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
a :
  CategoryStruct.comp (Y := tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z)) (Functor.OplaxMonoidal.δ F X Z)
      (F.map (r • f) ▷ F.obj Z ≫ Functor.LaxMonoidal.μ F Y Z) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z))
⊢ F.map ((r • f) ▷ Z) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z))

Tactic:
rw [Functor.Monoidal.map_whiskerRight]

Premises used: CategoryTheory.Functor.Monoidal.map_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Linear
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ CategoryStruct.comp (Y := tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z)) (Functor.OplaxMonoidal.δ F X Z)
      (F.map (r • f) ▷ F.obj Z ≫ Functor.LaxMonoidal.μ F Y Z) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
inst_5 : ModObj.{v₁, v₂, u₁, u₂} M X
⊢ Eq.{v₂ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M
        (@MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X) ⟶
      X)
    (M ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ @smul _ _ _ _ _ _ _ inst_4 _ _)
    (Iso.inv (αₗ M M X) ≫ μ ⊵ₗ X ≫ @smul _ _ _ _ _ _ _ inst_4 _ _)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
⊢ Eq.{v₁ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M M ⟶ M)
    (@smul _ _ _ _ _ _ _ inst_2 _ _) μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
X : C
h₁ h₂ : ModObj M X
H :
  Eq.{v₁ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
    (@smul _ _ _ _ _ _ _ inst_2 _ _) (@smul _ _ _ _ _ _ _ inst_2 _ _)
mk :
  ∀ (smul : @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
    (one_smul : η ⊵ₗ X ≫ smul = Iso.hom (λₗ X)) (mul_smul : μ ⊵ₗ X ≫ smul = Iso.hom (αₗ M M X) ≫ M ⊴ₗ smul ≫ smul)
    (H :
      Eq.{v₁ + 1} (α :=
        @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
        (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _) (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)),
    { smul := smul, one_smul := one_smul, mul_smul := mul_smul : ModObj M X } = h₂
⊢ h₁ = h₂

Tactic:
cases h₁
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
X : C
h₂ : ModObj M X
smul : @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X
one_smul : η ⊵ₗ X ≫ smul = Iso.hom (λₗ X)
mul_smul : μ ⊵ₗ X ≫ smul = Iso.hom (αₗ M M X) ≫ M ⊴ₗ smul ≫ smul
H :
  Eq.{v₁ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
    (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _) (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)
mk :
  ∀ (smul_1 : @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
    (one_smul_1 : η ⊵ₗ X ≫ smul_1 = Iso.hom (λₗ X))
    (mul_smul_1 : μ ⊵ₗ X ≫ smul_1 = Iso.hom (αₗ M M X) ≫ M ⊴ₗ smul_1 ≫ smul_1)
    (H :
      Eq.{v₁ + 1} (α :=
        @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
        (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _) (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)),
    { smul := smul, one_smul := one_smul, mul_smul := mul_smul : ModObj M X } =
      { smul := smul_1, one_smul := one_smul_1, mul_smul := mul_smul_1 }
⊢ { smul := smul, one_smul := one_smul, mul_smul := mul_smul : ModObj M X } = h₂

Tactic:
cases h₂