-- Mathlib/CategoryTheory/Monoidal/Linear.lean
theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linear R D]
    [MonoidalCategory D] [MonoidalPreadditive D] (F : D ⥤ C) [F.Monoidal] [F.Faithful]
    [F.Linear R] : MonoidalLinear R D :=
  { whiskerLeft_smul

Proof state:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
⊢ ∀ (X : D) {Y Z : D} (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f

Tactic:
intros X Y Z r f

Result:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ X ◁ (r • f) = r • X ◁ f

Proof state:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
⊢ ∀ (r : R) {Y Z : D} (f : Y ⟶ Z) (X : D), (r • f) ▷ X = r • f ▷ X

Tactic:
intros r X Y f Z

Result:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ (r • f) ▷ Z = r • f ▷ Z

Proof state:
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ F.map (X ◁ (r • f)) = F.map (r • X ◁ f)

Tactic:
rw [Functor.Monoidal.map_whiskerLeft]

Result:
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ Functor.OplaxMonoidal.δ F X Y ≫ F.obj X ◁ F.map (r • f) ≫ Functor.LaxMonoidal.μ F X Z = F.map (r • X ◁ f)

Proof state:
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ F.map ((r • f) ▷ Z) = F.map (r • f ▷ Z)

Tactic:
rw [Functor.Monoidal.map_whiskerRight]

Result:
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ Functor.OplaxMonoidal.δ F X Z ≫ F.map (r • f) ▷ F.obj Z ≫ Functor.LaxMonoidal.μ F Y Z = F.map (r • f ▷ Z)

Proof state:
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ Functor.OplaxMonoidal.δ F X Z ≫ F.map (r • f) ▷ F.obj Z ≫ Functor.LaxMonoidal.μ F Y Z = F.map (r • f ▷ Z)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ (r • f) ▷ Z = r • f ▷ Z

Tactic:
apply F.map_injective

Result:
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ F.map ((r • f) ▷ Z) = F.map (r • f ▷ Z)

Proof state:
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ Functor.OplaxMonoidal.δ F X Y ≫ F.obj X ◁ F.map (r • f) ≫ Functor.LaxMonoidal.μ F X Z = F.map (r • X ◁ f)

Tactic:
simp

Result:
no goals